perf(CategoryTheory): let aesop_cat attempt rfl before aesop

[JovanGerb]

This PR modifies the aesop_cat tactic so that it tries a proof by rfl before doing the more expensive aesop tactic.

This ran into a problem that is discussed here: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/changing.20a.20proof.20can.20break.20a.20later.20proof/near/497313462

The issue is that a proof by rfl doesn't have the same type as the expected type. Starting the proof with refine id ?_` is a trick to make sure that the type matches exactly with the expected type.

---

[github-actions]

PR summary b5bc210b0a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Category.Basic	262	263	+1 (+0.38%)
Mathlib.CategoryTheory.DiscreteCategory	302	303	+1 (+0.33%)
Mathlib.CategoryTheory.Monoidal.Mod_	463	464	+1 (+0.22%)
Mathlib.Algebra.Homology.DifferentialObject	652	653	+1 (+0.15%)
Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover	968	969	+1 (+0.10%)

Import changes for all files

Files

Import difference

720 files Mathlib.Algebra.Category.Grp.Basic Mathlib.Algebra.Category.Grp.Colimits Mathlib.Algebra.Category.Grp.EpiMono Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup Mathlib.Algebra.Category.Grp.FilteredColimits Mathlib.Algebra.Category.Grp.FiniteGrp Mathlib.Algebra.Category.Grp.ForgetCorepresentable Mathlib.Algebra.Category.Grp.Kernels Mathlib.Algebra.Category.Grp.Limits Mathlib.Algebra.Category.Grp.Preadditive Mathlib.Algebra.Category.Grp.Zero Mathlib.Algebra.Category.GrpWithZero Mathlib.Algebra.Category.MonCat.Adjunctions Mathlib.Algebra.Category.MonCat.Basic Mathlib.Algebra.Category.MonCat.Colimits Mathlib.Algebra.Category.MonCat.FilteredColimits Mathlib.Algebra.Category.MonCat.ForgetCorepresentable Mathlib.Algebra.Category.MonCat.Limits Mathlib.Algebra.Category.Ring.Basic Mathlib.Algebra.Category.Ring.Colimits Mathlib.Algebra.Category.Ring.FilteredColimits Mathlib.Algebra.Category.Ring.Limits Mathlib.Algebra.Category.Semigrp.Basic Mathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.ImageToKernel Mathlib.Algebra.Homology.ShortComplex.Basic Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence Mathlib.Algebra.Homology.ShortComplex.Homology Mathlib.Algebra.Homology.ShortComplex.LeftHomology Mathlib.Algebra.Homology.ShortComplex.Limits Mathlib.Algebra.Homology.ShortComplex.PreservesHomology Mathlib.Algebra.Homology.ShortComplex.QuasiIso Mathlib.Algebra.Homology.ShortComplex.Retract Mathlib.Algebra.Homology.ShortComplex.RightHomology Mathlib.Algebra.Homology.Single Mathlib.AlgebraicTopology.CechNerve Mathlib.AlgebraicTopology.DoldKan.Compatibility Mathlib.AlgebraicTopology.ModelCategory.Basic Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.SimplexCategory Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialObject.Basic Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal Mathlib.AlgebraicTopology.SimplicialObject.Split Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.AlgebraicTopology.SimplicialSet.Boundary Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Horn Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.CategoryTheory.Abelian.Images Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.CategoryTheory.Action.Basic Mathlib.CategoryTheory.Action.Continuous Mathlib.CategoryTheory.Adhesive Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Adjunction.Basic Mathlib.CategoryTheory.Adjunction.Comma Mathlib.CategoryTheory.Adjunction.Evaluation Mathlib.CategoryTheory.Adjunction.FullyFaithful Mathlib.CategoryTheory.Adjunction.Lifting.Left Mathlib.CategoryTheory.Adjunction.Lifting.Right Mathlib.CategoryTheory.Adjunction.Limits Mathlib.CategoryTheory.Adjunction.Mates Mathlib.CategoryTheory.Adjunction.Opposites Mathlib.CategoryTheory.Adjunction.Over Mathlib.CategoryTheory.Adjunction.PartialAdjoint Mathlib.CategoryTheory.Adjunction.Reflective Mathlib.CategoryTheory.Adjunction.Restrict Mathlib.CategoryTheory.Adjunction.Triple Mathlib.CategoryTheory.Adjunction.Unique Mathlib.CategoryTheory.Adjunction.Whiskering Mathlib.CategoryTheory.Balanced Mathlib.CategoryTheory.Bicategory.Adjunction.Basic Mathlib.CategoryTheory.Bicategory.Adjunction.Mate Mathlib.CategoryTheory.Bicategory.Basic Mathlib.CategoryTheory.Bicategory.Coherence Mathlib.CategoryTheory.Bicategory.End Mathlib.CategoryTheory.Bicategory.Extension Mathlib.CategoryTheory.Bicategory.Free Mathlib.CategoryTheory.Bicategory.Functor.Lax Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete Mathlib.CategoryTheory.Bicategory.Functor.Oplax Mathlib.CategoryTheory.Bicategory.Functor.Prelax Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax Mathlib.CategoryTheory.Bicategory.Grothendieck Mathlib.CategoryTheory.Bicategory.Kan.Adjunction Mathlib.CategoryTheory.Bicategory.Kan.HasKan Mathlib.CategoryTheory.Bicategory.Kan.IsKan Mathlib.CategoryTheory.Bicategory.LocallyDiscrete Mathlib.CategoryTheory.Bicategory.Modification.Oplax Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Strong Mathlib.CategoryTheory.Bicategory.SingleObj Mathlib.CategoryTheory.Bicategory.Strict Mathlib.CategoryTheory.CatCommSq Mathlib.CategoryTheory.Category.Basic Mathlib.CategoryTheory.Category.Bipointed Mathlib.CategoryTheory.Category.Cat.Adjunction Mathlib.CategoryTheory.Category.Cat.AsSmall Mathlib.CategoryTheory.Category.Cat.Limit Mathlib.CategoryTheory.Category.Cat Mathlib.CategoryTheory.Category.Factorisation Mathlib.CategoryTheory.Category.GaloisConnection Mathlib.CategoryTheory.Category.Grpd Mathlib.CategoryTheory.Category.KleisliCat Mathlib.CategoryTheory.Category.Pairwise Mathlib.CategoryTheory.Category.PartialFun Mathlib.CategoryTheory.Category.Pointed Mathlib.CategoryTheory.Category.Preorder Mathlib.CategoryTheory.Category.Quiv Mathlib.CategoryTheory.Category.ReflQuiv Mathlib.CategoryTheory.Category.RelCat Mathlib.CategoryTheory.Category.TwoP Mathlib.CategoryTheory.Category.ULift Mathlib.CategoryTheory.ChosenFiniteProducts.Cat Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory Mathlib.CategoryTheory.ChosenFiniteProducts.InfSemilattice Mathlib.CategoryTheory.ChosenFiniteProducts Mathlib.CategoryTheory.Closed.Cartesian Mathlib.CategoryTheory.Closed.Enrichment Mathlib.CategoryTheory.Closed.FunctorCategory.Complete Mathlib.CategoryTheory.Closed.FunctorCategory.Groupoid Mathlib.CategoryTheory.Closed.FunctorToTypes Mathlib.CategoryTheory.Closed.Functor Mathlib.CategoryTheory.Closed.Ideal Mathlib.CategoryTheory.Closed.Monoidal Mathlib.CategoryTheory.Closed.Types Mathlib.CategoryTheory.Closed.Zero Mathlib.CategoryTheory.ClosedUnderIsomorphisms Mathlib.CategoryTheory.CodiscreteCategory Mathlib.CategoryTheory.CofilteredSystem Mathlib.CategoryTheory.CommSq Mathlib.CategoryTheory.Comma.Arrow Mathlib.CategoryTheory.Comma.Basic Mathlib.CategoryTheory.Comma.CardinalArrow Mathlib.CategoryTheory.Comma.Final Mathlib.CategoryTheory.Comma.LocallySmall Mathlib.CategoryTheory.Comma.OverClass Mathlib.CategoryTheory.Comma.Over Mathlib.CategoryTheory.Comma.Presheaf.Basic Mathlib.CategoryTheory.Comma.Presheaf.Colimit Mathlib.CategoryTheory.Comma.StructuredArrow.Basic Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap Mathlib.CategoryTheory.Comma.StructuredArrow.Functor Mathlib.CategoryTheory.Comma.StructuredArrow.Small Mathlib.CategoryTheory.ComposableArrows Mathlib.CategoryTheory.ConcreteCategory.Basic Mathlib.CategoryTheory.ConcreteCategory.BundledHom Mathlib.CategoryTheory.ConcreteCategory.Elementwise Mathlib.CategoryTheory.ConcreteCategory.EpiMono Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso Mathlib.CategoryTheory.ConcreteCategory.UnbundledHom Mathlib.CategoryTheory.Conj Mathlib.CategoryTheory.ConnectedComponents Mathlib.CategoryTheory.Core Mathlib.CategoryTheory.Countable Mathlib.CategoryTheory.Dialectica.Basic Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.DifferentialObject Mathlib.CategoryTheory.DiscreteCategory Mathlib.CategoryTheory.EffectiveEpi.Basic Mathlib.CategoryTheory.EffectiveEpi.Comp Mathlib.CategoryTheory.EffectiveEpi.Coproduct Mathlib.CategoryTheory.EffectiveEpi.Enough Mathlib.CategoryTheory.EffectiveEpi.Extensive Mathlib.CategoryTheory.EffectiveEpi.Preserves Mathlib.CategoryTheory.EffectiveEpi.RegularEpi Mathlib.CategoryTheory.Elements Mathlib.CategoryTheory.Elementwise Mathlib.CategoryTheory.Endofunctor.Algebra Mathlib.CategoryTheory.Endomorphism Mathlib.CategoryTheory.Enriched.Basic Mathlib.CategoryTheory.Enriched.FunctorCategory Mathlib.CategoryTheory.Enriched.HomCongr Mathlib.CategoryTheory.Enriched.Opposite Mathlib.CategoryTheory.Enriched.Ordinary.Basic Mathlib.CategoryTheory.EpiMono Mathlib.CategoryTheory.EqToHom Mathlib.CategoryTheory.Equivalence Mathlib.CategoryTheory.EssentialImage Mathlib.CategoryTheory.EssentiallySmall Mathlib.CategoryTheory.Extensive Mathlib.CategoryTheory.FiberedCategory.BasedCategory Mathlib.CategoryTheory.FiberedCategory.Cartesian Mathlib.CategoryTheory.FiberedCategory.Cocartesian Mathlib.CategoryTheory.FiberedCategory.Fiber Mathlib.CategoryTheory.FiberedCategory.Fibered Mathlib.CategoryTheory.FiberedCategory.HomLift Mathlib.CategoryTheory.Filtered.Basic Mathlib.CategoryTheory.Filtered.Connected Mathlib.CategoryTheory.Filtered.CostructuredArrow Mathlib.CategoryTheory.Filtered.Final Mathlib.CategoryTheory.Filtered.Flat Mathlib.CategoryTheory.Filtered.Grothendieck Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit Mathlib.CategoryTheory.Filtered.Small Mathlib.CategoryTheory.FinCategory.AsType Mathlib.CategoryTheory.FinCategory.Basic Mathlib.CategoryTheory.FintypeCat Mathlib.CategoryTheory.FullSubcategory Mathlib.CategoryTheory.Functor.Basic Mathlib.CategoryTheory.Functor.Category Mathlib.CategoryTheory.Functor.Const Mathlib.CategoryTheory.Functor.CurryingThree Mathlib.CategoryTheory.Functor.Currying Mathlib.CategoryTheory.Functor.Derived.RightDerived Mathlib.CategoryTheory.Functor.EpiMono Mathlib.CategoryTheory.Functor.Flat Mathlib.CategoryTheory.Functor.FullyFaithful Mathlib.CategoryTheory.Functor.FunctorHom Mathlib.CategoryTheory.Functor.Functorial Mathlib.CategoryTheory.Functor.Hom Mathlib.CategoryTheory.Functor.KanExtension.Adjunction Mathlib.CategoryTheory.Functor.KanExtension.Basic Mathlib.CategoryTheory.Functor.KanExtension.Pointwise Mathlib.CategoryTheory.Functor.OfSequence Mathlib.CategoryTheory.Functor.ReflectsIso Mathlib.CategoryTheory.Functor.Trifunctor Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Galois.Decomposition Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.GlueData Mathlib.CategoryTheory.GradedObject.Associator Mathlib.CategoryTheory.GradedObject.Bifunctor Mathlib.CategoryTheory.GradedObject.Braiding Mathlib.CategoryTheory.GradedObject.Monoidal Mathlib.CategoryTheory.GradedObject.Single Mathlib.CategoryTheory.GradedObject.Trifunctor Mathlib.CategoryTheory.GradedObject.Unitor Mathlib.CategoryTheory.GradedObject Mathlib.CategoryTheory.Grothendieck Mathlib.CategoryTheory.Groupoid.Basic Mathlib.CategoryTheory.Groupoid.Discrete Mathlib.CategoryTheory.Groupoid.FreeGroupoid Mathlib.CategoryTheory.Groupoid.Subgroupoid Mathlib.CategoryTheory.Groupoid.VertexGroup Mathlib.CategoryTheory.Groupoid Mathlib.CategoryTheory.GuitartExact.Basic Mathlib.CategoryTheory.GuitartExact.VerticalComposition Mathlib.CategoryTheory.HomCongr Mathlib.CategoryTheory.IsConnected Mathlib.CategoryTheory.Iso Mathlib.CategoryTheory.IsomorphismClasses Mathlib.CategoryTheory.LiftingProperties.Adjunction Mathlib.CategoryTheory.LiftingProperties.Basic Mathlib.CategoryTheory.LiftingProperties.Limits Mathlib.CategoryTheory.Limits.Bicones Mathlib.CategoryTheory.Limits.ColimitLimit Mathlib.CategoryTheory.Limits.Comma Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic Mathlib.CategoryTheory.Limits.ConeCategory Mathlib.CategoryTheory.Limits.Cones Mathlib.CategoryTheory.Limits.Connected Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts Mathlib.CategoryTheory.Limits.Constructions.EpiMono Mathlib.CategoryTheory.Limits.Constructions.Equalizers Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant Mathlib.CategoryTheory.Limits.Constructions.Filtered Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers Mathlib.CategoryTheory.Limits.Constructions.Over.Basic Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Limits.Constructions.Over.Products Mathlib.CategoryTheory.Limits.Constructions.Pullbacks Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects Mathlib.CategoryTheory.Limits.Creates Mathlib.CategoryTheory.Limits.Elements Mathlib.CategoryTheory.Limits.EpiMono Mathlib.CategoryTheory.Limits.EssentiallySmall Mathlib.CategoryTheory.Limits.ExactFunctor Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct Mathlib.CategoryTheory.Limits.Filtered Mathlib.CategoryTheory.Limits.Final.ParallelPair Mathlib.CategoryTheory.Limits.Final Mathlib.CategoryTheory.Limits.FinallySmall Mathlib.CategoryTheory.Limits.FintypeCat Mathlib.CategoryTheory.Limits.Fubini Mathlib.CategoryTheory.Limits.FullSubcategory Mathlib.CategoryTheory.Limits.FunctorCategory.Basic Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered Mathlib.CategoryTheory.Limits.FunctorCategory.Finite Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products Mathlib.CategoryTheory.Limits.FunctorToTypes Mathlib.CategoryTheory.Limits.HasLimits Mathlib.CategoryTheory.Limits.IndYoneda Mathlib.CategoryTheory.Limits.Indization.Category Mathlib.CategoryTheory.Limits.Indization.Equalizers Mathlib.CategoryTheory.Limits.Indization.FilteredColimits Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Limits.Indization.LocallySmall Mathlib.CategoryTheory.Limits.Indization.ParallelPair Mathlib.CategoryTheory.Limits.Indization.Products Mathlib.CategoryTheory.Limits.IsConnected Mathlib.CategoryTheory.Limits.IsLimit Mathlib.CategoryTheory.Limits.Lattice Mathlib.CategoryTheory.Limits.MonoCoprod Mathlib.CategoryTheory.Limits.MorphismProperty Mathlib.CategoryTheory.Limits.Opposites Mathlib.CategoryTheory.Limits.Over Mathlib.CategoryTheory.Limits.Pi Mathlib.CategoryTheory.Limits.Preorder Mathlib.CategoryTheory.Limits.Preserves.Basic Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite Mathlib.CategoryTheory.Limits.Preserves.Filtered Mathlib.CategoryTheory.Limits.Preserves.Finite Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory Mathlib.CategoryTheory.Limits.Preserves.Grothendieck Mathlib.CategoryTheory.Limits.Preserves.Limits Mathlib.CategoryTheory.Limits.Preserves.Opposites Mathlib.CategoryTheory.Limits.Preserves.Presheaf Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero Mathlib.CategoryTheory.Limits.Preserves.Ulift Mathlib.CategoryTheory.Limits.Preserves.Yoneda Mathlib.CategoryTheory.Limits.Presheaf Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts Mathlib.CategoryTheory.Limits.Shapes.Biproducts Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory Mathlib.CategoryTheory.Limits.Shapes.Connected Mathlib.CategoryTheory.Limits.Shapes.Countable Mathlib.CategoryTheory.Limits.Shapes.Diagonal Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct Mathlib.CategoryTheory.Limits.Shapes.End Mathlib.CategoryTheory.Limits.Shapes.Equalizers Mathlib.CategoryTheory.Limits.Shapes.Equivalence Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes Mathlib.CategoryTheory.Limits.Shapes.Grothendieck Mathlib.CategoryTheory.Limits.Shapes.Images Mathlib.CategoryTheory.Limits.Shapes.IsTerminal Mathlib.CategoryTheory.Limits.Shapes.KernelPair Mathlib.CategoryTheory.Limits.Shapes.Kernels Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers Mathlib.CategoryTheory.Limits.Shapes.PiProd Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous Mathlib.CategoryTheory.Limits.Shapes.Products Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square Mathlib.CategoryTheory.Limits.Shapes.Reflexive Mathlib.CategoryTheory.Limits.Shapes.RegularMono Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct Mathlib.CategoryTheory.Limits.Shapes.SingleObj Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer Mathlib.CategoryTheory.Limits.Shapes.StrictInitial Mathlib.CategoryTheory.Limits.Shapes.StrongEpi Mathlib.CategoryTheory.Limits.Shapes.Terminal Mathlib.CategoryTheory.Limits.Shapes.Types Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects Mathlib.CategoryTheory.Limits.Sifted Mathlib.CategoryTheory.Limits.SmallComplete Mathlib.CategoryTheory.Limits.TypesFiltered Mathlib.CategoryTheory.Limits.Types Mathlib.CategoryTheory.Limits.Unit Mathlib.CategoryTheory.Limits.VanKampen Mathlib.CategoryTheory.Limits.Yoneda Mathlib.CategoryTheory.Linear.Basic Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Localization.Adjunction Mathlib.CategoryTheory.Localization.Bifunctor Mathlib.CategoryTheory.Localization.Bousfield Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions Mathlib.CategoryTheory.Localization.CalculusOfFractions Mathlib.CategoryTheory.Localization.Composition Mathlib.CategoryTheory.Localization.Construction Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor Mathlib.CategoryTheory.Localization.Equivalence Mathlib.CategoryTheory.Localization.FiniteProducts Mathlib.CategoryTheory.Localization.HasLocalization Mathlib.CategoryTheory.Localization.HomEquiv Mathlib.CategoryTheory.Localization.LocalizerMorphism Mathlib.CategoryTheory.Localization.LocallySmall Mathlib.CategoryTheory.Localization.Monoidal Mathlib.CategoryTheory.Localization.Opposite Mathlib.CategoryTheory.Localization.Pi Mathlib.CategoryTheory.Localization.Predicate Mathlib.CategoryTheory.Localization.Prod Mathlib.CategoryTheory.Localization.Resolution Mathlib.CategoryTheory.Localization.SmallHom Mathlib.CategoryTheory.Localization.StructuredArrow Mathlib.CategoryTheory.Localization.Trifunctor Mathlib.CategoryTheory.Monad.Adjunction Mathlib.CategoryTheory.Monad.Algebra Mathlib.CategoryTheory.Monad.Basic Mathlib.CategoryTheory.Monad.Coequalizer Mathlib.CategoryTheory.Monad.Comonadicity Mathlib.CategoryTheory.Monad.Equalizer Mathlib.CategoryTheory.Monad.EquivMon Mathlib.CategoryTheory.Monad.Kleisli Mathlib.CategoryTheory.Monad.Limits Mathlib.CategoryTheory.Monad.Monadicity Mathlib.CategoryTheory.Monad.Products Mathlib.CategoryTheory.Monad.Types Mathlib.CategoryTheory.Monoidal.Bimod Mathlib.CategoryTheory.Monoidal.Bimon_ Mathlib.CategoryTheory.Monoidal.Braided.Basic Mathlib.CategoryTheory.Monoidal.Braided.Opposite Mathlib.CategoryTheory.Monoidal.Braided.Reflection Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_ Mathlib.CategoryTheory.Monoidal.Category Mathlib.CategoryTheory.Monoidal.Center Mathlib.CategoryTheory.Monoidal.CoherenceLemmas Mathlib.CategoryTheory.Monoidal.CommMon_ Mathlib.CategoryTheory.Monoidal.Comon_ Mathlib.CategoryTheory.Monoidal.Conv Mathlib.CategoryTheory.Monoidal.Discrete Mathlib.CategoryTheory.Monoidal.End Mathlib.CategoryTheory.Monoidal.Free.Basic Mathlib.CategoryTheory.Monoidal.Free.Coherence Mathlib.CategoryTheory.Monoidal.FunctorCategory Mathlib.CategoryTheory.Monoidal.Functor Mathlib.CategoryTheory.Monoidal.Hopf_ Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory Mathlib.CategoryTheory.Monoidal.Internal.Limits Mathlib.CategoryTheory.Monoidal.Internal.Types Mathlib.CategoryTheory.Monoidal.Limits Mathlib.CategoryTheory.Monoidal.Mod_ Mathlib.CategoryTheory.Monoidal.Mon_ Mathlib.CategoryTheory.Monoidal.NaturalTransformation Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Basic Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Symmetric Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts Mathlib.CategoryTheory.Monoidal.Opposite Mathlib.CategoryTheory.Monoidal.Rigid.Basic Mathlib.CategoryTheory.Monoidal.Rigid.Braided Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence Mathlib.CategoryTheory.Monoidal.Skeleton Mathlib.CategoryTheory.Monoidal.Transport Mathlib.CategoryTheory.Monoidal.Types.Basic Mathlib.CategoryTheory.Monoidal.Types.Coyoneda Mathlib.CategoryTheory.Monoidal.Types.Symmetric Mathlib.CategoryTheory.MorphismProperty.Basic Mathlib.CategoryTheory.MorphismProperty.Comma Mathlib.CategoryTheory.MorphismProperty.Composition Mathlib.CategoryTheory.MorphismProperty.Concrete Mathlib.CategoryTheory.MorphismProperty.Factorization Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy Mathlib.CategoryTheory.MorphismProperty.LiftingProperty Mathlib.CategoryTheory.MorphismProperty.Limits Mathlib.CategoryTheory.MorphismProperty.OverAdjunction Mathlib.CategoryTheory.MorphismProperty.Representable Mathlib.CategoryTheory.MorphismProperty.Retract Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.CategoryTheory.NatIso Mathlib.CategoryTheory.NatTrans Mathlib.CategoryTheory.Opposites Mathlib.CategoryTheory.PEmpty Mathlib.CategoryTheory.PUnit Mathlib.CategoryTheory.PathCategory.Basic Mathlib.CategoryTheory.PathCategory.MorphismProperty Mathlib.CategoryTheory.Pi.Basic Mathlib.CategoryTheory.Preadditive.Basic Mathlib.CategoryTheory.Preadditive.FunctorCategory Mathlib.CategoryTheory.Preadditive.Injective Mathlib.CategoryTheory.Preadditive.OfBiproducts Mathlib.CategoryTheory.Preadditive.Projective Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.CategoryTheory.Presentable.Basic Mathlib.CategoryTheory.Presentable.IsCardinalFiltered Mathlib.CategoryTheory.Products.Associator Mathlib.CategoryTheory.Products.Basic Mathlib.CategoryTheory.Products.Bifunctor Mathlib.CategoryTheory.Products.Unitor Mathlib.CategoryTheory.Quotient Mathlib.CategoryTheory.Retract Mathlib.CategoryTheory.Shift.Adjunction Mathlib.CategoryTheory.Shift.Basic Mathlib.CategoryTheory.Shift.CommShift Mathlib.CategoryTheory.Shift.Induced Mathlib.CategoryTheory.Shift.Localization Mathlib.CategoryTheory.Shift.Predicate Mathlib.CategoryTheory.Shift.Quotient Mathlib.CategoryTheory.Shift.SingleFunctors Mathlib.CategoryTheory.Sigma.Basic Mathlib.CategoryTheory.SingleObj Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.ChosenFiniteProducts Mathlib.CategoryTheory.Sites.Closed Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.CompatiblePlus Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.Continuous Mathlib.CategoryTheory.Sites.CoverLifting Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.CategoryTheory.Sites.Coverage Mathlib.CategoryTheory.Sites.CoversTop Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.EffectiveEpimorphic Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.EqualizerSheafCondition Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.Grothendieck Mathlib.CategoryTheory.Sites.IsSheafFor Mathlib.CategoryTheory.Sites.IsSheafOneHypercover Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.Limits Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.MorphismProperty Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 Mathlib.CategoryTheory.Sites.OneHypercover Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.Preserves Mathlib.CategoryTheory.Sites.Pretopology Mathlib.CategoryTheory.Sites.Pullback Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.SheafOfTypes Mathlib.CategoryTheory.Sites.Sheaf Mathlib.CategoryTheory.Sites.Sheafification Mathlib.CategoryTheory.Sites.Sieves Mathlib.CategoryTheory.Sites.Spaces Mathlib.CategoryTheory.Sites.Subcanonical Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Sites.Whiskering Mathlib.CategoryTheory.Skeletal Mathlib.CategoryTheory.SmallObject.Construction Mathlib.CategoryTheory.SmallObject.Iteration.Basic Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting Mathlib.CategoryTheory.SmallObject.WellOrderInductionData Mathlib.CategoryTheory.Square Mathlib.CategoryTheory.Subobject.Basic Mathlib.CategoryTheory.Subobject.Comma Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits Mathlib.CategoryTheory.Subobject.MonoOver Mathlib.CategoryTheory.Subobject.Types Mathlib.CategoryTheory.Subobject.WellPowered Mathlib.CategoryTheory.Subpresheaf.Basic Mathlib.CategoryTheory.Subpresheaf.Equalizer Mathlib.CategoryTheory.Subpresheaf.Image Mathlib.CategoryTheory.Subpresheaf.OfSection Mathlib.CategoryTheory.Subpresheaf.Sieves Mathlib.CategoryTheory.Subterminal Mathlib.CategoryTheory.Sums.Associator Mathlib.CategoryTheory.Sums.Basic Mathlib.CategoryTheory.Thin Mathlib.CategoryTheory.Triangulated.Basic Mathlib.CategoryTheory.Types Mathlib.CategoryTheory.UnivLE Mathlib.CategoryTheory.Whiskering Mathlib.CategoryTheory.Widesubcategory Mathlib.CategoryTheory.WithTerminal Mathlib.CategoryTheory.Yoneda Mathlib.Combinatorics.Hall.Basic Mathlib.Combinatorics.Quiver.ReflQuiver Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.Control.Fold Mathlib.Geometry.RingedSpace.Basic Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.Order.Category.BddDistLat Mathlib.Order.Category.BddLat Mathlib.Order.Category.BddOrd Mathlib.Order.Category.BoolAlg Mathlib.Order.Category.CompleteLat Mathlib.Order.Category.DistLat Mathlib.Order.Category.FinBddDistLat Mathlib.Order.Category.FinBoolAlg Mathlib.Order.Category.FinPartOrd Mathlib.Order.Category.Frm Mathlib.Order.Category.HeytAlg Mathlib.Order.Category.Lat Mathlib.Order.Category.LinOrd Mathlib.Order.Category.NonemptyFinLinOrd Mathlib.Order.Category.OmegaCompletePartialOrder Mathlib.Order.Category.PartOrd Mathlib.Order.Category.Preord Mathlib.Order.Category.Semilat Mathlib.Tactic.CategoryTheory.BicategoricalComp Mathlib.Tactic.CategoryTheory.Bicategory.Basic Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes Mathlib.Tactic.CategoryTheory.Bicategory.Normalize Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence Mathlib.Tactic.CategoryTheory.BicategoryCoherence Mathlib.Tactic.CategoryTheory.CheckCompositions Mathlib.Tactic.CategoryTheory.Coherence.Basic Mathlib.Tactic.CategoryTheory.Coherence Mathlib.Tactic.CategoryTheory.Elementwise Mathlib.Tactic.CategoryTheory.Monoidal.Basic Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes Mathlib.Tactic.CategoryTheory.Monoidal.Normalize Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence Mathlib.Tactic.CategoryTheory.MonoidalComp Mathlib.Tactic.CategoryTheory.Reassoc Mathlib.Tactic.CategoryTheory.Slice Mathlib.Tactic.CategoryTheory.ToApp Mathlib.Tactic.Widget.CommDiag Mathlib.Tactic.Widget.StringDiagram Mathlib.Topology.Category.Born Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.Category.CompHausLike.Limits Mathlib.Topology.Category.CompHausLike.SigmaComparison Mathlib.Topology.Category.FinTopCat Mathlib.Topology.Category.Sequential Mathlib.Topology.Category.TopCat.Adjunctions Mathlib.Topology.Category.TopCat.Basic Mathlib.Topology.Category.TopCat.EffectiveEpi Mathlib.Topology.Category.TopCat.EpiMono Mathlib.Topology.Category.TopCat.Limits.Basic Mathlib.Topology.Category.TopCat.Limits.Cofiltered Mathlib.Topology.Category.TopCat.Limits.Konig Mathlib.Topology.Category.TopCat.Limits.Products Mathlib.Topology.Category.TopCat.Limits.Pullbacks Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.Topology.Category.TopCat.Opens Mathlib.Topology.Category.TopCat.Yoneda Mathlib.Topology.Category.UniformSpace Mathlib.Topology.Gluing Mathlib.Topology.Order.Category.AlexDisc Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.Topology.Sheaves.Presheaf Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks Mathlib.Topology.Specialization

