mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Adjunction
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverseSymmOfFunctor : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] (E : C ≌ D) [inst_12 : E.functor.CommShift ℤ]
  [h : E.functor.IsTriangulated], E.symm.inverse.IsTriangulated
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.final_op_of_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial], F.op.Final
-- Mathlib.CategoryTheory.Localization.Resolution
/-- a morphism from an object of the form `Φ.functor.obj X₁`  -/
CategoryTheory.LocalizerMorphism.LeftResolution.w : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → (self : Φ.LeftResolution X₂) → Φ.functor.obj self.X₁ ⟶ X₂
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instGroup : {α : Type u_1} → [Group α] → Group αᵐᵒᵖ
-- Mathlib.Analysis.Convex.Basic
AntitoneOn.convex_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, AntitoneOn f s → Convex 𝕜 s → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ f x < r}
-- Aesop.Saturate
_private.Aesop.Saturate.0.Aesop.Stateful.saturateCore.go : Aesop.LocalRuleSet →
  Std.HashMap Lean.FVarId ℕ →
    Aesop.ForwardState → Aesop.Stateful.Queue✝ → Std.HashSet Lean.FVarId → Lean.MVarId → Aesop.SaturateM Lean.MVarId
-- Mathlib.Computability.TuringMachine.Computable
Turing.FinTM2.mk : {K : Type} →
  [kDecidableEq : DecidableEq K] →
    [kFin : Fintype K] →
      (k₀ : K) →
        K →
          (Γ : K → Type) →
            (Λ : Type) →
              Λ →
                [ΛFin : Fintype Λ] →
                  (σ : Type) →
                    σ → [σFin : Fintype σ] → [Γk₀Fin : Fintype (Γ k₀)] → (Λ → Turing.TM2.Stmt Γ Λ σ) → Turing.FinTM2
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.nextConts.eq_1 : ∀ {K : Type u_2} [inst : DivisionRing K] (a b : K) (ppred pred : GenContFract.Pair K),
  GenContFract.nextConts a b ppred pred =
    { a := GenContFract.nextNum a b ppred.a pred.a, b := GenContFract.nextDen a b ppred.b pred.b }
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_pos_iff_exists_adj : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], 0 < G.degree v ↔ ∃ w, G.Adj v w
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- Evidence that the arbitrary choice of cone provided by `weakLimit.cone F`
is a weak limit cone.  -/
CategoryTheory.Limits.weakLimit.isWeakLimit : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasWeakLimit F] →
            CategoryTheory.Limits.IsWeakLimit (CategoryTheory.Limits.weakLimit.cone F)
-- Mathlib.Data.Set.Lattice.Image
Set.image_iInter₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {f : α → β},
  Function.Bijective f → ∀ (s : (i : ι) → κ i → Set α), f '' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f '' s i j
