chore(CategoryTheory): start using mk_concrete_category

[dagurtomas]

---

• depends on: feat(Tactic/CategoryTheory): concrete category boilerplate #38587
• depends on: fix(Topology/Category): make TopCat.Hom constructor private #39005

[github-actions]

PR summary f818ba367c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
1006 files Mathlib.Algebra.BrauerGroup.Defs Mathlib.Algebra.Category.AlgCat.Basic Mathlib.Algebra.Category.AlgCat.Limits Mathlib.Algebra.Category.AlgCat.Monoidal Mathlib.Algebra.Category.AlgCat.Symmetric Mathlib.Algebra.Category.BialgCat.Basic Mathlib.Algebra.Category.BialgCat.Monoidal Mathlib.Algebra.Category.BoolRing Mathlib.Algebra.Category.CoalgCat.Basic Mathlib.Algebra.Category.CoalgCat.ComonEquivalence Mathlib.Algebra.Category.CoalgCat.Monoidal Mathlib.Algebra.Category.CommAlgCat.Basic Mathlib.Algebra.Category.CommAlgCat.FiniteType Mathlib.Algebra.Category.CommAlgCat.Monoidal Mathlib.Algebra.Category.CommBialgCat Mathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Category.FGModuleCat.Abelian Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.Colimits Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.Adjunctions Mathlib.Algebra.Category.Grp.Basic Mathlib.Algebra.Category.Grp.Biproducts Mathlib.Algebra.Category.Grp.CartesianMonoidal Mathlib.Algebra.Category.Grp.Colimits Mathlib.Algebra.Category.Grp.EnoughInjectives 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.Images Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.Grp.Kernels Mathlib.Algebra.Category.Grp.LargeColimits Mathlib.Algebra.Category.Grp.LeftExactFunctor Mathlib.Algebra.Category.Grp.Limits Mathlib.Algebra.Category.Grp.Preadditive Mathlib.Algebra.Category.Grp.Shrink Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.Grp.Ulift Mathlib.Algebra.Category.Grp.Yoneda Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.Grp.Zero Mathlib.Algebra.Category.GrpWithZero Mathlib.Algebra.Category.HopfAlgCat.Basic Mathlib.Algebra.Category.HopfAlgCat.Monoidal Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.Descent Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting Mathlib.Algebra.Category.ModuleCat.Ext.Finite Mathlib.Algebra.Category.ModuleCat.Ext.HasExt Mathlib.Algebra.Category.ModuleCat.ExteriorPower Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.LeftResolution Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Localization Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Semi Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.ModuleCat.Stalk Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.ModuleCat.Topology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.Algebra.Category.ModuleCat.Ulift 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.MonCat.Shrink Mathlib.Algebra.Category.MonCat.Yoneda Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Category.Ring.Basic Mathlib.Algebra.Category.Ring.Colimits Mathlib.Algebra.Category.Ring.Constructions Mathlib.Algebra.Category.Ring.Epi Mathlib.Algebra.Category.Ring.EqualizerPushout Mathlib.Algebra.Category.Ring.FilteredColimits Mathlib.Algebra.Category.Ring.FinitePresentation Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Category.Ring.Limits Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Small Mathlib.Algebra.Category.Ring.Topology Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.Category.Ring.Under.Property Mathlib.Algebra.Category.Semigrp.Basic Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective Mathlib.Algebra.Homology.DerivedCategory.Ext.Map Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure Mathlib.Algebra.Homology.DerivedCategory.Fractions Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.KInjective Mathlib.Algebra.Homology.DerivedCategory.KProjective Mathlib.Algebra.Homology.DerivedCategory.Linear Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom Mathlib.Algebra.Homology.DerivedCategory.TStructure Mathlib.Algebra.Homology.EulerCharacteristic Mathlib.Algebra.Homology.Factorizations.CM5a Mathlib.Algebra.Homology.Factorizations.CM5b Mathlib.Algebra.Homology.HomotopyCategory.Acyclic Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.KInjective Mathlib.Algebra.Homology.HomotopyCategory.KProjective Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Homology.ModelCategory.Lifting Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Lie.Basis Mathlib.Algebra.Lie.Weights.IsSimple Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Algebra.Module.CharacterModule Mathlib.Algebra.Module.PID Mathlib.Algebra.Module.SpanRankOperations Mathlib.Algebra.Module.Torsion.PrimaryComponent Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.AlgClosed.Basic Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EffectiveEpi Mathlib.AlgebraicGeometry.EllipticCurve.LFunction Mathlib.AlgebraicGeometry.EllipticCurve.Reduction Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.Geometrically.Basic Mathlib.AlgebraicGeometry.Geometrically.Connected Mathlib.AlgebraicGeometry.Geometrically.Integral Mathlib.AlgebraicGeometry.Geometrically.Irreducible Mathlib.AlgebraicGeometry.Geometrically.Reduced Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Descent Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.FlatDescent Mathlib.AlgebraicGeometry.Morphisms.FlatMono Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.ConstantSheaf Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Fpqc Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.CechNerve Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.AlgebraicTopology.MooreComplex Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal Mathlib.AlgebraicTopology.SimplexCategory.Basic Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty Mathlib.AlgebraicTopology.SimplexCategory.Rev Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne Mathlib.AlgebraicTopology.SimplexCategory.Truncated Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialObject.Basic Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal Mathlib.AlgebraicTopology.SimplicialObject.Homotopy Mathlib.AlgebraicTopology.SimplicialObject.II Mathlib.AlgebraicTopology.SimplicialObject.Op Mathlib.AlgebraicTopology.SimplicialObject.Split Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.AlgebraicTopology.SimplicialSet.Boundary Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated Mathlib.AlgebraicTopology.SimplicialSet.CompStruct Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.AlgebraicTopology.SimplicialSet.Degenerate Mathlib.AlgebraicTopology.SimplicialSet.Dimension Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd Mathlib.AlgebraicTopology.SimplicialSet.Finite Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Homotopy Mathlib.AlgebraicTopology.SimplicialSet.HornColimits Mathlib.AlgebraicTopology.SimplicialSet.Horn Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices Mathlib.AlgebraicTopology.SimplicialSet.Nonempty Mathlib.AlgebraicTopology.SimplicialSet.Op Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.AlgebraicTopology.SimplicialSet.PiZero Mathlib.AlgebraicTopology.SimplicialSet.Presentable Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.RegularEpi Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism Mathlib.AlgebraicTopology.SimplicialSet.Simplices Mathlib.AlgebraicTopology.SimplicialSet.Skeleton Mathlib.AlgebraicTopology.SimplicialSet.Splitting Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex Mathlib.AlgebraicTopology.SimplicialSet.Subdivision Mathlib.AlgebraicTopology.SimplicialSet.TopAdj Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.AlgebraicTopology.SingularHomology.HomologyZero Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance Mathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Injective.Ext Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Ext Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Action.Basic Mathlib.CategoryTheory.Action.Concrete Mathlib.CategoryTheory.Action.Continuous Mathlib.CategoryTheory.Action.Limits Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Action Mathlib.CategoryTheory.Adhesive.Basic Mathlib.CategoryTheory.Adhesive.Over Mathlib.CategoryTheory.Adhesive.Subobject Mathlib.CategoryTheory.Adhesive Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Category.Cat.Colimit Mathlib.CategoryTheory.CofilteredSystem Mathlib.CategoryTheory.EffectiveEpi.Extensive Mathlib.CategoryTheory.Extensive Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Galois.Decomposition Mathlib.CategoryTheory.Galois.Equivalence Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Galois.Topology Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory Mathlib.CategoryTheory.Groupoid.Grpd.Basic Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy Mathlib.CategoryTheory.Limits.Shapes.SingleObj Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_ Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_ Mathlib.CategoryTheory.Monoidal.Cartesian.Grp Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_ Mathlib.CategoryTheory.Monoidal.Cartesian.Mon Mathlib.CategoryTheory.Monoidal.Cartesian.Normal Mathlib.CategoryTheory.Monoidal.Cartesian.Over Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda Mathlib.CategoryTheory.Monoidal.CommGrp_ Mathlib.CategoryTheory.Monoidal.Grp_ Mathlib.CategoryTheory.Monoidal.Grp Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp Mathlib.CategoryTheory.Monoidal.Ring Mathlib.CategoryTheory.MorphismProperty.CommaSites Mathlib.CategoryTheory.Preadditive.CommGrp_ Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Preadditive.Mat Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.RegularCategory.Basic Mathlib.CategoryTheory.SingleObj 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.ExtensiveColimits 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.ConstantSheaf Mathlib.CategoryTheory.Sites.CoversTop.Over Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime Mathlib.CategoryTheory.Sites.Descent.DescentData Mathlib.CategoryTheory.Sites.Descent.IsPrestack Mathlib.CategoryTheory.Sites.Descent.IsStack Mathlib.CategoryTheory.Sites.Descent.Precoverage Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.LocalProperties Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.Point.Category Mathlib.CategoryTheory.Sites.Point.Comap Mathlib.CategoryTheory.Sites.Point.Conservative Mathlib.CategoryTheory.Sites.Point.IsMonoidalW Mathlib.CategoryTheory.Sites.Point.Map Mathlib.CategoryTheory.Sites.Point.Monoidal Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered Mathlib.CategoryTheory.Sites.Point.Over Mathlib.CategoryTheory.Sites.Point.Presheaf Mathlib.CategoryTheory.Sites.Point.Skyscraper Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver Mathlib.CategoryTheory.Sites.Pullback Mathlib.CategoryTheory.Sites.RegularEpi Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.Cech Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.SubcanonicalOver Mathlib.CategoryTheory.Topos.Sheaf Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.Opposite.OpOp Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Combinatorics.Configuration Mathlib.Combinatorics.Hall.Basic Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.Combinatorics.SimpleGraph.Hall Mathlib.Condensed.AB Mathlib.Condensed.Basic Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Discrete.Module Mathlib.Condensed.EffectiveEpi Mathlib.Condensed.Epi Mathlib.Condensed.Equivalence Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.EffectiveEpi Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.Instances Mathlib.Condensed.Light.InternallyProjective Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.Monoidal Mathlib.Condensed.Light.Sequence Mathlib.Condensed.Light.Small Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison Mathlib.FieldTheory.Galois.IsGaloisGroup Mathlib.FieldTheory.Galois.NormalBasis Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.FieldTheory.RatFunc.IntermediateField Mathlib.FieldTheory.RatFunc.Luroth Mathlib.FieldTheory.RatFunc.Valuation Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.RingedSpace.Basic Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.GroupTheory.FreeGroup.NielsenSchreier Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.LinearAlgebra.RootSystem.BaseChange Mathlib.LinearAlgebra.RootSystem.BaseExists Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.RootSystem.CartanMatrix Mathlib.LinearAlgebra.RootSystem.Chain Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.RootSystem.Finite.G2 Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.LinearAlgebra.RootSystem.Irreducible Mathlib.LinearAlgebra.RootSystem.IsValuedIn Mathlib.LinearAlgebra.RootSystem.Reduced Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.MeasureTheory.Category.MeasCat Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LSeries.ZetaZeros Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.MahlerMeasure Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion.FinitePlace Mathlib.NumberTheory.NumberField.Completion.Ramification Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind Mathlib.NumberTheory.NumberField.InfiniteAdeleRing Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.Padics.HeightOneSpectrum Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.HilbertTheory Mathlib.NumberTheory.RamificationInertia.Inertia Mathlib.NumberTheory.RamificationInertia.Ramification Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.NumberTheory.RatFunc.Ostrowski 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.PartOrdEmb Mathlib.Order.Category.PartOrd Mathlib.Order.Category.Preord Mathlib.Order.Category.Semilat Mathlib.Order.NonemptyFiniteChains Mathlib.RepresentationTheory.Action Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FinGroupCharZero Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Homological.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro Mathlib.RepresentationTheory.Homological.GroupHomology.Basic Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro Mathlib.RepresentationTheory.Homological.Resolution Mathlib.RepresentationTheory.Induced Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Rep.Basic Mathlib.RepresentationTheory.Rep.Iso Mathlib.RepresentationTheory.Rep.Res Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.Algebraic.StronglyTranscendental Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.GaussLemma Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.Etale.Descent Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Etale.QuasiFinite Mathlib.RingTheory.Finiteness.Descent Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.FaithfullyFlat.Descent Mathlib.RingTheory.Flat.Rank Mathlib.RingTheory.Flat.Tensor Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.Ideal.AssociatedPrime.Localization Mathlib.RingTheory.Ideal.Int Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.Ideal.Pure Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.Invariant.Basic Mathlib.RingTheory.Invariant.Profinite Mathlib.RingTheory.KrullDimension.Module Mathlib.RingTheory.KrullDimension.Regular Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.InjectiveDimension Mathlib.RingTheory.LocalProperties.Injective Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.ProjectiveDimension Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalProperties.Semilocal Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.LocalRing.ResidueField.Polynomial Mathlib.RingTheory.Localization.AtPrime.Extension Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.Morita.Matrix Mathlib.RingTheory.OrderOfVanishing.Noetherian Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.QuasiFinite.Polynomial Mathlib.RingTheory.RamificationInertia.Inertia Mathlib.RingTheory.RamificationInertia.Ramification Mathlib.RingTheory.Regular.Category Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.Regular.LinearMap Mathlib.RingTheory.Regular.ProjectiveDimension Mathlib.RingTheory.RegularLocalRing.Defs Mathlib.RingTheory.RingHom.Bijective Mathlib.RingTheory.RingHom.EssFiniteType Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.LocallyStandardSmooth Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.OpenImmersion Mathlib.RingTheory.RingHom.QuasiFinite Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.Smooth.Fiber Mathlib.RingTheory.Smooth.Field Mathlib.RingTheory.Smooth.Flat Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.Quotient Mathlib.RingTheory.Smooth.StandardSmoothOfFree Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Spectrum.Prime.Module Mathlib.RingTheory.Support Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight Mathlib.RingTheory.TotallySplit Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Unramified.Dedekind Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.LocalStructure Mathlib.RingTheory.Unramified.Locus Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.RingTheory.Valuation.Discrete.RankOne Mathlib.RingTheory.ZariskisMainTheorem Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.Algebra.Ring.Compact Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.CompHaus.Frm Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Topology.Category.CompHausLike.Cartesian Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.Category.CompHausLike.Limits Mathlib.Topology.Category.CompHausLike.SigmaComparison Mathlib.Topology.Category.CompactlyGenerated Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Category.FinTopCat Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.Cartesian Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.LightProfinite.Injective Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Locale Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Category.Profinite.Nobeling.Basic Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Span Mathlib.Topology.Category.Profinite.Nobeling.Successor Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Sequential Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.Stonean.Limits Mathlib.Topology.Category.TopCat.Adjunctions Mathlib.Topology.Category.TopCat.Basic Mathlib.Topology.Category.TopCat.EffectiveEpi Mathlib.Topology.Category.TopCat.EpiMono Mathlib.Topology.Category.TopCat.GrothendieckTopology 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.Monoidal Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.Topology.Category.TopCat.Opens Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.Category.TopCat.ULift Mathlib.Topology.Category.TopCat.Yoneda Mathlib.Topology.Category.TopCommRingCat Mathlib.Topology.Category.TopPair Mathlib.Topology.Category.UniformSpace Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.Convenient.Category Mathlib.Topology.Convenient.Localization Mathlib.Topology.Gluing Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Topology.Homotopy.Lifting Mathlib.Topology.Homotopy.TopCat.Basic Mathlib.Topology.Homotopy.TopCat.Path Mathlib.Topology.Homotopy.TopCat.ToSSet Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy Mathlib.Topology.Order.Category.AlexDisc Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.Sheaves.Abelian Mathlib.Topology.Sheaves.AddCommGrpCat Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.Sheaves.Flasque Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.Points 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 Mathlib.Topology.Subpath	1
Mathlib.Tactic.CategoryTheory.MkConcreteCategory (new file)	292