1

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[leanprover-bot]

Here are the benchmark results for commit 11db251.
The entire run failed.
Found no significant differences.

[JovanGerb]

!bench

[leanprover-bot]

Here are the benchmark results for commit 775ba62.
The entire run failed.
Found no significant differences.

[JovanGerb]

!bench

[leanprover-bot]

Here are the benchmark results for commit 55aba30.
There were significant changes against commit 213a36c:

  Benchmark                                                                Metric         Change
  ==============================================================================================
+ build                                                                    aesop          -18.5%
+ build                                                                    simp            -7.1%
+ ~Mathlib.Algebra.Category.Grp.Adjunctions                                instructions   -54.4%
+ ~Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup                   instructions   -53.7%
+ ~Mathlib.Algebra.Category.Grp.ForgetCorepresentable                      instructions   -59.2%
+ ~Mathlib.Algebra.Category.ModuleCat.Algebra                              instructions   -38.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Basic                                instructions   -15.9%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                        instructions    -3.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf                             instructions    -8.9%
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward                 instructions   -42.7%
+ ~Mathlib.Algebra.Category.ModuleCat.Pseudofunctor                        instructions   -51.5%
+ ~Mathlib.Algebra.Category.ModuleCat.Sheaf                                instructions   -28.7%
+ ~Mathlib.Algebra.Homology.Augment                                        instructions   -16.6%
+ ~Mathlib.Algebra.Homology.Opposite                                       instructions   -18.7%
+ ~Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence                instructions   -15.9%
+ ~Mathlib.AlgebraicGeometry.Modules.Tilde                                 instructions   -38.9%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf             instructions   -16.7%
+ ~Mathlib.AlgebraicGeometry.StructureSheaf                                instructions    -6.6%
+ ~Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject                 instructions   -41.9%
+ ~Mathlib.AlgebraicTopology.SimplicialNerve                               instructions   -63.9%
+ ~Mathlib.AlgebraicTopology.SimplicialObject.Basic                        instructions   -26.7%
+ ~Mathlib.AlgebraicTopology.SimplicialSet.Nerve                           instructions   -71.0%
+ ~Mathlib.CategoryTheory.Action.Basic                                     instructions   -17.8%
+ ~Mathlib.CategoryTheory.Bicategory.Coherence                             instructions   -14.3%
+ ~Mathlib.CategoryTheory.Comma.Basic                                      instructions   -13.0%
+ ~Mathlib.CategoryTheory.Comma.Over                                       instructions    -8.2%
+ ~Mathlib.CategoryTheory.Comma.Presheaf.Basic                             instructions   -18.3%
+ ~Mathlib.CategoryTheory.Comma.StructuredArrow.Basic                      instructions   -20.0%
+ ~Mathlib.CategoryTheory.Elements                                         instructions   -35.3%
+ ~Mathlib.CategoryTheory.Functor.Currying                                 instructions   -38.9%
+ ~Mathlib.CategoryTheory.Functor.KanExtension.Pointwise                   instructions   -16.9%
+ ~Mathlib.CategoryTheory.Functor.Trifunctor                               instructions    -6.3%
+ ~Mathlib.CategoryTheory.Limits.ConeCategory                              instructions   -27.8%
+ ~Mathlib.CategoryTheory.Limits.Cones                                     instructions    -8.2%
+ ~Mathlib.CategoryTheory.Limits.Constructions.Over.Products               instructions   -26.0%
+ ~Mathlib.CategoryTheory.Limits.ExactFunctor                              instructions   -25.1%
+ ~Mathlib.CategoryTheory.Limits.Final                                     instructions   -27.5%
+ ~Mathlib.CategoryTheory.Limits.Lattice                                   instructions   -46.3%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Biproducts                         instructions   -19.3%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer                     instructions   -14.1%
+ ~Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor   instructions   -56.3%
+ ~Mathlib.CategoryTheory.Monad.Products                                   instructions   -28.9%
+ ~Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_                        instructions   -43.9%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory                instructions    -8.9%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.Module                         instructions   -35.3%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.Types                          instructions   -68.7%
+ ~Mathlib.CategoryTheory.Products.Basic                                   instructions   -22.7%
+ ~Mathlib.CategoryTheory.Skeletal                                         instructions   -53.2%
+ ~Mathlib.CategoryTheory.Square                                           instructions   -33.4%
+ ~Mathlib.CategoryTheory.Subobject.Types                                  instructions   -57.5%
+ ~Mathlib.CategoryTheory.Triangulated.Opposite.Triangle                   instructions   -25.2%
+ ~Mathlib.Condensed.Discrete.Colimit                                      instructions   -16.5%
+ ~Mathlib.Condensed.Discrete.LocallyConstant                              instructions   -49.5%
+ ~Mathlib.Condensed.Discrete.Module                                       instructions   -27.9%
+ ~Mathlib.Geometry.RingedSpace.LocallyRingedSpace                         instructions   -24.6%
+ ~Mathlib.Order.Category.BddLat                                           instructions   -31.8%
+ ~Mathlib.Order.Category.BoolAlg                                          instructions   -43.3%
+ ~Mathlib.Order.Category.FinBddDistLat                                    instructions   -55.2%
+ ~Mathlib.Order.Category.FinBoolAlg                                       instructions   -48.3%
+ ~Mathlib.Order.Category.NonemptyFinLinOrd                                instructions   -50.3%
+ ~Mathlib.Order.Category.Semilat                                          instructions   -50.0%
+ ~Mathlib.RepresentationTheory.Rep                                        instructions    -9.6%
+ ~Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic                    instructions   -23.1%
+ ~Mathlib.Topology.Category.TopCat.OpenNhds                               instructions   -65.4%
+ ~Mathlib.Topology.Category.TopCat.Opens                                  instructions   -54.4%
+ ~Mathlib.Topology.Order.Category.AlexDisc                                instructions   -62.7%
+ ~Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts               instructions   -10.2%
+ ~Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover                    instructions   -20.5%
+ ~Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections           instructions   -37.1%

