[Merged by Bors] - perf(CategoryTheory): let aesop_cat attempt rfl before aesop#21330
Closed
[Merged by Bors] - perf(CategoryTheory): let aesop_cat attempt rfl before aesop#21330
aesop_cat attempt rfl before aesop#21330Conversation
PR summary c262624cfc
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.Category.Basic | 268 | 269 | +1 (+0.37%) |
| Mathlib.CategoryTheory.Monoidal.Mod_ | 472 | 473 | +1 (+0.21%) |
| Mathlib.Algebra.Homology.DifferentialObject | 709 | 710 | +1 (+0.14%) |
Import changes for all files
| Files | Import difference |
|---|---|
786 filesMathlib.Algebra.Category.Grp.Adjunctions 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.BifunctorFlip Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double 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.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.AlgebraicTopology.CechNerve Mathlib.AlgebraicTopology.DoldKan.Compatibility Mathlib.AlgebraicTopology.ModelCategory.Basic Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells Mathlib.AlgebraicTopology.RelativeCellComplex.Basic Mathlib.AlgebraicTopology.SimplexCategory.Basic Mathlib.AlgebraicTopology.SimplexCategory.Defs Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty 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.CategoryWithFibrations Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.AlgebraicTopology.SimplicialSet.Degenerate Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Horn Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex Mathlib.CategoryTheory.Abelian.Images Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.CategoryTheory.Action.Basic Mathlib.CategoryTheory.Action.Concrete Mathlib.CategoryTheory.Action.Continuous Mathlib.CategoryTheory.Action 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.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.Colimit Mathlib.CategoryTheory.Category.Cat.Limit Mathlib.CategoryTheory.Category.Cat.Op 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.Basic 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.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.Over.Basic Mathlib.CategoryTheory.Comma.Over.OverClass Mathlib.CategoryTheory.Comma.Over.Pullback Mathlib.CategoryTheory.Comma.Presheaf.Basic Mathlib.CategoryTheory.Comma.Presheaf.Colimit Mathlib.CategoryTheory.Comma.StructuredArrow.Basic Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap Mathlib.CategoryTheory.Comma.StructuredArrow.Final 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.Discrete.Basic Mathlib.CategoryTheory.Discrete.SumsProducts 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.Limits.HasConicalLimits Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal 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.Balanced Mathlib.CategoryTheory.Functor.ReflectsIso.Basic Mathlib.CategoryTheory.Functor.Trifunctor Mathlib.CategoryTheory.Functor.TwoSquare Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Galois.Decomposition Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex 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.FunctorCategory.Shapes.Pullbacks 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.Preorder 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.Set Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts 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.Fin Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape 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.Cartesian.Mon_ Mathlib.CategoryTheory.Monoidal.Category Mathlib.CategoryTheory.Monoidal.Center Mathlib.CategoryTheory.Monoidal.CoherenceLemmas Mathlib.CategoryTheory.Monoidal.CommGrp_ 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.Grp_ Mathlib.CategoryTheory.Monoidal.Hopf_ Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory Mathlib.CategoryTheory.Monoidal.Internal.Limits Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_ 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.Yoneda Mathlib.CategoryTheory.MorphismProperty.Basic Mathlib.CategoryTheory.MorphismProperty.Comma Mathlib.CategoryTheory.MorphismProperty.Composition Mathlib.CategoryTheory.MorphismProperty.Concrete Mathlib.CategoryTheory.MorphismProperty.Descent Mathlib.CategoryTheory.MorphismProperty.Factorization Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy Mathlib.CategoryTheory.MorphismProperty.IsSmall Mathlib.CategoryTheory.MorphismProperty.LiftingProperty Mathlib.CategoryTheory.MorphismProperty.Limits Mathlib.CategoryTheory.MorphismProperty.OverAdjunction Mathlib.CategoryTheory.MorphismProperty.Representable Mathlib.CategoryTheory.MorphismProperty.RetractArgument Mathlib.CategoryTheory.MorphismProperty.Retract Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.CategoryTheory.NatIso Mathlib.CategoryTheory.NatTrans Mathlib.CategoryTheory.ObjectProperty.Basic Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms Mathlib.CategoryTheory.ObjectProperty.ContainsZero Mathlib.CategoryTheory.ObjectProperty.Shift 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.Basic Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties Mathlib.CategoryTheory.Preadditive.Injective.Preserves Mathlib.CategoryTheory.Preadditive.LiftToFinset Mathlib.CategoryTheory.Preadditive.OfBiproducts Mathlib.CategoryTheory.Preadditive.Projective.Basic Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties Mathlib.CategoryTheory.Preadditive.Projective.Preserves Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.CategoryTheory.Presentable.Basic Mathlib.CategoryTheory.Presentable.IsCardinalFiltered Mathlib.CategoryTheory.Presentable.Limits 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.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.Monoidal 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.Basic Mathlib.CategoryTheory.SmallObject.Construction Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument 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.TransfiniteIteration Mathlib.CategoryTheory.SmallObject.WellOrderInductionData Mathlib.CategoryTheory.Square Mathlib.CategoryTheory.Subobject.Basic Mathlib.CategoryTheory.Subobject.Comma Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.CategoryTheory.Subobject.HasCardinalLT Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits Mathlib.CategoryTheory.Subobject.MonoOver Mathlib.CategoryTheory.Subobject.Presheaf Mathlib.CategoryTheory.Subobject.Types Mathlib.CategoryTheory.Subobject.WellPowered Mathlib.CategoryTheory.Subpresheaf.Basic Mathlib.CategoryTheory.Subpresheaf.Equalizer Mathlib.CategoryTheory.Subpresheaf.Finite Mathlib.CategoryTheory.Subpresheaf.Image Mathlib.CategoryTheory.Subpresheaf.OfSection Mathlib.CategoryTheory.Subpresheaf.Sieves Mathlib.CategoryTheory.Subpresheaf.Subobject Mathlib.CategoryTheory.Subterminal Mathlib.CategoryTheory.Sums.Associator Mathlib.CategoryTheory.Sums.Basic Mathlib.CategoryTheory.Thin Mathlib.CategoryTheory.Topos.Classifier 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.Data.Set.FunctorToTypes Mathlib.Geometry.RingedSpace.Basic Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.GroupTheory.FreeGroup.NielsenSchreier 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.Order.Interval.Set.Final 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.ULift 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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Collaborator
|
Here are the benchmark results for commit 11db251. |
Collaborator
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 775ba62. |
Collaborator
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 55aba30. 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% |
2 files, Instructions +7.0⬝10⁹
2 files, Instructions +3.0⬝10⁹
3 files, Instructions +2.0⬝10⁹
13 files, Instructions +1.0⬝10⁹
46 files, Instructions -2.0⬝10⁹
38 files, Instructions -3.0⬝10⁹
15 files, Instructions -4.0⬝10⁹
13 files, Instructions -5.0⬝10⁹
18 files, Instructions -6.0⬝10⁹
10 files, Instructions -7.0⬝10⁹
5 files, Instructions -8.0⬝10⁹
4 files, Instructions -9.0⬝10⁹
7 files, Instructions -10.0⬝10⁹
7 files, Instructions -11.0⬝10⁹
5 files, Instructions -12.0⬝10⁹
4 files, Instructions -13.0⬝10⁹
9 files, Instructions -14.0⬝10⁹
2 files, Instructions -17.0⬝10⁹
6 files, Instructions -18.0⬝10⁹
2 files, Instructions -21.0⬝10⁹
2 files, Instructions -22.0⬝10⁹
4 files, Instructions -25.0⬝10⁹
3 files, Instructions -26.0⬝10⁹
2 files, Instructions -29.0⬝10⁹
|
Collaborator
|
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:
|
Collaborator
Author
|
One question I have is whether this is the right solution, or if this is something that can be improved in |
Collaborator
|
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. |
Collaborator
|
The most natural way to do this would be to make This will make Aesop try However, it'll also retry So for now, the approach used in this PR is probably optimal. |
Collaborator
|
Btw, might be worth trying |
Collaborator
Author
|
I think |
Collaborator
Author
|
To make |
Collaborator
|
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? |
Collaborator
Author
|
I think I found an underlying reason today for why the |
Collaborator
Author
|
Just to clear up the current status:
So there is quite a dependency chain going on 😅 |
kim-em
reviewed
Mar 31, 2025
Contributor
|
bors d+ |
Contributor
|
✌️ JovanGerb can now approve this pull request. To approve and merge a pull request, simply reply with |
Collaborator
Author
|
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 1, 2025
…21330) 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.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
aesop_cat attempt rfl before aesopaesop_cat attempt rfl before aesop
grunweg
added a commit
that referenced
this pull request
Jun 5, 2025
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR modifies the
aesop_cattactic so that it tries a proof byrflbefore doing the more expensiveaesoptactic.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
rfldoesn't have the same type as the expected type. Starting the proof withrefine id ?_` is a trick to make sure that the type matches exactly with the expected type.