---

Declarations diff

+ CustomOfHomData
++ AdditiveTestCat
++ Fun
++ Fun.comp
++ Fun.id
++ ModuleTestCat
++ MultiplicativeTestCat
++ TestCat
++ instCoeSort
++ instance (X Y : TestCat.{u}) : FunLike (Fun X Y) X.α Y.α
++ instance : CoeSort (ModuleTestCat.{v} R) (Type v)
++++ morphism
++++ of
- AddCommGrpCat.Hom
- AddCommMonCat.Hom
- AddGrpCat.Hom
- AddMagmaCat.Hom
- AddMonCat.Hom
- AddSemigrp.Hom
- CommGrpCat.Hom
- CommMonCat.Hom
- GrpCat.Hom
- MagmaCat.Hom
- MonCat.Hom
- ProfiniteAddGrp.Hom
- ProfiniteGrp.Hom
- ProfiniteGrp.Hom.hom
- ProfiniteGrp.ofHom
- Semigrp.Hom
- instance : Category (AlgCat.{v} R)
- instance : Category (CommAlgCat.{v} R)
- instance : Category (CommBialgCat.{v} R)
- instance : Category (Rep.{w} k G)
- instance : Category (TopModuleCat R)
- instance : Category BddDistLat.{u}
- instance : Category BddOrd.{u}
- instance : Category BoolAlg.{u}
- instance : Category BoolRing
- instance : Category CommGrpCat.{u}
- instance : Category CommMonCat.{u}
- instance : Category CommRingCat
- instance : Category CommSemiRingCat
- instance : Category DistLat.{u}
- instance : Category FinBddDistLat.{u}
- instance : Category Frm.{u}
- instance : Category GrpCat.{u}
- instance : Category HeytAlg.{u}
- instance : Category Lat.{u}
- instance : Category LinOrd.{u}
- instance : Category MagmaCat.{u}
- instance : Category MonCat.{u}
- instance : Category PartOrd.{u}
- instance : Category PartOrdEmb.{u}
- instance : Category Preord.{u}
- instance : Category ProfiniteGrp
- instance : Category RingCat
- instance : Category SemiRingCat
- instance : Category Semigrp.{u}
- instance : Category TopCat
- instance : ConcreteCategory (AlgCat.{v} R) (· →ₐ[R] ·)
- instance : ConcreteCategory (CommAlgCat.{v} R) (· →ₐ[R] ·)
- instance : ConcreteCategory (CommBialgCat.{v} R) (· →ₐc[R] ·)
- instance : ConcreteCategory (ModuleCat.{v} R) (· →ₗ[R] ·)
- instance : ConcreteCategory (Rep.{w} k G) (fun A B ↦ A.ρ.IntertwiningMap B.ρ)
- instance : ConcreteCategory (SemimoduleCat.{v} R) (· →ₗ[R] ·)
- instance : ConcreteCategory (TopModuleCat R) (· →L[R] ·)
- instance : ConcreteCategory BddDistLat (BoundedLatticeHom · ·)
- instance : ConcreteCategory BddLat (BoundedLatticeHom · ·)
- instance : ConcreteCategory BddOrd (BoundedOrderHom · ·)
- instance : ConcreteCategory BoolAlg (BoundedLatticeHom · ·)
- instance : ConcreteCategory BoolRing (· →+* ·)
- instance : ConcreteCategory CommGrpCat (· →* ·)
- instance : ConcreteCategory CommMonCat (· →* ·)
- instance : ConcreteCategory DistLat (LatticeHom · ·)
- instance : ConcreteCategory FinBddDistLat (BoundedLatticeHom · ·)
- instance : ConcreteCategory Frm (FrameHom · ·)
- instance : ConcreteCategory GrpCat (· →* ·)
- instance : ConcreteCategory HeytAlg (HeytingHom · ·)
- instance : ConcreteCategory Lat (LatticeHom · ·)
- instance : ConcreteCategory LinOrd (· →o ·)
- instance : ConcreteCategory MagmaCat (· →ₙ* ·)
- instance : ConcreteCategory MonCat (· →* ·)
- instance : ConcreteCategory PartOrd (· →o ·)
- instance : ConcreteCategory PartOrdEmb (· ↪o ·)
- instance : ConcreteCategory Preord (· →o ·)
- instance : ConcreteCategory ProfiniteGrp (fun X Y => X →ₜ* Y)
- instance : ConcreteCategory SemiNormedGrp (NormedAddGroupHom · ·)
- instance : ConcreteCategory Semigrp (· →ₙ* ·)
- instance : ConcreteCategory UniformSpaceCat ({ f : · → · // UniformContinuous f })
- instance : ConcreteCategory.{u} CommRingCat (fun R S => R →+* S)
- instance : ConcreteCategory.{u} CommSemiRingCat (fun R S => R →+* S)
- instance : ConcreteCategory.{u} RingCat (fun R S => R →+* S)
- instance : ConcreteCategory.{u} SemiRingCat (fun R S => R →+* S)
- instance : ConcreteCategory.{u} TopCat (fun X Y => C(X, Y))
- instance : LargeCategory.{u} BddLat
- instance : LargeCategory.{u} SemiNormedGrp
- instance : LargeCategory.{u} UniformSpaceCat.{u}
-- moduleCategory
---------------------------- Hom
-------------------------------- Hom.Simps.hom
-------------------------------- ofHom_hom
--------------------------------- hom_ofHom
---------------------------------- Hom.hom
---------------------------------- hom_comp
---------------------------------- hom_id
---------------------------------- ofHom

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Tactic/CategoryTheory): concrete category boilerplate #38587
• fix(Topology/Category): make TopCat.Hom constructor private #39005
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[dagurtomas]

!radar

[leanprover-radar]

Benchmark results for 15a17a8 against f818ba3 are in. No significant results found. @dagurtomas

• 🟥 build//instructions: +33.4G (+0.02%)

No significant changes detected.

[dagurtomas]

!radar

[leanprover-radar]

Benchmark results for aa0f9ca against f818ba3 are in. No significant results found. @dagurtomas

• ✅ build//instructions: -838.9M (-0.00%)

No significant changes detected.