Commit 2023-06-09 07:23 5b958613

View on Github →

chore: review of automation in category theory (#4793) Clean up of automation in the category theory library. Leaving out unnecessary proof steps, or fields done by aesop_cat, and making more use of available autoparameters.

Estimated changes

Modified Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.lean

Modified Mathlib/Algebra/Category/GroupCat/Limits.lean

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

Modified Mathlib/Algebra/Homology/Additive.lean

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

Modified Mathlib/Algebra/Homology/Opposite.lean

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

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

Modified Mathlib/Algebra/Homology/ShortExact/Abelian.lean

Modified Mathlib/Algebra/Homology/Single.lean

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

Modified Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean

Modified Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.lean

added def FundamentalGroupoid.punitEquivDiscretePUnit

deleted def FundamentalGroupoid.punitEquivDiscretePunit

Modified Mathlib/AlgebraicTopology/SimplicialObject.lean

Modified Mathlib/CategoryTheory/Adjunction/Basic.lean

Modified Mathlib/CategoryTheory/Adjunction/Comma.lean

Modified Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

Modified Mathlib/CategoryTheory/Adjunction/Limits.lean

modified def CategoryTheory.Adjunction.functorialityIsLeftAdjoint

modified def CategoryTheory.Adjunction.functorialityIsRightAdjoint

modified def CategoryTheory.Adjunction.leftAdjointPreservesColimits

modified def CategoryTheory.Adjunction.rightAdjointPreservesLimits

Modified Mathlib/CategoryTheory/Adjunction/Opposites.lean

Modified Mathlib/CategoryTheory/Arrow.lean

Modified Mathlib/CategoryTheory/Bicategory/End.lean

Modified Mathlib/CategoryTheory/Bicategory/Free.lean

Modified Mathlib/CategoryTheory/Bicategory/SingleObj.lean

Modified Mathlib/CategoryTheory/Category/Bipointed.lean

Modified Mathlib/CategoryTheory/Category/Cat.lean

Modified Mathlib/CategoryTheory/Category/Cat/Limit.lean

modified def CategoryTheory.Cat.HasLimits.limitCone

modified def CategoryTheory.Cat.HasLimits.limitConeLift

Modified Mathlib/CategoryTheory/Category/Pairwise.lean

added def CategoryTheory.Pairwise.pairwiseCases

Modified Mathlib/CategoryTheory/Category/TwoP.lean

Modified Mathlib/CategoryTheory/Category/ULift.lean

Modified Mathlib/CategoryTheory/Closed/Monoidal.lean

modified def CategoryTheory.unitClosed

Modified Mathlib/CategoryTheory/Comma.lean

modified def CategoryTheory.Comma.mapLeft

modified def CategoryTheory.Comma.mapLeftComp

modified def CategoryTheory.Comma.mapLeftId

modified def CategoryTheory.Comma.mapRight

modified def CategoryTheory.Comma.mapRightComp

modified def CategoryTheory.Comma.mapRightId

modified def CategoryTheory.Comma.post

modified def CategoryTheory.Comma.preLeft

modified def CategoryTheory.Comma.preRight

Modified Mathlib/CategoryTheory/DiscreteCategory.lean

Modified Mathlib/CategoryTheory/Elements.lean

Modified Mathlib/CategoryTheory/Endofunctor/Algebra.lean

added theorem CategoryTheory.Endofunctor.Algebra.ext

modified def CategoryTheory.Endofunctor.Algebra.isoMk

added theorem CategoryTheory.Endofunctor.Coalgebra.ext

modified def CategoryTheory.Endofunctor.Coalgebra.isoMk

Modified Mathlib/CategoryTheory/EqToHom.lean

Modified Mathlib/CategoryTheory/Equivalence.lean

Modified Mathlib/CategoryTheory/EssentiallySmall.lean

Modified Mathlib/CategoryTheory/FinCategory.lean

Modified Mathlib/CategoryTheory/FullSubcategory.lean

Modified Mathlib/CategoryTheory/Functor/Currying.lean

Modified Mathlib/CategoryTheory/Functor/Flat.lean

Modified Mathlib/CategoryTheory/Functor/Hom.lean

Modified Mathlib/CategoryTheory/GlueData.lean

Modified Mathlib/CategoryTheory/GradedObject.lean

Modified Mathlib/CategoryTheory/Groupoid.lean

Modified Mathlib/CategoryTheory/Idempotents/HomologicalComplex.lean

Modified Mathlib/CategoryTheory/Idempotents/Karoubi.lean

Modified Mathlib/CategoryTheory/IsConnected.lean

Modified Mathlib/CategoryTheory/Limits/ConeCategory.lean

Modified Mathlib/CategoryTheory/Limits/Cones.lean

modified def CategoryTheory.Limits.Cocones.ext

modified def CategoryTheory.Limits.Cones.ext

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

Modified Mathlib/CategoryTheory/Limits/Creates.lean

Modified Mathlib/CategoryTheory/Limits/Final.lean

Modified Mathlib/CategoryTheory/Limits/Fubini.lean

Modified Mathlib/CategoryTheory/Limits/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

modified def CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom

modified def CategoryTheory.Limits.IsColimit.equivIsoColimit

modified def CategoryTheory.Limits.IsLimit.equivIsoLimit

modified def CategoryTheory.Limits.IsLimit.natIso

Modified Mathlib/CategoryTheory/Limits/Over.lean

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

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

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

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

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

modified def CategoryTheory.Limits.Cofork.ext

modified def CategoryTheory.Limits.Fork.ext

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

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

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

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

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

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

modified def CategoryTheory.Limits.Cotrident.ext

modified def CategoryTheory.Limits.Cotrident.mkHom

modified def CategoryTheory.Limits.Trident.ext

modified def CategoryTheory.Limits.Trident.mkHom

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

Modified Mathlib/CategoryTheory/Limits/Yoneda.lean

Modified Mathlib/CategoryTheory/Monad/Adjunction.lean

Modified Mathlib/CategoryTheory/Monad/Algebra.lean

modified def CategoryTheory.Comonad.Coalgebra.isoMk

modified def CategoryTheory.Monad.Algebra.isoMk

Modified Mathlib/CategoryTheory/Monad/Basic.lean

Modified Mathlib/CategoryTheory/Monad/Kleisli.lean

Modified Mathlib/CategoryTheory/Monad/Limits.lean

Modified Mathlib/CategoryTheory/Monad/Products.lean

Modified Mathlib/CategoryTheory/Monad/Types.lean

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

Modified Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Monoidal/Preadditive.lean

Modified Mathlib/CategoryTheory/NatIso.lean

Modified Mathlib/CategoryTheory/Opposites.lean

Modified Mathlib/CategoryTheory/Over.lean

modified def CategoryTheory.Under.isoMk

Modified Mathlib/CategoryTheory/PEmpty.lean

Modified Mathlib/CategoryTheory/PUnit.lean

modified def CategoryTheory.Functor.pUnitExt

modified theorem CategoryTheory.Functor.pUnit_ext'

Modified Mathlib/CategoryTheory/Pi/Basic.lean

Modified Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean

Modified Mathlib/CategoryTheory/Products/Associator.lean

Modified Mathlib/CategoryTheory/Products/Basic.lean

modified def CategoryTheory.Functor.prod'

modified def CategoryTheory.Functor.prod

modified def CategoryTheory.evaluation

modified def CategoryTheory.evaluationUncurried

Modified Mathlib/CategoryTheory/Quotient.lean

Modified Mathlib/CategoryTheory/Sigma/Basic.lean

Modified Mathlib/CategoryTheory/SingleObj.lean

modified def CategoryTheory.SingleObj.mapHom

Modified Mathlib/CategoryTheory/Sites/CoverLifting.lean

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

Modified Mathlib/CategoryTheory/Sites/Plus.lean

Modified Mathlib/CategoryTheory/Sites/Pushforward.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

Modified Mathlib/CategoryTheory/Sites/Sheafification.lean

Modified Mathlib/CategoryTheory/Skeletal.lean

Modified Mathlib/CategoryTheory/StructuredArrow.lean

modified def CategoryTheory.CostructuredArrow.homMk

modified def CategoryTheory.CostructuredArrow.isoMk

modified def CategoryTheory.StructuredArrow.homMk

modified def CategoryTheory.StructuredArrow.isoMk

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

Modified Mathlib/CategoryTheory/Subobject/Lattice.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

modified def CategoryTheory.MonoOver.isoMk

Modified Mathlib/CategoryTheory/Subobject/Types.lean

Modified Mathlib/CategoryTheory/Subterminal.lean

Modified Mathlib/CategoryTheory/Sums/Basic.lean

modified def CategoryTheory.Sum.swap

Modified Mathlib/CategoryTheory/Triangulated/Basic.lean

Modified Mathlib/CategoryTheory/Triangulated/Rotate.lean

Modified Mathlib/CategoryTheory/Triangulated/Triangulated.lean

Modified Mathlib/CategoryTheory/Types.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

Modified Mathlib/Order/Category/DistLatCat.lean

Modified Mathlib/Order/Category/FinPartOrd.lean

Modified Mathlib/Order/Category/LatCat.lean

Modified Mathlib/Order/Category/LinOrdCat.lean

Modified Mathlib/Order/Category/NonemptyFinLinOrdCat.lean

Modified Mathlib/Order/Category/PartOrdCat.lean

Modified Mathlib/Order/Category/PreordCat.lean

Modified Mathlib/RepresentationTheory/Action.lean

modified def Action.mkIso

Modified Mathlib/Topology/Category/Compactum.lean

Modified Mathlib/Topology/Category/TopCat/OpenNhds.lean

Modified Mathlib/Topology/Category/TopCat/Opens.lean

Modified Mathlib/Topology/Sheaves/Limits.lean

Modified Mathlib/Topology/Sheaves/LocalPredicate.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean