[Merged by Bors] - feat(Logic/Embedding/Set): Injections from subtypes of disjoint sets

[apnelson1]

For disjoint s t : Set α, there is a natural injection from ↑s ⊕ ↑t to α. We provide this as an embedding, and do the same for an indexed family of pairwise disjoint sets.

---

[github-actions]

PR summary 88b771f010

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Logic.Embedding.Set	223	315	+92 (+41.26%)

Import changes for all files

Files	Import difference
80 files Mathlib.CategoryTheory.Limits.Constructions.Filtered Mathlib.Data.Finset.PiInduction Mathlib.Data.Fintype.Sum Mathlib.Data.Fintype.Powerset Mathlib.Data.SetLike.Fintype Mathlib.Data.W.Constructions Mathlib.Order.CountableDenseLinearOrder Mathlib.Data.QPF.Multivariate.Basic Mathlib.Data.W.Basic Mathlib.Data.Finset.Lattice Mathlib.CategoryTheory.Enriched.Basic Mathlib.Algebra.Group.Subgroup.ZPowers Mathlib.Data.PFunctor.Univariate.M Mathlib.Dynamics.PeriodicPts Mathlib.Order.JordanHolder Mathlib.CategoryTheory.Closed.Ideal Mathlib.Data.PFunctor.Multivariate.M Mathlib.Data.PFunctor.Multivariate.W Mathlib.Algebra.Order.Ring.Finset Mathlib.Data.Finset.Powerset Mathlib.Order.Category.OmegaCompletePartialOrder Mathlib.Computability.ContextFreeGrammar Mathlib.Data.Finset.Sym Mathlib.Combinatorics.SetFamily.Kleitman Mathlib.CategoryTheory.Monoidal.Types.Basic Mathlib.Data.Finset.Pairwise Mathlib.Data.Fintype.Sort Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory Mathlib.CategoryTheory.Monoidal.Internal.Types Mathlib.CategoryTheory.Monoidal.Types.Coyoneda Mathlib.Data.Fintype.Array Mathlib.Computability.Halting Mathlib.Order.SupIndep Mathlib.Logic.Equiv.Array Mathlib.Order.Irreducible Mathlib.Data.Finite.Basic Mathlib.Computability.Partrec Mathlib.Computability.Language Mathlib.CategoryTheory.Limits.Constructions.Over.Basic Mathlib.Data.Fintype.Sigma Mathlib.Data.QPF.Multivariate.Constructions.Quot Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts Mathlib.Data.QPF.Multivariate.Constructions.Fix Mathlib.Computability.TMToPartrec Mathlib.Logic.Equiv.List Mathlib.Order.Minimal Mathlib.Computability.DFA Mathlib.Data.Fintype.List Mathlib.Data.Finset.Sort Mathlib.Computability.NFA Mathlib.Data.QPF.Multivariate.Constructions.Comp Mathlib.Data.QPF.Multivariate.Constructions.Prj Mathlib.Computability.Primrec Mathlib.Combinatorics.SetFamily.HarrisKleitman Mathlib.Data.Finmap Mathlib.Computability.EpsilonNFA Mathlib.Computability.Reduce Mathlib.Data.PFunctor.Univariate.Basic Mathlib.Data.QPF.Multivariate.Constructions.Sigma Mathlib.Data.QPF.Univariate.Basic Mathlib.CategoryTheory.Monoidal.Types.Symmetric Mathlib.Data.Finset.Sigma Mathlib.Combinatorics.SetFamily.Compression.Down Mathlib.CategoryTheory.Limits.VanKampen Mathlib.Data.QPF.Multivariate.Constructions.Const Mathlib.CategoryTheory.ChosenFiniteProducts Mathlib.Data.FunLike.Fintype Mathlib.Computability.PartrecCode Mathlib.CategoryTheory.Limits.Lattice Mathlib.Data.QPF.Multivariate.Constructions.Cofix Mathlib.Tactic.DeriveFintype Mathlib.CategoryTheory.Limits.FintypeCat Mathlib.Computability.Ackermann Mathlib.Data.PFunctor.Multivariate.Basic Mathlib.Computability.RegularExpressions Mathlib.Algebra.Order.Field.Pi Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers Mathlib.Data.Countable.Basic Mathlib.Data.List.Cycle Mathlib.Data.Fintype.Lattice	2
4 files Mathlib.Logic.Equiv.Fin Mathlib.Algebra.Ring.Fin Mathlib.Data.Fin.Tuple.Curry Mathlib.Order.Fin.Tuple	3
Mathlib.Order.RelIso.Set Mathlib.Order.InitialSeg	89
Mathlib.Logic.Equiv.Embedding Mathlib.Logic.Embedding.Set	92

---

Declarations diff

+ Function.Embedding.coe_sigmaSet
+ Function.Embedding.coe_sumSet
+ Function.Embedding.sigmaSet
+ Function.Embedding.sigmaSet_preimage
+ Function.Embedding.sigmaSet_range
+ Function.Embedding.sumSet
+ Function.Embedding.sumSet_preimage_inl
+ Function.Embedding.sumSet_preimage_inr
+ Function.Embedding.sumSet_range

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>

[kim-em]

(@YaelDillies, it's helpful when you leave review comments requesting changes if you can add the awaiting-author label, so the PR comes off the queue in the meantime.)

[YaelDillies]

Sorry, I do that except that here it was a quick back and forth and maybe someone else would have wanted to comment. If you see such a PR and have nothing else to comment then please add awaiting-author.

[YaelDillies]

Looks otherwise okay

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ apnelson1 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[apnelson1]

bors r+

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style