-- Mathlib.Topology.Compactification.StoneCech
/-- `pure : α → Ultrafilter α` defines a dense inducing of `α` in `Ultrafilter α`.  -/
isDenseInducing_pure : ∀ {α : Type u}, IsDenseInducing pure
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.hasSum_symmetricIoc_int_iff : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : ℤ → α} {a : α},
  HasSum f a (SummationFilter.symmetricIoc ℤ) ↔
    Filter.Tendsto (fun N => ∑ n ∈ Finset.Ioc (-↑N) ↑N, f n) Filter.atTop (nhds a)
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.norm_alternatizeUncurryFinCLM_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ},
  ‖ContinuousAlternatingMap.alternatizeUncurryFinCLM 𝕜 E F‖ ≤ ↑n + 1
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr : ∀ (x : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x).hom.τr =
    CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardId (Opposite.unop x.as)).inv
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.congr_simp : ∀ (R : Type u_1) (M : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [inst_6 : IsScalarTower R A M] (x x_1 : A),
  x = x_1 → Module.AEval R M x = Module.AEval R M x_1
-- Mathlib.CategoryTheory.Localization.FiniteProducts
/-- Auxiliary definition for `Localization.preservesProductsOfShape`.  -/
CategoryTheory.Localization.HasProductsOfShapeAux.isLimitMapCone : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [L.IsLocalization W] →
              (J : Type) →
                [inst_3 : CategoryTheory.Limits.HasProductsOfShape J C] →
                  [W.IsStableUnderProductsOfShape J] →
                    [W.ContainsIdentities] →
                      [Finite J] →
                        (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) →
                          CategoryTheory.Limits.IsLimit (L.mapCone (CategoryTheory.Limits.limit.cone F))
-- Mathlib.Algebra.Order.Sub.Defs
OrderedSub.mk : ∀ {α : Type u_2} [inst : LE α] [inst_1 : Add α] [inst_2 : Sub α], (∀ (a b c : α), a - b ≤ c ↔ a ≤ c + b) → OrderedSub α
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
/-- The global evaluation map from `Γ(X, ⊤)` to the residue field at `x`.  -/
AlgebraicGeometry.LocallyRingedSpace.Γevaluation : (X : AlgebraicGeometry.LocallyRingedSpace) → (x : ↑X.toTopCat) → X.presheaf.obj (Opposite.op ⊤) ⟶ X.residueField x
-- Mathlib.Algebra.Group.Ext
AddLeftCancelMonoid.ext_iff : ∀ {M : Type u} {m₁ m₂ : AddLeftCancelMonoid M}, m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd
-- Init.Data.Nat.Power2.Lemmas
Nat.ne_zero_and_sub_one_eq_zero_iff_isPowerOfTwo : ∀ {n : ℕ}, n ≠ 0 ∧ n &&& n - 1 = 0 ↔ n.isPowerOfTwo
-- Lean.Compiler.MetaAttr
/-- Marks a declaration to be exported for interpretation.  -/
Lean.setDeclMeta : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.GroupTheory.Coset.Card
QuotientAddGroup.fintype : {α : Type u_1} →
  [inst : AddGroup α] →
    [Fintype α] → (s : AddSubgroup α) → [DecidableRel ⇑(QuotientAddGroup.leftRel s)] → Fintype (α ⧸ s)
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.dimension_reindex : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ),
  (P.reindex e f).dimension = P.dimension
-- Mathlib.Algebra.Group.Shrink
Shrink.instMulAction.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Monoid M] [inst_2 : MulAction M α],
  Shrink.instMulAction = Equiv.mulAction M (equivShrink α).symm
