Commit 2023-06-19 13:10 5ed7d916

View on Github →

chore: add @[ext] lemmas for NatTrans synonyms (#5228)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Tannaka.lean

Modified Mathlib/AlgebraicGeometry/PresheafedSpace.lean

Modified Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/AlgebraicGeometry/Stalks.lean

Modified Mathlib/AlgebraicTopology/Nerve.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet.lean

added theorem SSet.Truncated.hom_ext

added theorem SSet.hom_ext

modified def SSet.hornInclusion

Modified Mathlib/CategoryTheory/Limits/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Localization/Construction.lean

Modified Mathlib/CategoryTheory/Localization/Predicate.lean

Modified Mathlib/CategoryTheory/MorphismProperty.lean

added theorem CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext

Modified Mathlib/CategoryTheory/Whiskering.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

added theorem CategoryTheory.yonedaPairingExt

Modified Mathlib/Topology/Sheaves/Presheaf.lean

added theorem TopCat.Presheaf.ext