[github-actions]

File	Instructions	%
build	-2104.144⬝10⁹	(-1.37%)

2 files, Instructions +7.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.MorphismProperty.OverAdjunction	+7.844⬝10⁹	(+7.97%)
Mathlib.Algebra.Homology.Embedding.TruncLE	+7.654⬝10⁹	(+32.43%)

File	Instructions	%
Mathlib.AlgebraicTopology.MooreComplex	+5.519⬝10⁹	(+13.86%)

2 files, Instructions +3.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Monoidal.Discrete	+3.258⬝10⁹	(+8.06%)
Mathlib.CategoryTheory.GradedObject.Trifunctor	+3.119⬝10⁹	(+1.22%)

3 files, Instructions +2.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Triangulated.Functor	+2.612⬝10⁹	(+0.83%)
Mathlib.CategoryTheory.Functor.CurryingThree	+2.130⬝10⁹	(+1.24%)
Mathlib.CategoryTheory.Bicategory.LocallyDiscrete	+2.0⬝10⁹	(+15.10%)

13 files, Instructions +1.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.GradedObject	+1.795⬝10⁹	(+2.93%)
Mathlib.Algebra.Homology.ShortComplex.Preadditive	+1.776⬝10⁹	(+1.80%)
Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete	+1.595⬝10⁹	(+1.72%)
Mathlib.CategoryTheory.GuitartExact.VerticalComposition	+1.517⬝10⁹	(+3.73%)
Mathlib.Algebra.Homology.Bifunctor	+1.484⬝10⁹	(+1.31%)
Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap	+1.437⬝10⁹	(+1.20%)
Mathlib.CategoryTheory.Comma.StructuredArrow.Functor	+1.257⬝10⁹	(+2.32%)
Mathlib.CategoryTheory.Sites.ChosenFiniteProducts	+1.181⬝10⁹	(+7.62%)
Mathlib.CategoryTheory.Functor.Flat	+1.130⬝10⁹	(+1.35%)
Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory	+1.45⬝10⁹	(+1.64%)
Mathlib.Algebra.Homology.ShortComplex.Linear	+1.31⬝10⁹	(+1.88%)
Mathlib.CategoryTheory.Adjunction.Over	+1.14⬝10⁹	(+1.19%)
Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors	+1.11⬝10⁹	(+1.35%)