-- Mathlib.Topology.MetricSpace.DilationEquiv
/-- Identity map as a `DilationEquiv`.  -/
DilationEquiv.refl : (X : Type u_4) → [inst : PseudoEMetricSpace X] → X ≃ᵈ X
-- Std.Do.Internal.Ensures.Lemmas
/-- `MonadAttach.attach`, retagged with `MayReturn` proofs, witnesses `IsAttach`.  -/
Std.Do.Internal.IsAttach.of_attach : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : LawfulMonad m] [inst_2 : MonadAttach m]
  [inst_3 : LawfulMonadAttach m],
  Std.Do.Internal.IsAttach fun {x} x_1 => do
    let x_2 ← MonadAttach.attach x_1
    match x_2 with
      | ⟨a, h⟩ => pure ⟨a, ⋯⟩
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.OplaxMonoidal]
  [inst_5 : G.LaxMonoidal] [adj.IsMonoidal] (X Y : C),
  CategoryTheory.CategoryStruct.comp (adj.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
      (G.map (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app X) (adj.unit.app Y))
      (CategoryTheory.Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y))
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LevelMVarErrorInfo.mk.sizeOf_spec : ∀ (lctx : Lean.LocalContext) (expr : Lean.Expr) (ref : Lean.Syntax) (msgData? : Option Lean.MessageData),
  sizeOf { lctx := lctx, expr := expr, ref := ref, msgData? := msgData? } =
    1 + sizeOf lctx + sizeOf expr + sizeOf ref + sizeOf msgData?
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.endHom_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {P : Type u_5} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  [inst_7 : Module S P] [inst_8 : IsScalarTower R S P] {α : M →ₗ[R] P} (j : IsBaseChange S α) (f : M →ₗ[R] M) (p : P),
  (j.endHom f) p = ((LinearMap.liftBaseChangeEquiv S) (α ∘ₗ f)) (j.equiv.symm p)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMulForallForallStar : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A],
  CanLift (Set A) (NonUnitalStarSubalgebra R A) SetLike.coe fun s =>
    0 ∈ s ∧
      (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
        (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧
          (∀ (r : R) {x : A}, x ∈ s → r • x ∈ s) ∧ ∀ {x : A}, x ∈ s → star x ∈ s
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.forget₂_module_obj : ∀ (R : Type u) [inst : CommRing R] (X : AlgCat R),
  (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).obj X = ModuleCat.of R ↑X
-- Std.Http.Data.URI.Config
/-- Maximum length of the userinfo component (username and password each), in bytes.
 -/
Std.Http.URI.Config.maxUserInfoLength : Std.Http.URI.Config → ℕ
-- Mathlib.Algebra.Category.Grp.FiniteGrp
/-- The category of finite groups.  -/
FiniteGrp : Type (u + 1)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects limits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.leftOp : Cᵒᵖ ⥤ D` reflects
colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.reflectsColimit_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsLimit K.leftOp F],
  CategoryTheory.Limits.ReflectsColimit K F.leftOp
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.IsComplex.cokerToKer.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n)
  [inst_2 : CategoryTheory.Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
  [inst_3 : CategoryTheory.Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)], hS.cokerToKer k hk = hS.cokerToKer k hk
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` creates limits of `K.leftOp : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : Cᵒᵖ ⥤ D`
creates colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.createsColimitOfRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J Cᵒᵖ) →
              (F : CategoryTheory.Functor Cᵒᵖ D) →
                [CategoryTheory.CreatesLimit K.leftOp F.rightOp] → CategoryTheory.CreatesColimit K F
-- Init.Data.List.Impl
List.dropLast_eq_dropLastTR : @List.dropLast = @List.dropLastTR
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal],
  CategoryTheory.NatTrans.IsMonoidal e.counit
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.head?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Min α] [inst_1 : LE α]
  [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] [Std.LawfulEqCmp cmp],
  t.WF → t.toList.head? = t.min?
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.isPushout : ∀ {X Y : SSet} (i : X ⟶ Y) (d : ℕ),
  CategoryTheory.IsPushout (SSet.relativeCellComplexOfMono.t i d) (SSet.relativeCellComplexOfMono.l i d)
    (SSet.relativeCellComplexOfMono.r i d) (SSet.relativeCellComplexOfMono.b i d)
-- Init.Data.Nat.Lemmas
Nat.log2_two_pow : ∀ {n : ℕ}, (2 ^ n).log2 = n
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.map_extend_nhds_of_mem_interior_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M},
  x ∈ f.source →
    ↑(f.extend I) x ∈ interior (Set.range ↑I) → Filter.map (↑(f.extend I)) (nhds x) = nhds (↑(f.extend I) x)
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The divisor of a constant function is `0`.
 -/
MeromorphicOn.divisor_ofNat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} (n : ℕ), MeromorphicOn.divisor (OfNat.ofNat n) U = 0
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.HomRel.CompClosure.intro : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {r : HomRel C} {s t : C} (a b : C) (f : s ⟶ a)
  (m₁ m₂ : a ⟶ b) (g : b ⟶ t),
  r m₁ m₂ →
    CategoryTheory.HomRel.CompClosure r (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp m₁ g))
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp m₂ g))
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instIsScalarTower_1 : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} {P : Type u_4}
  [inst_1 : Ring S] [inst_2 : SMul P S] [inst_3 : SMul R S] [inst_4 : SMul P R] [IsScalarTower P R S]
  (v : Valuation S Γ₀), IsScalarTower P R (WithVal v)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_not_contains_map_fst : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  Std.Internal.List.containsKey k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) =
    (Std.Internal.List.containsKey k l₁ && !Std.Internal.List.containsKey k l₂)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Constructor for morphisms in `Grp C`.  -/
