mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_add_natCast : ∀ {x : ℝ} (m : ℕ), Irrational (x + ↑m) → Irrational x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGT.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β)
  (l r : Std.DTreeMap.Internal.Impl α fun x => β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.Const.getEntryGT k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    if hkky : compare k ky = Ordering.lt then Std.DTreeMap.Internal.Impl.Const.getEntryGTD k l (ky, y)
    else Std.DTreeMap.Internal.Impl.Const.getEntryGT k r ⋯ ⋯
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.exists_eq_zpow_of_isSquare : ∀ {R : Type u} [inst : Field R] [IsRealClosed R] {x : R}, IsSquare x → ∀ {k : ℤ}, k ≠ 0 → ∃ r, x = r ^ k
-- Mathlib.Order.Filter.Cofinite
/-- If `α` is a preorder with no bottom element, then `atBot ≤ cofinite`.  -/
Filter.atBot_le_cofinite : ∀ {α : Type u_2} [inst : Preorder α] [NoBotOrder α], Filter.atBot ≤ Filter.cofinite
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given Localization maps `f : M →* N, k : P →* Q` for Submonoids `S, T` respectively, if a
`CommMonoid` homomorphism `g : M →* P` induces a `f.map hy k : N →* Q`, then for all `z : N`,
we have `f.map hy k z * k (g y) = k (g x)` where `x : M, y ∈ S` are such that
`z * f y = f x`.  -/
Submonoid.LocalizationMap.map_mul_right : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} (z : N),
  (f.map hy k) z * k (g ↑(f.sec z).2) = k (g (f.sec z).1)
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_of_le_castSucc : ∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i ≤ p.castSucc), p.predAbove i = i.castPred ⋯
-- Mathlib.Topology.Algebra.Group.Basic
vadd_connectedComponent : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] (g h : G),
  g +ᵥ connectedComponent h = connectedComponent (g + h)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHintParams : Lean.ToJson Lean.Lsp.InlayHintParams
-- Mathlib.MeasureTheory.Category.MeasCat
MeasCat.instInhabited : Inhabited MeasCat
-- Mathlib.Analysis.InnerProductSpace.OfNorm
/-- **Fréchet–von Neumann–Jordan Theorem**. A normed space `E` whose norm satisfies the
parallelogram identity can be given a compatible inner product. Do
`casesI nonempty_innerProductSpace 𝕜 E` to locally upgrade `InnerProductSpaceable E` to
`InnerProductSpace 𝕜 E`.  -/
nonempty_innerProductSpace : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] (E : Type u_2) [inst_1 : NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [InnerProductSpaceable E], Nonempty (InnerProductSpace 𝕜 E)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.preimage_symm_preimage : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (S : Set A), ⇑e ⁻¹' ⇑e.symm ⁻¹' S = S
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- Given a basis `bW` of a submodule of an `R`-module `V`,
and a basis `bQ` of the quotient `V ⧸ W`,
this is a basis of `V` combining `bW` and a lift of `bQ`.  -/
Module.Basis.sumQuot : {R : Type u_2} →
  {V : Type u_3} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          {W : Submodule R V} →
            {m : Type u_4} → {n : Type u_5} → Module.Basis m R ↥W → Module.Basis n R (V ⧸ W) → Module.Basis (m ⊕ n) R V
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (Hₚ : ι → CategoryTheory.Functor TopPair C) →
            (H : ι → CategoryTheory.Functor TopCat C) →
              ((i : ι) → H i ≅ TopPair.incl.comp (Hₚ i)) →
                (δ : (i j : ι) → Hₚ i ⟶ TopPair.proj₂.comp (H j)) →
                  autoParam (∀ (i j : ι), ¬c.Rel i j → δ i j = 0) TopPair.HomologyPretheory.shape_δ._autoParam →
                    TopPair.HomologyPretheory C c
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findSomeRevM?.find.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m (Option β)) (as : Array α)
  (x_2 : 0 ≤ as.size), Array.findSomeRevM?.find✝ f as 0 x_2 = pure none
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.tag.inj : ∀ {α : Type u} {a : α} {a_1 : Lean.Widget.TaggedText α} {a_2 : α} {a_3 : Lean.Widget.TaggedText α},
  Lean.Widget.TaggedText.tag a a_1 = Lean.Widget.TaggedText.tag a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.ofHom_hom : ∀ {X Y : AddSemigrp} (f : X ⟶ Y), AddSemigrp.ofHom (AddSemigrp.Hom.hom f) = f
