Commit 2025-08-22 13:19 b7307db8

View on Github →

feat: grind annotations in Logic/Equiv/Defs (#28025)

Estimated changes

Modified Mathlib/Logic/Equiv/Array.lean

modified def Equiv.arrayEquivList

Modified Mathlib/Logic/Equiv/Defs.lean

modified theorem Equiv.apply_eq_iff_eq_symm_apply

modified theorem Equiv.arrowCongr'_symm

modified theorem Equiv.arrowCongr_symm

modified def Equiv.arrowPUnitEquivPUnit

modified theorem Equiv.conj_symm

modified theorem Equiv.eq_symm_apply

modified theorem Equiv.equivCongr_apply_apply

modified theorem Equiv.equivCongr_symm

modified theorem Equiv.ext

modified theorem Equiv.permCongr_apply

modified theorem Equiv.permCongr_symm

modified def Equiv.punitEquivPUnit

modified theorem Equiv.refl_apply

modified theorem Equiv.refl_symm

modified theorem Equiv.self_trans_symm

modified def Equiv.sigmaEquivProd

modified theorem Equiv.symm_apply_eq

modified theorem Equiv.symm_symm

modified theorem Equiv.symm_trans_apply

modified theorem Equiv.symm_trans_self

modified theorem Equiv.trans_apply

modified theorem Equiv.trans_refl

Modified Mathlib/Logic/Equiv/Embedding.lean

Modified Mathlib/Logic/Equiv/Finset.lean

Modified Mathlib/Logic/Equiv/Fintype.lean

modified def Function.Embedding.toEquivRange

Modified Mathlib/Logic/Equiv/Option.lean

Modified Mathlib/Logic/Equiv/Prod.lean

modified def Equiv.prodComm

modified def Equiv.prodPUnit

modified def Equiv.sigmaPUnit

modified def Equiv.uniqueSigma