CategoryTheory.Grp.homMk'' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A B : CategoryTheory.Grp C} →
        (f : A.X ⟶ B.X) →
          autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one)
              CategoryTheory.Grp.homMk''._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
                    CategoryTheory.MonObj.mul)
                CategoryTheory.Grp.homMk''._auto_3 →
              (A ⟶ B)
-- Mathlib.CategoryTheory.Sites.Preserves
CategoryTheory.Presieve.piComparison_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) {α : Type u_1}
  [inst_1 : Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c),
  have this := ⋯;
  (CategoryTheory.Limits.piComparison F fun x => Opposite.op (X x)) =
    CategoryTheory.CategoryStruct.comp
      (F.map
        (CategoryTheory.Limits.opCoproductIsoProduct' hc
            (CategoryTheory.Limits.productIsProduct fun x => Opposite.op (X x))).inv)
      (CategoryTheory.Equalizer.Presieve.Arrows.forkMap F X c.inj)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The type of AddMonoid homomorphisms satisfying the characteristic predicate: if `f : M →+ N`
satisfies this predicate, then `N` is isomorphic to the localization of `M` at `S`.  -/
AddSubmonoid.LocalizationMap : {M : Type u_1} → [inst : AddCommMonoid M] → AddSubmonoid M → (N : Type u_2) → [AddCommMonoid N] → Type (max u_1 u_2)
-- Mathlib.Computability.RecursiveIn
RecursiveIn.iff_nat : ∀ {f : ℕ →. ℕ} {O : Set (ℕ →. ℕ)}, RecursiveIn O f ↔ Nat.RecursiveIn O f
-- Std.Async.System
/-- Gets information about the CPU cores.
 -/
Std.Async.System.getCPUInfo : IO (Array Std.Async.System.CPUInfo)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsInt.to_isRat : ∀ {α : Type u_1} [inst : Ring α] {a : α} {n : ℤ}, Mathlib.Meta.NormNum.IsInt a n → Mathlib.Meta.NormNum.IsRat a n 1
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.id_mem_of_nonempty_isotropy : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C),
  ∀ c ∈ S.objs, CategoryTheory.CategoryStruct.id c ∈ S.arrows c c
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.opEquiv_apply : ∀ {X : SSet} (x : X.op.S), SSet.S.opEquiv x = { dim := x.dim, simplex := SSet.opObjEquiv x.simplex }
-- Mathlib.Analysis.Complex.UpperHalfPlane.Exp
UpperHalfPlane.norm_qParam_lt_one : ∀ (n : ℕ) [NeZero n] (τ : UpperHalfPlane), ‖Function.Periodic.qParam ↑n ↑τ‖ < 1
-- Init.Prelude
/-- All the name components `(<module_name>.<scopes>)*` from the imports
concatenated together.  -/
Lean.MacroScopesView.imported : Lean.MacroScopesView → Lean.Name
-- Mathlib.Order.BoundedOrder.Basic
botOrderOrNoBotOrder.eq_1 : ∀ (α : Type u_1) [inst : LE α],
  botOrderOrNoBotOrder α =
    if H : ∀ (a : α), ∃ b, ¬a ≤ b then PSum.inr ⋯ else PSum.inl { bot := Classical.choose ⋯, bot_le := ⋯ }