-- Init.Data.SInt.Lemmas
Int16.toInt32_toInt64 : ∀ (n : Int16), n.toInt64.toInt32 = n.toInt32
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- The optimal coupling constructed above realizes exactly the Gromov-Hausdorff distance,
essentially by design.  -/
GromovHausdorff.hausdorffDist_optimal : ∀ {X : Type u} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] {Y : Type v}
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
  Metric.hausdorffDist (Set.range (GromovHausdorff.optimalGHInjl X Y)) (Set.range (GromovHausdorff.optimalGHInjr X Y)) =
    GromovHausdorff.ghDist X Y
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.add : ∀ {α : Type u_1} {f : α → α} {x : α} {m n : ℕ},
  Function.IsPeriodicPt f n x → Function.IsPeriodicPt f m x → Function.IsPeriodicPt f (n + m) x
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.uniqueUpToIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C),
  (𝒞₁.uniqueUpToIso 𝒞₂).inv = 𝒞₂.hom 𝒞₁
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.mul'.eq_1 : ∀ (k : ℤ), Lean.Grind.Linarith.Poly.nil.mul' k = Lean.Grind.Linarith.Poly.nil
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.evalSuggestions : Lean.Elab.Tactic.Tactic
-- Mathlib.MeasureTheory.Group.AEStabilizer
MulAction.coe_aestabilizer : ∀ (G : Type u_1) {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.SMulInvariantMeasure G α μ] (s : Set α),
  ↑(MulAction.aestabilizer G μ s) = {g | g • s =ᵐ[μ] s}
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
ModularFormClass.levelOne_weight_zero_const : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range 0]
  (f : F), ∃ c, ⇑f = Function.const UpperHalfPlane c
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.toZeroHom : {M : Type u_10} → {N : Type u_11} → [inst : AddZero M] → [inst_1 : AddZero N] → (M →+ N) → ZeroHom M N
-- LeanSearchClient.Syntax
LeanSearchClient.checkTactic : Lean.Expr → Lean.Syntax → Lean.Elab.TermElabM (Option ℕ)
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newHyp.injEq : ∀ (fvarId : Lean.FVarId) (goal : Lean.Meta.Grind.Goal) (fvarId_1 : Lean.FVarId) (goal_1 : Lean.Meta.Grind.Goal),
  (Lean.Meta.Grind.IntroResult.newHyp✝ fvarId goal = Lean.Meta.Grind.IntroResult.newHyp✝ fvarId_1 goal_1) =
    (fvarId = fvarId_1 ∧ goal = goal_1)
-- Mathlib.FieldTheory.Normal.Defs
/-- Restrict algebra homomorphism to normal subfield (`AlgEquiv` version)  -/
AlgHom.restrictNormal' : {F : Type u_1} →
  [inst : Field F] →
    {K₁ : Type u_3} →
      {K₂ : Type u_4} →
        [inst_1 : Field K₁] →
          [inst_2 : Field K₂] →
            [inst_3 : Algebra F K₁] →
              [inst_4 : Algebra F K₂] →
                (K₁ →ₐ[F] K₂) →
                  (E : Type u_6) →
                    [inst_5 : Field E] →
                      [inst_6 : Algebra F E] →
                        [inst_7 : Algebra E K₁] →
                          [inst_8 : Algebra E K₂] →
                            [IsScalarTower F E K₁] → [IsScalarTower F E K₂] → [Normal F E] → Gal(E/F)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.mk.sizeOf_spec : ∀ (carrier : Type u) [str : Add carrier], sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Lean.Meta.Eqns
/-- Registers a new function for retrieving equation theorems.
We generate equations theorems on demand, and they are generated by more than one module.
For example, the structural and well-founded recursion modules generate them.
Most recent getters are tried first.

