Commit 2024-06-26 12:43 90b77f05

View on Github →

chore: Rename Equiv.forall_congr lemmas (#13725) These names were all over the place and there were missing versions.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

Modified Mathlib/Combinatorics/Additive/Dissociation.lean

Modified Mathlib/Combinatorics/HalesJewett.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/Nat/Factorization/PrimePow.lean

Modified Mathlib/Data/Set/Prod.lean

Modified Mathlib/Geometry/Manifold/Diffeomorph.lean

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/Init/Logic.lean

added theorem existsUnique_congr

deleted theorem exists_unique_congr

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/Topology/Homeomorph.lean

Modified Mathlib/Topology/UniformSpace/Equiv.lean