feat(Combinatorics): Set-Valued Pigeonhole Principle

[cjrl]

This PR contributes two theorems to combinatorics:

• exists_lt_card_cover_of_card_biUnion_lt_card is a set-valued version of the pigeonhole principle.

• sum_card_eq_sum_card_cover_biUnion is a set theoretic corollary of a double counting result proved for bipartite graphs (Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow). This was needed to prove the above pigeonhole principle.

The motivation for these results is our Latin Square PR #36698. These results were proved in less general terms in that PR, but are independent of Latin Square considerations and so we have generalized and moved them into more relevant files.

---

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 9059feef90

Import changes exceeding 2%

%	File
+4.28%	Mathlib.Algebra.BigOperators.Group.Finset.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.BigOperators.Group.Finset.Basic	467	487	+20 (+4.28%)
Mathlib.Combinatorics.Enumerative.DoubleCounting	646	647	+1 (+0.15%)
Mathlib.Combinatorics.Pigeonhole	775	776	+1 (+0.13%)

Import changes for all files

Files	Import difference
328 files Mathlib.Algebra.Algebra.Basic Mathlib.Algebra.Algebra.Bilinear Mathlib.Algebra.Algebra.Equiv Mathlib.Algebra.Algebra.Hom.Rat Mathlib.Algebra.Algebra.Hom Mathlib.Algebra.Algebra.IsSimpleRing Mathlib.Algebra.Algebra.NonUnitalHom Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Algebra.Algebra.Opposite Mathlib.Algebra.Algebra.Pi Mathlib.Algebra.Algebra.Prod Mathlib.Algebra.Algebra.RestrictScalars Mathlib.Algebra.Algebra.Shrink Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Algebra.Algebra.Tower Mathlib.Algebra.Algebra.TransferInstance Mathlib.Algebra.Algebra.Unitization Mathlib.Algebra.BigOperators.Associated Mathlib.Algebra.BigOperators.Field Mathlib.Algebra.BigOperators.Finprod Mathlib.Algebra.BigOperators.Finsupp.Basic Mathlib.Algebra.BigOperators.Group.Finset.Gaps Mathlib.Algebra.BigOperators.Group.Finset.Interval Mathlib.Algebra.BigOperators.Group.Finset.Preimage Mathlib.Algebra.BigOperators.GroupWithZero.Action Mathlib.Algebra.BigOperators.NatAntidiagonal Mathlib.Algebra.BigOperators.Ring.Finset Mathlib.Algebra.BigOperators.Sym Mathlib.Algebra.Category.Grp.Biproducts Mathlib.Algebra.Category.Grp.CartesianMonoidal Mathlib.Algebra.Category.Grp.Colimits Mathlib.Algebra.Category.Grp.LeftExactFunctor Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.MonCat.Adjunctions Mathlib.Algebra.ContinuedFractions.Computation.Approximations Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat Mathlib.Algebra.DirectSum.AddChar Mathlib.Algebra.DirectSum.Basic Mathlib.Algebra.DirectSum.Ring Mathlib.Algebra.Exact Mathlib.Algebra.Field.Subfield.Basic Mathlib.Algebra.FiniteSupport.Basic Mathlib.Algebra.FiveLemma Mathlib.Algebra.FreeAbelianGroup.Finsupp Mathlib.Algebra.GCDMonoid.FinsetLemmas Mathlib.Algebra.Group.AddChar Mathlib.Algebra.Group.Subgroup.Finsupp Mathlib.Algebra.Group.Submonoid.Finsupp Mathlib.Algebra.GroupWithZero.Torsion Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.CommSq Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.Linear Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Homology.Square Mathlib.Algebra.Lie.Basic Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra Mathlib.Algebra.Module.LinearMap.DivisionRing Mathlib.Algebra.Module.Presentation.Basic Mathlib.Algebra.Module.Presentation.Cokernel Mathlib.Algebra.Module.Presentation.Tautological Mathlib.Algebra.Module.Presentation.Tensor Mathlib.Algebra.Module.SnakeLemma Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Algebra.Module.Submodule.Invariant Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Algebra.Module.Submodule.Ker Mathlib.Algebra.Module.Submodule.Lattice Mathlib.Algebra.Module.Submodule.Map Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.Algebra.Module.Submodule.Range Mathlib.Algebra.Module.Submodule.RestrictScalars Mathlib.Algebra.MonoidAlgebra.Defs Mathlib.Algebra.MonoidAlgebra.Division Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Algebra.MonoidAlgebra.Lift Mathlib.Algebra.MonoidAlgebra.MapDomain Mathlib.Algebra.MonoidAlgebra.Opposite Mathlib.Algebra.NonAssoc.LieAdmissible.Defs Mathlib.Algebra.Order.BigOperators.Ring.Finset Mathlib.Algebra.Order.Group.Int.Sum Mathlib.Algebra.Order.Module.Archimedean Mathlib.Algebra.Order.Ring.Ordering.Basic Mathlib.Algebra.Order.Ring.Ordering.Defs Mathlib.Algebra.Order.Star.Conjneg Mathlib.Algebra.Ring.CentroidHom Mathlib.Algebra.Ring.Semireal.Defs Mathlib.Algebra.Ring.Subring.Basic Mathlib.Algebra.Ring.Subring.MulOpposite Mathlib.Algebra.Ring.Subring.Pointwise Mathlib.Algebra.Ring.Subsemiring.Basic Mathlib.Algebra.Ring.Subsemiring.MulOpposite Mathlib.Algebra.Ring.Subsemiring.Pointwise Mathlib.Algebra.Ring.SumsOfSquares Mathlib.Algebra.RingQuot Mathlib.Algebra.Star.BigOperators Mathlib.Algebra.Star.CentroidHom Mathlib.Algebra.Star.Module Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Algebra.Star.RingQuot Mathlib.Algebra.Star.StarAlgHom Mathlib.Algebra.Star.Subsemiring Mathlib.Algebra.Star.TensorProduct Mathlib.Algebra.Tropical.BigOperators Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Center.Localization Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.CategoryTheory.Localization.Linear Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.CategoryTheory.Preadditive.CommGrp_ Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.CategoryTheory.Preadditive.Transfer Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Shift.Linear Mathlib.CategoryTheory.Shift.Opposite Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.CompatiblePlus Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.CategoryTheory.Sites.Continuous Mathlib.CategoryTheory.Sites.CoproductSheafCondition Mathlib.CategoryTheory.Sites.CoverLifting Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.CategoryTheory.Sites.Coverage Mathlib.CategoryTheory.Sites.CoversTop Mathlib.CategoryTheory.Sites.Hypercover.Homotopy Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf Mathlib.CategoryTheory.Sites.Hypercover.One Mathlib.CategoryTheory.Sites.Hypercover.Saturate Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical Mathlib.CategoryTheory.Sites.Limits Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.MorphismProperty Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.Sheaf Mathlib.CategoryTheory.Sites.Sheafification Mathlib.CategoryTheory.Sites.Subcanonical Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Sites.Whiskering Mathlib.CategoryTheory.Triangulated.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Triangle Mathlib.CategoryTheory.Triangulated.Rotate Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.AP.Three.Defs Mathlib.Combinatorics.Additive.Corner.Defs Mathlib.Combinatorics.Additive.Dissociation Mathlib.Combinatorics.Additive.FreimanHom Mathlib.Combinatorics.Enumerative.DoubleCounting Mathlib.Combinatorics.Pigeonhole Mathlib.Combinatorics.SetFamily.Shatter Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise Mathlib.Data.DFinsupp.BigOperators Mathlib.Data.DFinsupp.Multiset Mathlib.Data.DFinsupp.Small Mathlib.Data.DFinsupp.Submonoid Mathlib.Data.ENat.BigOperators Mathlib.Data.Finset.Slice Mathlib.Data.Finset.Sym Mathlib.Data.Finsupp.AList Mathlib.Data.Finsupp.Antidiagonal Mathlib.Data.Finsupp.Basic Mathlib.Data.Finsupp.BigOperators Mathlib.Data.Finsupp.Encodable Mathlib.Data.Finsupp.Lex Mathlib.Data.Finsupp.MonomialOrder.DegLex Mathlib.Data.Finsupp.MonomialOrder Mathlib.Data.Finsupp.Multiset Mathlib.Data.Finsupp.Option Mathlib.Data.Finsupp.Order Mathlib.Data.Finsupp.PointwiseSMul Mathlib.Data.Finsupp.SMul Mathlib.Data.Finsupp.Sigma Mathlib.Data.Finsupp.ToDFinsupp Mathlib.Data.Finsupp.Weight Mathlib.Data.Finsupp.WellFounded Mathlib.Data.Int.Fib.Basic Mathlib.Data.Int.Fib.Lemmas Mathlib.Data.Nat.Factorial.BigOperators Mathlib.Data.Nat.Factorization.Basic Mathlib.Data.Nat.Factorization.Defs Mathlib.Data.Nat.Factorization.Induction Mathlib.Data.Nat.Factorization.LCM Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.Nat.Factorization.Root Mathlib.Data.Nat.Fib.Basic Mathlib.Data.Nat.Fib.Zeckendorf Mathlib.Data.Setoid.Partition Mathlib.Data.Sym.Sym2.Finsupp Mathlib.Dynamics.Ergodic.Conservative Mathlib.FieldTheory.Galois.Notation Mathlib.GroupTheory.MonoidLocalization.Away Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero Mathlib.GroupTheory.Perm.ClosureSwap Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.LinearAlgebra.Basis.Bilinear Mathlib.LinearAlgebra.Basis.Defs Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.LinearAlgebra.BilinearMap Mathlib.LinearAlgebra.ConvexSpace Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.Dual.Basis Mathlib.LinearAlgebra.Dual.Defs Mathlib.LinearAlgebra.Finsupp.Defs Mathlib.LinearAlgebra.Finsupp.LSum Mathlib.LinearAlgebra.Finsupp.LinearCombination Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.Finsupp.Span Mathlib.LinearAlgebra.Finsupp.SumProd Mathlib.LinearAlgebra.Finsupp.Supported Mathlib.LinearAlgebra.Goursat Mathlib.LinearAlgebra.LeftExact Mathlib.LinearAlgebra.LinearIndependent.Defs Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Prod Mathlib.LinearAlgebra.Projection Mathlib.LinearAlgebra.Quotient.Basic Mathlib.LinearAlgebra.Quotient.Pi Mathlib.LinearAlgebra.Span.Basic Mathlib.LinearAlgebra.Span.Defs Mathlib.LinearAlgebra.TensorProduct.Associator Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.LinearAlgebra.TensorProduct.Defs Mathlib.LinearAlgebra.TensorProduct.Map Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.Logic.Hydra Mathlib.MeasureTheory.Constructions.AddChar Mathlib.NumberTheory.ClassNumber.AdmissibleAbs Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.NumberTheory.ClassNumber.Finite Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Divisors Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.Order.Filter.AtTopBot.BigOperators Mathlib.Order.Partition.Equipartition Mathlib.Order.Partition.Finpartition Mathlib.RingTheory.ChainOfDivisors Mathlib.RingTheory.Coprime.Lemmas Mathlib.RingTheory.HahnSeries.Addition Mathlib.RingTheory.Ideal.Lattice Mathlib.RingTheory.Ideal.Maximal Mathlib.RingTheory.Ideal.Nonunits Mathlib.RingTheory.Ideal.Prime Mathlib.RingTheory.Ideal.Span Mathlib.RingTheory.LocalRing.Basic Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.RingTheory.LocalRing.Subring Mathlib.RingTheory.NonUnitalSubring.Basic Mathlib.RingTheory.SimpleRing.Congr Mathlib.RingTheory.SimpleRing.Field Mathlib.RingTheory.Spectrum.Maximal.Basic Mathlib.RingTheory.Spectrum.Maximal.Defs Mathlib.RingTheory.Spectrum.Prime.Defs Mathlib.RingTheory.TwoSidedIdeal.Operations Mathlib.RingTheory.UniqueFactorizationDomain.Basic Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.RingTheory.UniqueFactorizationDomain.Finite Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity Mathlib.RingTheory.UniqueFactorizationDomain.Nat Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors Mathlib.Tactic.Algebraize Mathlib.Tactic.Module Mathlib.Tactic.NormNum.IsCoprime Mathlib.Tactic.NormNum.NatFib Mathlib.Tactic.Simproc.Divisors	1
9 files Mathlib.Algebra.Group.Pointwise.Set.BigOperators Mathlib.Algebra.Order.BigOperators.Group.Finset Mathlib.Algebra.Order.Interval.Basic Mathlib.Algebra.Order.Rearrangement Mathlib.Data.Multiset.Fintype Mathlib.Data.NNRat.BigOperators Mathlib.Data.Set.Equitable Mathlib.GroupTheory.Perm.List Mathlib.GroupTheory.Perm.Support	6
15 files Mathlib.Algebra.BigOperators.Pi Mathlib.Algebra.Group.Submonoid.BigOperators Mathlib.Algebra.Group.Translate Mathlib.Algebra.Module.Submodule.Basic Mathlib.Algebra.Star.Conjneg Mathlib.CategoryTheory.Center.Linear Mathlib.CategoryTheory.Center.Preadditive Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Localization.Preadditive Mathlib.CategoryTheory.Preadditive.FunctorCategory Mathlib.Data.Finset.NoncommProd Mathlib.GroupTheory.MonoidLocalization.Lemmas Mathlib.NumberTheory.Padics.PadicVal.Defs Mathlib.RingTheory.Ideal.BigOperators Mathlib.RingTheory.UniqueFactorizationDomain.Defs	7
3 files Mathlib.Algebra.GradedMonoid Mathlib.Algebra.GradedMulAction Mathlib.RingTheory.FilteredAlgebra.Basic	8
Mathlib.RingTheory.Multiplicity	16
6 files Mathlib.Algebra.BigOperators.Group.Finset.Powerset Mathlib.Algebra.BigOperators.Group.Finset.Sigma Mathlib.Algebra.Order.Archimedean.Class Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset Mathlib.Data.Holor Mathlib.Data.Nat.Factorial.DoubleFactorial	19
17 files Mathlib.Algebra.BigOperators.Group.Finset.Basic Mathlib.Algebra.BigOperators.Group.Finset.Indicator Mathlib.Algebra.BigOperators.Group.Finset.Lemmas Mathlib.Algebra.BigOperators.Group.Finset.Piecewise Mathlib.Algebra.BigOperators.GroupWithZero.Finset Mathlib.Algebra.BigOperators.Option Mathlib.Algebra.BigOperators.WithTop Mathlib.Algebra.Group.EvenFunction Mathlib.Dynamics.BirkhoffSum.Average Mathlib.Dynamics.BirkhoffSum.Basic Mathlib.GroupTheory.MonoidLocalization.Basic Mathlib.GroupTheory.MonoidLocalization.DivPairs Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup Mathlib.GroupTheory.MonoidLocalization.Maps Mathlib.GroupTheory.MonoidLocalization.Order Mathlib.NumberTheory.Harmonic.Defs Mathlib.RingTheory.Prime	20

---

Declarations diff

+ exists_lt_card_cover_of_card_biUnion_lt_card
+ sum_card_eq_sum_card_cover_biUnion

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).