A getter returns an `Option (Array Name)`. The result is `none` if the getter failed.
Otherwise, it is a sequence of theorem names where each one of them corresponds to
an alternative. Example: the definition

```
def f (xs : List Nat) : List Nat :=
  match xs with
  | [] => []
  | x::xs => (x+1)::f xs
```
should have two equational theorems associated with it
```
f [] = []
```
and
```
(x : Nat) → (xs : List Nat) → f (x :: xs) = (x+1) :: f xs
```
 -/
Lean.Meta.registerGetEqnsFn : Lean.Meta.GetEqnsFn → IO Unit
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharRole.head.sizeOf_spec : sizeOf Lean.FuzzyMatching.CharRole.head = 1
-- Qq.Match
Qq.Impl.replaceTempExprsByQVars : List Qq.Impl.PatVarDecl → Lean.Expr → Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.involutiveNeg : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [InvolutiveNeg α] → InvolutiveNeg (Matrix m n α)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H1Iso_inv_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : groupHomology.H1 A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.π
      (CategoryTheory.CategoryStruct.comp (groupHomology.H1Iso A).inv h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.H1π A) h
-- Mathlib.Data.Finset.Defs
Finset.ssubset_def : ∀ {α : Type u_1} {s t : Finset α}, s ⊂ t ↔ s ⊆ t ∧ ¬t ⊆ s
-- Batteries.CodeAction.Attr
/-- Insert a tactic code action entry into the `TacticCodeActions` structure.  -/
Batteries.CodeAction.TacticCodeActions.insert : Batteries.CodeAction.TacticCodeActions →
  Array Lean.Name → Batteries.CodeAction.TacticCodeAction → Batteries.CodeAction.TacticCodeActions
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIsUniformAddGroup : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : UniformSpace G] [inst_2 : IsUniformAddGroup G],
  IsUniformAddGroup (SeparationQuotient G)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (toMulEquiv : α ≃* β) (map_le_map_iff' : ∀ {a b : α}, toMulEquiv.toFun a ≤ toMulEquiv.toFun b ↔ a ≤ b)
  (toMulEquiv_1 : α ≃* β) (map_le_map_iff'_1 : ∀ {a b : α}, toMulEquiv_1.toFun a ≤ toMulEquiv_1.toFun b ↔ a ≤ b),
  ({ toMulEquiv := toMulEquiv, map_le_map_iff' := map_le_map_iff' } =
      { toMulEquiv := toMulEquiv_1, map_le_map_iff' := map_le_map_iff'_1 }) =
    (toMulEquiv = toMulEquiv_1)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- The space of continuous affine maps from a topological vector space to a topological affine
space is in bijection with the product of the codomain with the space of linear maps, by taking the
value of the affine map at `(0 : V)` and the linear part.  -/
ContinuousAffineMap.decompEquiv : (R : Type u_1) →
  (V : Type u_3) →
    {W : Type u_4} →
      (Q : Type u_5) →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] →
            [inst_2 : Module R V] →
              [inst_3 : TopologicalSpace V] →
                [IsTopologicalAddGroup V] →
                  [inst_5 : AddCommGroup W] →
                    [inst_6 : Module R W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : AddTorsor W Q] →
                          [inst_9 : TopologicalSpace Q] → [IsTopologicalAddTorsor Q] → (V →ᴬ[R] Q) ≃ Q × (V →L[R] W)
-- Mathlib.FieldTheory.KrullTopology
instTotallySeparatedSpaceAlgEquivOfIsIntegral : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsIntegral K L],
  TotallySeparatedSpace Gal(L/K)
-- Std.Http.Data.Request
Std.Http.Request.mk.sizeOf_spec : ∀ {t : Type} [inst : SizeOf t] (line : Std.Http.Request.Head) (body : t) (extensions : Std.Http.Extensions),
  sizeOf { line := line, body := body, extensions := extensions } = 1 + sizeOf line + sizeOf body + sizeOf extensions
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_subtype_le : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} (K : AddSubgroup ↥H), AddSubgroup.map H.subtype K ≤ H
-- Mathlib.Analysis.Seminorm
Seminorm.ball_antitone : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {x : E} {r : ℝ}
  {p q : Seminorm 𝕜 E}, q ≤ p → p.ball x r ⊆ q.ball x r
