[Merged by Bors] - feat(Finset): extra toLeft/toRight API

[YaelDillies]

Add the API that I independently came up with in #20433 (comment).

---

[github-actions]

PR summary 97680769fd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ disjSum_subset
+ gc_map_inl_toLeft
+ gc_map_inr_toRight
+ map_inl_subset_iff_subset_toLeft
+ map_inr_subset_iff_subset_toRight
+ subset_disjSum
+ subset_map_inl
+ subset_map_inr
+ toLeft_eq_empty
+ toLeft_eq_univ
+ toLeft_univ
+ toRight_eq_empty
+ toRight_eq_univ
+ toRight_univ
+ univ_disjSum_univ
- Finset.univ_disjSum_univ

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[YaelDillies]

@fpvandoorn, what's your preferred way for me to fix the simps error in Logic.Equiv.Set?

[b-mehta]

The finset/fintype changes look great to me

[fpvandoorn]

@fpvandoorn, what's your preferred way for me to fix the simps error in Logic.Equiv.Set?

By making sure that Logic.Equiv.Defs imports a file containing initialize_simps_projections Subtype (val → coe) (currently Data.Subtype).
At least, I think that is the issue.
If that is the issue, please open an issue that simps should raise a warning when two conflicting configurations are found in different imports.

[fpvandoorn]

#23041 might also help

[fpvandoorn]

Or, going even further, we can disallow @[simps] at all, unless initialize_simps_projections has been called explicitly.

When I wrote @[simps], I was under the impression that being more permissive is better: if the user wants to do X, it should try to do X as best as it can. However, I realize that in the current Mathlib with its many refactors, this is not desired: refactors often unintentionally change things, and simps should just complain whenever something changes.

Please open issues (or make fixes to simps) with how you want it to behave.
In particular, the suggestion at the start of this message is easy: currently getRawProjections either retrieves projection information, or generates it. Splitting that up into two separate functions would do the trick.

[YaelDillies]

By making sure that Logic.Equiv.Defs imports a file containing initialize_simps_projections Subtype (val → coe) (currently Data.Subtype).

Indeed that's the case.

If that is the issue, please open an issue that simps should raise a warning when two conflicting configurations are found in different imports.

I see that you have opened #23041 for that, so I will refrain from doing so.

[fpvandoorn]

It's not quite the same, but I added it to that issue.

Do you think this would be good?

Or, going even further, we can disallow @[simps] at all, unless initialize_simps_projections has been called explicitly.

[eric-wieser]

Interestingly the new function seems to avoid stackoverflows where the previous one did not:

def foo : Finset (ℕ ⊕ ℕ) := (Finset.Icc 0 100000).map .inl

set_option trace.profiler true in
#eval foo.toLeft.card

succeeds only with this PR.

[b-mehta]

This is now very nice, thank you!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style