Commit 2025-02-11 15:35 b1c343ee

View on Github →

refactor(*): get rid of last HasForget.instFunLike instances (#21725) This PR should get rid of the last lines of the form:

attribute [local instance] HasForget.instFunLike HasForget.hasCoeToSort

anywhere in Mathlib. A few places provided some nice cleanup opportunities. There are still quite some (forget _).obj and (forget _).map calls remaining, I'll tackle those in a follow up PR.

Estimated changes

Modified Mathlib/Algebra/Homology/ConcreteCategory.lean

Modified Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean

modified theorem CategoryTheory.ShortComplex.SnakeInput.δ_apply

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

deleted theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply'

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

added theorem CategoryTheory.ConcreteCategory.forget₂_comp_apply

Modified Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean

Modified Mathlib/CategoryTheory/Galois/Examples.lean

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean

modified theorem CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq

modified theorem CategoryTheory.Limits.Concrete.colimit_exists_rep

modified theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists

modified theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists

modified theorem CategoryTheory.Limits.Concrete.isColimit_exists_rep

modified theorem CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists

modified theorem CategoryTheory.Limits.Concrete.isLimit_ext

modified theorem CategoryTheory.Limits.Concrete.limit_ext

modified theorem CategoryTheory.Limits.Concrete.surjective_π_app_zero_of_surjective_map

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory/WithAlgebraicStructures.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean

modified theorem CategoryTheory.Limits.Concrete.Pi.map_ext

modified theorem CategoryTheory.Limits.Concrete.cokernel_funext

modified theorem CategoryTheory.Limits.Concrete.prodEquiv_apply_fst

modified theorem CategoryTheory.Limits.Concrete.prodEquiv_apply_snd

modified theorem CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_fst

modified theorem CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_snd

modified theorem CategoryTheory.Limits.Concrete.productEquiv_apply_apply

modified theorem CategoryTheory.Limits.Concrete.productEquiv_symm_apply_π

modified theorem CategoryTheory.Limits.Concrete.pullbackMk_fst

modified theorem CategoryTheory.Limits.Concrete.pullbackMk_snd

modified theorem CategoryTheory.Limits.Concrete.pullbackMk_surjective

Modified Mathlib/CategoryTheory/MorphismProperty/Concrete.lean

Modified Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

Modified Mathlib/Topology/Order/Category/AlexDisc.lean

Modified Mathlib/Topology/Sheaves/CommRingCat.lean