-- Mathlib.Data.List.Sublists
List.sublistsLenAux.eq_2 : ∀ {α : Type u} {β : Type v} (x : List α → β) (x_1 : List β) (n : ℕ), List.sublistsLenAux n.succ [] x x_1 = x_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Raw.filter f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Raw.Const.get t x ⋯)).getD fallback
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.ResiduallyFinite.iInf_eq_bot : ∀ {G : Type u_1} {inst : AddGroup G} [self : AddGroup.ResiduallyFinite G], ⨅ H, H.toAddSubgroup = ⊥
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.sec_spec : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f : S.LocalizationMap N} (z : N), z * f ↑(f.sec z).2 = f (f.sec z).1
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.comp_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (h : L.Embedding N P), Function.Injective h.comp
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
CategoryTheory.Abelian.Ext.bilinearCompOfLinear_apply_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (R : Type t) [inst_3 : CommRing R] [inst_4 : CategoryTheory.Linear R C] (X Y Z : C)
  (a b c : ℕ) (h : a + b = c) (α : CategoryTheory.Abelian.Ext X Y a) (β : CategoryTheory.Abelian.Ext Y Z b),
  ((CategoryTheory.Abelian.Ext.bilinearCompOfLinear R X Y Z a b c h) α) β = α.comp β h
-- Lean.Data.KVMap
Lean.KVMap.mergeBy : (Lean.Name → Lean.DataValue → Lean.DataValue → Lean.DataValue) → Lean.KVMap → Lean.KVMap → Lean.KVMap
-- Mathlib.Tactic.Ring.Common
/-- Cast `ExSum btℕ sℕ` to `ExSumNat`.  -/
Mathlib.Tactic.Ring.Common.ExSum.toExSumNat : (e : Q(ℕ)) →
  Mathlib.Tactic.Ring.Common.ExSum Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ e →
    (e' : Q(ℕ)) × Mathlib.Tactic.Ring.Common.ExSumNat e'
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.StrongHomClass.homClass : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {F : Type u_3}
  [inst_2 : FunLike F M N] [L.StrongHomClass F M N], L.HomClass F M N
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- Construct a bialgebra equiv from an algebra equiv respecting counit and comultiplication.  -/
BialgEquiv.ofAlgEquiv : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Bialgebra R A] →
              [inst_4 : Bialgebra R B] →
                (f : A ≃ₐ[R] B) →
                  (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A →
                    (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) =
                        (Bialgebra.comulAlgHom R B).comp ↑f →
                      A ≃ₐc[R] B
-- Mathlib.Order.Atoms
Set.isAtom_singleton : ∀ {α : Type u_2} (x : α), IsAtom {x}
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.1}
  {c₂ : CategoryTheory.Limits.Cofan F.obj} (s t : c₁.pt ⟶ c₂.pt)
  (hs :
    ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s =
        CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 }))
  (ht :
    ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 })
  (i : CategoryTheory.Limits.Cofork s t) (x : J),
  (CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit s t hs ht i).ι.app x =
    CategoryTheory.CategoryStruct.comp (c₂.ι.app { as := x }) i.π
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.pushValue : Lean.Json.CompressWorkItemQueue✝ → Lean.Json → Lean.Json.CompressWorkItemQueue✝
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
/-- Inverse of the `tan` function, returns values in the range `-π / 2 < arctan x` and
`arctan x < π / 2`  -/
Real.arctan : ℝ → ℝ
-- Init.Data.BitVec.Bitblast
/-- The output of `divRec` has no more bits left to process (i.e., `wn = 0`)  -/
BitVec.wn_divRec : ∀ {w : ℕ} (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w), (BitVec.divRec qr.wn args qr).wn = 0
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ChangeAnnotationSupport : Type
-- Lean.Elab.Tactic.Classical
/-- `classical t` runs `t` in a scope where `Classical.propDecidable` is a low priority
local instance.
 -/
