Commit 2026-02-11 19:24 d6c9e7aa

View on Github →

feat: some finset lemmas (#13686)

From the Sobolev inequality project
The increase in imports in Mathlib.Data.Finset.Update is not problematic: it is only imported in MeasureTheory files.
Add DepRewrite to Tactic.Common.
Change the normal form of {x} ∪ {y} to {x, y} (previously {y, x}).

Estimated changes

Modified Mathlib/Algebra/Group/Finsupp.lean

Modified Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

Modified Mathlib/Data/Finset/Basic.lean

added theorem Equiv.Finset.union_inl

added theorem Equiv.Finset.union_inr

deleted theorem Equiv.Finset.union_symm_inl

deleted theorem Equiv.Finset.union_symm_inr

added theorem Equiv.Finset.union_symm_left

added theorem Equiv.Finset.union_symm_right

added theorem Equiv.piFinsetUnion_left

added theorem Equiv.piFinsetUnion_right

Modified Mathlib/Data/Finset/Lattice/Lemmas.lean

Modified Mathlib/Data/Finset/Update.lean

added theorem Function.updateFinset_congr

modified theorem Function.updateFinset_def

modified theorem Function.updateFinset_singleton

added theorem Function.updateFinset_univ

added theorem Function.updateFinset_univ_apply

modified theorem Function.updateFinset_updateFinset

modified theorem Function.update_eq_updateFinset

added theorem Function.update_updateFinset

Modified Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean

Modified Mathlib/Tactic/Common.lean