46 files, Instructions -2.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Closed.Zero	-1.5⬝10⁹	(-14.22%)
Mathlib.CategoryTheory.Preadditive.EilenbergMoore	-1.50⬝10⁹	(-4.85%)
Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex	-1.52⬝10⁹	(-1.88%)
Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Basic	-1.81⬝10⁹	(-3.56%)
Mathlib.CategoryTheory.Quotient	-1.124⬝10⁹	(-8.05%)
Mathlib.CategoryTheory.Category.ReflQuiv	-1.149⬝10⁹	(-3.92%)
Mathlib.CategoryTheory.Category.Cat	-1.180⬝10⁹	(-4.96%)
Mathlib.Topology.Sheaves.Sheaf	-1.184⬝10⁹	(-15.55%)
Mathlib.CategoryTheory.Opposites	-1.188⬝10⁹	(-2.60%)
Mathlib.Algebra.Homology.ShortComplex.Basic	-1.199⬝10⁹	(-3.89%)
Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition	-1.231⬝10⁹	(-15.26%)
Mathlib.AlgebraicGeometry.Scheme	-1.239⬝10⁹	(-1.12%)
Mathlib.Order.Category.HeytAlg	-1.245⬝10⁹	(-17.14%)
Mathlib.CategoryTheory.Category.GaloisConnection	-1.289⬝10⁹	(-25.91%)
Mathlib.Algebra.Homology.HomotopyCategory	-1.294⬝10⁹	(-7.61%)
Mathlib.CategoryTheory.Subobject.Basic	-1.299⬝10⁹	(-2.37%)
Mathlib.CategoryTheory.Limits.HasLimits	-1.334⬝10⁹	(-1.66%)
Mathlib.CategoryTheory.Limits.Unit	-1.361⬝10⁹	(-24.50%)
Mathlib.CategoryTheory.IsConnected	-1.378⬝10⁹	(-7.59%)
Mathlib.CategoryTheory.Subpresheaf.Basic	-1.433⬝10⁹	(-7.09%)
Mathlib.CategoryTheory.Limits.Shapes.Equalizers	-1.441⬝10⁹	(-2.35%)
Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed	-1.457⬝10⁹	(-1.61%)
Mathlib.Algebra.Homology.Embedding.Restriction	-1.460⬝10⁹	(-18.54%)
Mathlib.CategoryTheory.FiberedCategory.BasedCategory	-1.460⬝10⁹	(-3.95%)
Mathlib.CategoryTheory.Idempotents.HomologicalComplex	-1.460⬝10⁹	(-3.89%)
Mathlib.CategoryTheory.Sites.Types	-1.474⬝10⁹	(-13.11%)
Mathlib.Algebra.Category.FGModuleCat.Basic	-1.489⬝10⁹	(-4.78%)
Mathlib.Topology.Category.Profinite.AsLimit	-1.496⬝10⁹	(-10.88%)
Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject	-1.499⬝10⁹	(-17.89%)
Mathlib.CategoryTheory.Limits.IsLimit	-1.514⬝10⁹	(-1.61%)
Mathlib.CategoryTheory.Linear.LinearFunctor	-1.530⬝10⁹	(-13.89%)
Mathlib.CategoryTheory.Limits.Final.ParallelPair	-1.537⬝10⁹	(-30.27%)
Mathlib.Topology.Category.TopCat.Basic	-1.567⬝10⁹	(-16.54%)
Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes	-1.672⬝10⁹	(-6.93%)
Mathlib.CategoryTheory.Category.Pointed	-1.679⬝10⁹	(-27.67%)
Mathlib.Algebra.Homology.Additive	-1.684⬝10⁹	(-2.25%)
Mathlib.CategoryTheory.Idempotents.Karoubi	-1.723⬝10⁹	(-10.65%)
Mathlib.CategoryTheory.Products.Unitor	-1.723⬝10⁹	(-25.45%)
Mathlib.CategoryTheory.Category.ULift	-1.735⬝10⁹	(-7.40%)
Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric	-1.767⬝10⁹	(-9.22%)
Mathlib.AlgebraicGeometry.Cover.MorphismProperty	-1.849⬝10⁹	(-8.35%)
Mathlib.Geometry.RingedSpace.PresheafedSpace	-1.849⬝10⁹	(-1.74%)
Mathlib.CategoryTheory.Sites.Continuous	-1.892⬝10⁹	(-15.89%)
Mathlib.CategoryTheory.Sites.Sieves	-1.957⬝10⁹	(-5.88%)
Mathlib.AlgebraicTopology.AlternatingFaceMapComplex	-1.966⬝10⁹	(-5.82%)
Mathlib.Condensed.TopCatAdjunction	-1.983⬝10⁹	(-9.89%)