-- Batteries.Data.List.Basic
List.replaceFTR.eq_1 : ∀ {α : Type u_1} (f : α → Option α) (l : List α), List.replaceFTR f l = List.replaceFTR.go f l #[]
-- Lean.Meta.Basic
/-- `isInstance` is true if the parameter type is a class instance.  -/
Lean.Meta.ParamInfo.isInstance : Lean.Meta.ParamInfo → Bool
-- Mathlib.Order.Concept
/-- Swap the sets of a concept to make it a concept of the dual context.  -/
Concept.swap : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → Concept α β r → Concept β α (Function.swap r)
-- Mathlib.Order.Max
not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] (a : α), ¬IsMin a
-- Mathlib.RingTheory.PolynomialAlgebra
instIsPushoutPolynomial : ∀ (R : Type u_1) [inst : CommSemiring R] {S : Type u_4} [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.IsPushout R S (Polynomial R) (Polynomial S)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.mem_zeroLocus : ∀ {R : Type u} [inst : CommSemiring R] (x : PrimeSpectrum R) (s : Set R), x ∈ PrimeSpectrum.zeroLocus s ↔ s ⊆ ↑x.asIdeal
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- A nilpotent endomorphism has nilpotent eigenvalues.

See also `LinearMap.isNilpotent_trace_of_isNilpotent`.  -/
Module.End.HasUnifEigenvalue.isNilpotent_of_isNilpotent : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] {f : Module.End R M}, IsNilpotent f → ∀ {μ : R}, f.HasUnifEigenvalue μ 1 → IsNilpotent μ
-- Mathlib.Tactic.ClearExcept
/-- Clears all hypotheses from a goal except those in the preserve list, class instances, and
auxiliary declarations (e.g. recursive hypotheses).  -/
Lean.Elab.Tactic.clearExcept : Array Lean.FVarId → Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Topology.Order.IntermediateValue
/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and for any `a ≤ x < y ≤ b`, `x ∈ s`, the set `s ∩ (x, y]`
is not empty, then `[a, b] ⊆ s`.  -/
IsClosed.Icc_subset_of_forall_exists_gt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {a b : α}
  {s : Set α},
  IsClosed (s ∩ Set.Icc a b) →
    a ∈ s → (∀ x ∈ s ∩ Set.Ico a b, ∀ y ∈ Set.Ioi x, (s ∩ Set.Ioc x y).Nonempty) → Set.Icc a b ⊆ s
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.apply_smulCommClass' : ∀ {R : Type u_1} {S : Type u_4} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : SMul S R] [inst_4 : SMul S M] [IsScalarTower S R M], SMulCommClass (M ≃ₗ[R] M) S M
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_zero : ∀ (x : ℕ), x ||| 0 = x
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimitsOfShape_opposite_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J],
  CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ Cᵒᵖ ↔ CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.Algebra.Group.AddChar
AddChar.prod_apply : ∀ {ι : Type u_1} {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (s : Finset ι)
  (ψ : ι → AddChar A M) (a : A), (∏ i ∈ s, ψ i) a = ∏ i ∈ s, (ψ i) a
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.finsuppAntidiag_mono : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] {s t : Finset ι}, s ⊆ t → ∀ (n : μ), s.finsuppAntidiag n ⊆ t.finsuppAntidiag n
-- Init.Data.Dyadic.Basic
Dyadic.blt.eq_2 : ∀ (n k : ℤ) (hn : n % 2 = 1), Dyadic.zero.blt (Dyadic.ofOdd n k hn) = decide (0 < n)
-- ProofWidgets.Component.PenroseDiagram
/-- Abbreviation for backwards-compatibility.  -/
ProofWidgets.PenroseDiagram : ProofWidgets.Component ProofWidgets.Penrose.DiagramProps
-- Mathlib.RingTheory.Flat.Rank
RingHom.finrank_algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).finrank = Module.rankAtStalk S
-- Lean.DocString.Extension
Lean.ElabBlock.deferred.injEq : ∀ (index index_1 : ℕ), (Lean.ElabBlock.deferred index = Lean.ElabBlock.deferred index_1) = (index = index_1)
-- Mathlib.Data.List.Basic
List.getLastI.eq_3 : ∀ {α : Type u_1} [inst : Inhabited α] (head b : α), [head, b].getLastI = b