Lean.Elab.Tactic.classical : {m : Type → Type} →
  {α : Type} → [Monad m] → [Lean.MonadEnv m] → [MonadFinally m] → [MonadLiftT Lean.MetaM m] → m α → m α
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.sizeUpTo_ofLength_le : ∀ {n : ℕ} (c : Composition n) (i : ℕ), c.length ≤ i → c.sizeUpTo i = n
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- The atlas of charts in a `ChartedSpace`.  -/
atlas : (H : Type u_5) →
  [inst : TopologicalSpace H] →
    (M : Type u_6) → [inst_1 : TopologicalSpace M] → [ChartedSpace H M] → Set (OpenPartialHomeomorph M H)
-- Mathlib.CategoryTheory.Action.Basic
Action.functorCategoryEquivalence_counitIso : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G],
  (Action.functorCategoryEquivalence V G).counitIso = Action.FunctorCategoryEquivalence.counitIso
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_neg : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : Neg G] (f : α → G), ↑(-f) = -↑f
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.iff_of_isOpenCover : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover U →
    (Topology.IsLocallyConstructible s ↔ ∀ (i : ι), Topology.IsLocallyConstructible (Subtype.val ⁻¹' s))
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.all_eq_not_any_not : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {p : α → β → Bool},
  m.WF → m.all p = !m.any fun a b => !p a b
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.isSheaf_coherent_iff_regular_and_extensive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A)
  [inst_2 : CategoryTheory.Preregular C] [inst_3 : CategoryTheory.FinitaryPreExtensive C],
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) F ∧
      CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F
-- Init.Data.Vector.Find
Vector.find?_replicate_eq_none_iff : ∀ {α : Type} {n : ℕ} {a : α} {p : α → Bool}, Vector.find? p (Vector.replicate n a) = none ↔ n = 0 ∨ (!p a) = true
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Theory.completeTheory.subset : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {T : L.Theory} [MT : M ⊨ T], T ⊆ L.completeTheory M
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zigzag.of_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ j₃ : J} (f₂₁ : j₂ ⟶ j₁) (f₂₃ : j₂ ⟶ j₃),
  CategoryTheory.Zigzag j₁ j₃
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_differentiable_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E},
  Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f
-- Lean.Parser.Level
Lean.Parser.Level.hole.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instSetLike.eq_1 : ∀ {α : Type u_1} [inst : LE α], LowerSet.instSetLike = { coe := LowerSet.carrier, coe_injective := ⋯ }
-- Mathlib.Analysis.Real.Sqrt
/-- `NNReal.sqrt` as a `MonoidWithZeroHom`.  -/
NNReal.sqrtHom : NNReal →*₀ NNReal
-- Mathlib.Tactic.NormNum.Result
/-- The result is `proof : x`, where `x` is a (true) proposition.  -/
Mathlib.Meta.NormNum.Result.isTrue : {x : Q(Prop)} → Q(«$x») → Mathlib.Meta.NormNum.Result q(«$x»)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.map_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L M : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (ψ : L ⟶ M) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] [inst_6 : M.HasTotal c₁₂],
  HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.comp φ ψ) c₁₂ =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map φ c₁₂) (HomologicalComplex₂.total.map ψ c₁₂)
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.id_hComp_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnrichedOrdinary C}
  (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CatEnrichedOrdinary.hComp (CategoryTheory.CategoryStruct.id f) (CategoryTheory.CategoryStruct.id g) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_pow_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℕ}, f.SameCycle ((f ^ n) x) y ↔ f.SameCycle x y
-- Mathlib.Data.Nat.Nth
Nat.nth_zero_of_zero : ∀ {p : ℕ → Prop}, p 0 → Nat.nth p 0 = 0
-- Mathlib.Computability.DFA
DFA.evalFrom_singleton : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (a : α), M.evalFrom s [a] = M.step s a
-- Batteries.Data.List.Lemmas
List.getElem?_set_of_lt : ∀ {α : Type u_1} (a : α) {m n : ℕ} (l : List α), n < l.length → (l.set m a)[n]? = if m = n then some a else l[n]?
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f : X ⟶ Y} (self : HomotopicalAlgebra.CofibrantBrownFactorization f), HomotopicalAlgebra.Cofibration self.s