38 files, Instructions -3.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor	-2.22⬝10⁹	(-11.41%)
Mathlib.Geometry.Manifold.Sheaf.Smooth	-2.158⬝10⁹	(-2.03%)
Mathlib.Algebra.Category.Grp.Ulift	-2.248⬝10⁹	(-13.67%)
Mathlib.CategoryTheory.Limits.Shapes.Reflexive	-2.249⬝10⁹	(-3.14%)
Mathlib.CategoryTheory.WithTerminal	-2.258⬝10⁹	(-1.78%)
Mathlib.CategoryTheory.Sites.Grothendieck	-2.271⬝10⁹	(-10.24%)
Mathlib.CategoryTheory.Category.Quiv	-2.286⬝10⁹	(-17.60%)
Mathlib.Condensed.Light.TopCatAdjunction	-2.290⬝10⁹	(-9.95%)
Mathlib.CategoryTheory.Comma.Arrow	-2.296⬝10⁹	(-7.80%)
Mathlib.CategoryTheory.Closed.FunctorToTypes	-2.303⬝10⁹	(-12.21%)
Mathlib.Algebra.Category.GrpWithZero	-2.309⬝10⁹	(-26.41%)
Mathlib.AlgebraicTopology.SimplexCategory	-2.310⬝10⁹	(-4.33%)
Mathlib.CategoryTheory.Sites.Coherent.SheafComparison	-2.311⬝10⁹	(-10.30%)
Mathlib.CategoryTheory.Whiskering	-2.331⬝10⁹	(-0.88%)
Mathlib.CategoryTheory.Sites.SheafHom	-2.336⬝10⁹	(-6.45%)
Mathlib.Topology.Category.Profinite.Basic	-2.338⬝10⁹	(-12.98%)
Mathlib.CategoryTheory.Monoidal.CommMon_	-2.446⬝10⁹	(-2.34%)
Mathlib.CategoryTheory.Sites.Over	-2.470⬝10⁹	(-9.40%)
Mathlib.CategoryTheory.Sums.Associator	-2.504⬝10⁹	(-12.46%)
Mathlib.CategoryTheory.Monoidal.Bimon_	-2.505⬝10⁹	(-2.89%)
Mathlib.CategoryTheory.Types	-2.547⬝10⁹	(-23.38%)
Mathlib.Topology.Sheaves.SheafCondition.Sites	-2.549⬝10⁹	(-20.42%)
Mathlib.CategoryTheory.Closed.Types	-2.582⬝10⁹	(-12.88%)
Mathlib.CategoryTheory.Category.Cat.Adjunction	-2.605⬝10⁹	(-20.62%)
Mathlib.Order.Category.DistLat	-2.612⬝10⁹	(-25.28%)
Mathlib.Algebra.Homology.LocalCohomology	-2.619⬝10⁹	(-8.37%)
Mathlib.CategoryTheory.Sites.Limits	-2.633⬝10⁹	(-8.41%)
Mathlib.AlgebraicGeometry.Limits	-2.682⬝10⁹	(-3.51%)
Mathlib.CategoryTheory.DiscreteCategory	-2.691⬝10⁹	(-7.96%)
Mathlib.CategoryTheory.CodiscreteCategory	-2.735⬝10⁹	(-33.78%)
Mathlib.Algebra.Category.Grp.Preadditive	-2.737⬝10⁹	(-18.59%)
Mathlib.CategoryTheory.Sites.Equivalence	-2.752⬝10⁹	(-7.73%)
Mathlib.CategoryTheory.Monoidal.Comon_	-2.766⬝10⁹	(-4.12%)
Mathlib.Analysis.Normed.Group.SemiNormedGrp	-2.780⬝10⁹	(-17.76%)
Mathlib.Topology.Category.UniformSpace	-2.782⬝10⁹	(-21.50%)
Mathlib.Algebra.Homology.HomologicalBicomplex	-2.839⬝10⁹	(-6.51%)
Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat	-2.947⬝10⁹	(-15.44%)
Mathlib.Condensed.TopComparison	-2.990⬝10⁹	(-19.32%)

15 files, Instructions -4.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.SmallObject.Iteration.Basic	-3.21⬝10⁹	(-10.75%)
Mathlib.CategoryTheory.Functor.Const	-3.92⬝10⁹	(-13.95%)
Mathlib.Algebra.Category.MonCat.Basic	-3.102⬝10⁹	(-10.55%)
Mathlib.CategoryTheory.MorphismProperty.Limits	-3.105⬝10⁹	(-9.29%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator	-3.178⬝10⁹	(-19.11%)
Mathlib.Topology.Category.Compactum	-3.210⬝10⁹	(-16.21%)
Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks	-3.282⬝10⁹	(-2.62%)
Mathlib.CategoryTheory.Enriched.Basic	-3.585⬝10⁹	(-12.16%)
Mathlib.CategoryTheory.Grothendieck	-3.719⬝10⁹	(-3.64%)
Mathlib.AlgebraicTopology.SimplicialSet.Boundary	-3.809⬝10⁹	(-41.60%)
Mathlib.Algebra.Homology.ShortComplex.SnakeLemma	-3.834⬝10⁹	(-3.88%)
Mathlib.Algebra.Category.MonCat.Adjunctions	-3.881⬝10⁹	(-32.85%)
Mathlib.CategoryTheory.Monad.EquivMon	-3.896⬝10⁹	(-9.19%)
Mathlib.Topology.Category.Profinite.Product	-3.930⬝10⁹	(-30.01%)
Mathlib.Algebra.Category.AlgebraCat.Basic	-3.981⬝10⁹	(-9.50%)

13 files, Instructions -5.0⬝10⁹

File	Instructions	%
Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings	-4.37⬝10⁹	(-16.23%)
Mathlib.CategoryTheory.Monoidal.Mon_	-4.121⬝10⁹	(-2.85%)
Mathlib.Topology.Sheaves.CommRingCat	-4.289⬝10⁹	(-6.15%)
Mathlib.Algebra.Category.Ring.Adjunctions	-4.313⬝10⁹	(-26.52%)
Mathlib.CategoryTheory.Localization.Resolution	-4.422⬝10⁹	(-18.68%)
Mathlib.Algebra.Homology.DifferentialObject	-4.523⬝10⁹	(-8.14%)
Mathlib.CategoryTheory.Category.TwoP	-4.561⬝10⁹	(-41.59%)
Mathlib.CategoryTheory.Limits.Opposites	-4.610⬝10⁹	(-4.87%)
Mathlib.Algebra.Category.Grp.Basic	-4.647⬝10⁹	(-10.89%)
Mathlib.CategoryTheory.Sites.SheafOfTypes	-4.713⬝10⁹	(-18.76%)
Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous	-4.859⬝10⁹	(-34.85%)
Mathlib.Order.Category.PartOrd	-4.867⬝10⁹	(-38.06%)
Mathlib.Algebra.Category.HopfAlgebraCat.Basic	-4.905⬝10⁹	(-18.97%)

18 files, Instructions -6.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Category.Pairwise	-5.19⬝10⁹	(-30.29%)
Mathlib.Order.Category.Lat	-5.234⬝10⁹	(-40.81%)
Mathlib.Topology.Category.LightProfinite.Basic	-5.237⬝10⁹	(-13.40%)
Mathlib.Order.Category.Preord	-5.239⬝10⁹	(-50.09%)
Mathlib.Topology.Category.DeltaGenerated	-5.239⬝10⁹	(-41.24%)
Mathlib.Algebra.Category.CoalgebraCat.Basic	-5.259⬝10⁹	(-21.07%)
Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi	-5.360⬝10⁹	(-19.31%)
Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal	-5.462⬝10⁹	(-18.41%)
Mathlib.Order.Category.CompleteLat	-5.550⬝10⁹	(-37.13%)
Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric	-5.558⬝10⁹	(-41.31%)
Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat	-5.582⬝10⁹	(-10.91%)
Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers	-5.635⬝10⁹	(-14.25%)
Mathlib.CategoryTheory.MorphismProperty.Concrete	-5.745⬝10⁹	(-44.49%)
Mathlib.CategoryTheory.Functor.Category	-5.788⬝10⁹	(-19.36%)
Mathlib.AlgebraicTopology.SimplicialSet.Horn	-5.825⬝10⁹	(-26.45%)
Mathlib.CategoryTheory.Endofunctor.Algebra	-5.938⬝10⁹	(-9.15%)
Mathlib.Topology.Category.TopCommRingCat	-5.974⬝10⁹	(-44.82%)
Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence	-5.986⬝10⁹	(-8.13%)

10 files, Instructions -7.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Yoneda	-6.178⬝10⁹	(-5.48%)
Mathlib.CategoryTheory.Monad.Algebra	-6.368⬝10⁹	(-11.49%)
Mathlib.Algebra.Category.AlgebraCat.Symmetric	-6.396⬝10⁹	(-43.41%)
Mathlib.CategoryTheory.Functor.FunctorHom	-6.407⬝10⁹	(-15.93%)
Mathlib.CategoryTheory.Limits.Shapes.Types	-6.443⬝10⁹	(-12.15%)
Mathlib.Topology.Sheaves.Alexandrov	-6.448⬝10⁹	(-21.74%)
Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Strong	-6.520⬝10⁹	(-13.57%)
Mathlib.Topology.Category.TopCat.Adjunctions	-6.584⬝10⁹	(-59.08%)
Mathlib.CategoryTheory.Category.Preorder	-6.820⬝10⁹	(-48.70%)
Mathlib.Order.Category.LinOrd	-6.933⬝10⁹	(-47.33%)

5 files, Instructions -8.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Category.Bipointed	-7.39⬝10⁹	(-46.51%)
Mathlib.CategoryTheory.Products.Associator	-7.401⬝10⁹	(-53.07%)
Mathlib.CategoryTheory.Action.Limits	-7.709⬝10⁹	(-14.95%)
Mathlib.Algebra.Category.BialgebraCat.Basic	-7.800⬝10⁹	(-20.61%)
Mathlib.Topology.Sheaves.Presheaf	-7.948⬝10⁹	(-10.70%)

4 files, Instructions -9.0⬝10⁹

File	Instructions	%
Mathlib.Algebra.Category.BoolRing	-8.153⬝10⁹	(-34.27%)
Mathlib.Algebra.Homology.Functor	-8.477⬝10⁹	(-52.61%)
Mathlib.Order.Category.FinPartOrd	-8.520⬝10⁹	(-59.50%)
Mathlib.Topology.Order.Category.FrameAdjunction	-8.925⬝10⁹	(-33.69%)

7 files, Instructions -10.0⬝10⁹

File	Instructions	%
Mathlib.Algebra.Category.MonCat.ForgetCorepresentable	-9.64⬝10⁹	(-57.42%)
Mathlib.Algebra.Category.AlgebraCat.Monoidal	-9.121⬝10⁹	(-30.62%)
Mathlib.Algebra.Category.Ring.Basic	-9.552⬝10⁹	(-20.66%)
Mathlib.Topology.Sheaves.LocalPredicate	-9.578⬝10⁹	(-37.59%)
Mathlib.Order.Category.BddOrd	-9.645⬝10⁹	(-55.85%)
Mathlib.Order.Category.BddDistLat	-9.768⬝10⁹	(-49.28%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings	-9.773⬝10⁹	(-13.54%)

7 files, Instructions -11.0⬝10⁹

File	Instructions	%
Mathlib.Order.Category.BddLat	-10.65⬝10⁹	(-31.80%)
Mathlib.CategoryTheory.Action.Basic	-10.283⬝10⁹	(-17.81%)
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings	-10.362⬝10⁹	(-3.30%)
Mathlib.CategoryTheory.Limits.Lattice	-10.525⬝10⁹	(-46.34%)
Mathlib.Algebra.Homology.Augment	-10.632⬝10⁹	(-16.55%)
Mathlib.CategoryTheory.Functor.Trifunctor	-10.718⬝10⁹	(-6.30%)
Mathlib.Algebra.Category.Grp.ForgetCorepresentable	-10.753⬝10⁹	(-59.20%)

5 files, Instructions -12.0⬝10⁹

File	Instructions	%
Mathlib.AlgebraicGeometry.StructureSheaf	-11.115⬝10⁹	(-6.59%)
Mathlib.Topology.Order.Category.AlexDisc	-11.402⬝10⁹	(-62.73%)
Mathlib.Algebra.Category.ModuleCat.Sheaf	-11.554⬝10⁹	(-28.68%)
Mathlib.Order.Category.Semilat	-11.613⬝10⁹	(-50.04%)
Mathlib.Order.Category.BoolAlg	-11.871⬝10⁹	(-43.33%)

4 files, Instructions -13.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Functor.KanExtension.Pointwise	-12.308⬝10⁹	(-16.92%)
Mathlib.RepresentationTheory.Rep	-12.520⬝10⁹	(-9.61%)
Mathlib.Algebra.Homology.Opposite	-12.940⬝10⁹	(-18.74%)
Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer	-12.963⬝10⁹	(-14.12%)

9 files, Instructions -14.0⬝10⁹

File	Instructions	%
Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts	-13.99⬝10⁹	(-10.23%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf	-13.168⬝10⁹	(-16.74%)
Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup	-13.179⬝10⁹	(-53.68%)
Mathlib.Algebra.Category.ModuleCat.Basic	-13.241⬝10⁹	(-15.92%)
Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory	-13.350⬝10⁹	(-8.86%)
Mathlib.CategoryTheory.Limits.ExactFunctor	-13.444⬝10⁹	(-25.09%)
Mathlib.AlgebraicTopology.SimplicialSet.Nerve	-13.545⬝10⁹	(-70.97%)
Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_	-13.576⬝10⁹	(-43.85%)
Mathlib.Geometry.RingedSpace.LocallyRingedSpace	-13.976⬝10⁹	(-24.61%)

File	Instructions	%
Mathlib.Order.Category.FinBddDistLat	-14.341⬝10⁹	(-55.22%)
Mathlib.Order.Category.NonemptyFinLinOrd	-15.933⬝10⁹	(-50.32%)

2 files, Instructions -17.0⬝10⁹

File	Instructions	%
Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject	-16.213⬝10⁹	(-41.92%)
Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence	-16.317⬝10⁹	(-15.91%)

6 files, Instructions -18.0⬝10⁹

File	Instructions	%
Mathlib.Algebra.Category.ModuleCat.Algebra	-17.214⬝10⁹	(-38.32%)
Mathlib.CategoryTheory.Bicategory.Coherence	-17.399⬝10⁹	(-14.26%)
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic	-17.468⬝10⁹	(-23.08%)
Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover	-17.498⬝10⁹	(-20.48%)
Mathlib.CategoryTheory.Monad.Products	-17.570⬝10⁹	(-28.94%)
Mathlib.Order.Category.FinBoolAlg	-17.740⬝10⁹	(-48.27%)

File	Instructions	%
Mathlib.Algebra.Category.Grp.Adjunctions	-18.223⬝10⁹	(-54.44%)

2 files, Instructions -21.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Products.Basic	-20.67⬝10⁹	(-22.73%)
Mathlib.Condensed.Discrete.Colimit	-20.456⬝10⁹	(-16.49%)

2 files, Instructions -22.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Skeletal	-21.257⬝10⁹	(-53.16%)
Mathlib.CategoryTheory.Limits.Constructions.Over.Products	-21.660⬝10⁹	(-26.00%)

File	Instructions	%
Mathlib.Topology.Category.TopCat.OpenNhds	-22.226⬝10⁹	(-65.41%)
Mathlib.Algebra.Category.ModuleCat.Presheaf	-23.322⬝10⁹	(-8.91%)

4 files, Instructions -25.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Square	-24.111⬝10⁹	(-33.41%)
Mathlib.CategoryTheory.Limits.ConeCategory	-24.171⬝10⁹	(-27.80%)
Mathlib.Algebra.Category.ModuleCat.Pseudofunctor	-24.717⬝10⁹	(-51.52%)
Mathlib.CategoryTheory.Elements	-24.965⬝10⁹	(-35.30%)

3 files, Instructions -26.0⬝10⁹

File	Instructions	%
Mathlib.CategoryTheory.Comma.Over	-25.161⬝10⁹	(-8.20%)
Mathlib.CategoryTheory.Comma.Basic	-25.427⬝10⁹	(-13.02%)
Mathlib.CategoryTheory.Limits.Cones	-25.979⬝10⁹	(-8.24%)

File	Instructions	%
Mathlib.CategoryTheory.Subobject.Types	-26.885⬝10⁹	(-57.45%)
Mathlib.CategoryTheory.Comma.Presheaf.Basic	-27.305⬝10⁹	(-18.34%)

2 files, Instructions -29.0⬝10⁹

File	Instructions	%
Mathlib.Topology.Category.TopCat.Opens	-28.709⬝10⁹	(-54.38%)
Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor	-28.932⬝10⁹	(-56.27%)

File	Instructions	%
Mathlib.Condensed.Discrete.Module	-31.950⬝10⁹	(-27.92%)
Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections	-33.41⬝10⁹	(-37.07%)
Mathlib.CategoryTheory.Triangulated.Opposite.Triangle	-34.196⬝10⁹	(-25.19%)
Mathlib.CategoryTheory.Monoidal.Internal.Types	-36.565⬝10⁹	(-68.71%)
Mathlib.Condensed.Discrete.LocallyConstant	-37.208⬝10⁹	(-49.49%)
Mathlib.CategoryTheory.Functor.Currying	-42.715⬝10⁹	(-38.92%)
Mathlib.CategoryTheory.Monoidal.Internal.Module	-50.723⬝10⁹	(-35.34%)
Mathlib.CategoryTheory.Limits.Final	-51.135⬝10⁹	(-27.49%)
Mathlib.AlgebraicGeometry.Modules.Tilde	-52.875⬝10⁹	(-38.91%)
Mathlib.CategoryTheory.Limits.Shapes.Biproducts	-53.141⬝10⁹	(-19.28%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward	-54.458⬝10⁹	(-42.72%)
Mathlib.AlgebraicTopology.SimplicialObject.Basic	-56.709⬝10⁹	(-26.65%)
Mathlib.CategoryTheory.Comma.StructuredArrow.Basic	-63.465⬝10⁹	(-19.95%)
Mathlib.AlgebraicTopology.SimplicialNerve	-86.948⬝10⁹	(-63.86%)
CI run

[grunweg]

Thanks for trying this; the gains looks impressive! I took a look already and have a few comments - which maybe you were intending to address all along. In case one of them is new, let me share them here:

• Would you like to split out the unused variable removal and the @simp un-tagging? I'll approve the former change immediately.
• Can you say something about why the refine id ?_ change is necessary? (Both in the PR description and code, say.)
• Can you make the same change to aesop_cat?, please?

[JovanGerb]

One question I have is whether this is the right solution, or if this is something that can be improved in aesop internally.

[grunweg]

Good question! @JLimperg Can you comment on the above question: would it be useful to have an "easy pre-pass" in aesop, trying proofs like "rfl" first, before running all of aesop? This PR does this for the auto-params in category theory, with dramatic effects.

[JLimperg]

The most natural way to do this would be to make rfl a high-priority (low-penalty) Aesop normalisation rule. So something like

add_aesop_rules norm -10 (rule_sets := [CategoryTheory]) (by rfl)

This will make Aesop try rfl before most other rules, in particular simp.

However, it'll also retry rfl on each normalisation round, which is not ideal. Aesop used to have an option to use a rule at most n times (here n = 1), but I removed it at some point because it was unused. I could bring that back.

So for now, the approach used in this PR is probably optimal.

[JLimperg]

Btw, might be worth trying with_reducible rfl instead of rfl as well.

[JovanGerb]

I think rfl instead of with_reducible rfl is the right tactic. with_reducible rfl is also used by simp, so any goal that can be closed by with_reducible rfl would be closed by aesop fairly quickly.

[JovanGerb]

To make aesop_cat? work nicely, I've added a macro rfl_cat which gets suggested by aesop_cat? and which is short for refine id ?_; intros; rfl.

[grunweg]

Thanks for your PR. As far as I can, the two dependent changes have been merged, this PR is documented and seems like a good approach for now. Is there anything else this PR is waiting on?
@JovanGerb If there's nothing else you'd like to do, if you merge master and un-draft this PR, I'll be happy to maintainer merge it.

[JovanGerb]

I think I found an underlying reason today for why the simp calls in category theory were so slow in the first place. I've posted it on Zulip now. So I think it would be better to wait with this PR until that is figured out further.