mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Gcd
/-- Computes the greatest common divisor of two natural numbers. The GCD of two natural numbers is the
largest natural number that evenly divides both.

In particular, the GCD of a number and `0` is the number itself.

This reference implementation via the Euclidean algorithm is overridden in both the kernel and the
compiler to efficiently evaluate using arbitrary-precision arithmetic. The definition provided here
is the logical model.

Examples:
* `Nat.gcd 10 15 = 5`
* `Nat.gcd 0 5 = 5`
* `Nat.gcd 7 0 = 7`
 -/
Nat.gcd : ℕ → ℕ → ℕ
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.Preadditive.commGrpEquivalence.functor.map f).hom.hom.hom = f
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subset_div_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α] {s t : Finset α}, 1 ∈ t → s ⊆ s / t
-- Init.Data.List.ToArray
List.toArray_eq_iff : ∀ {α : Type u_1} {as : List α} {bs : Array α}, as.toArray = bs ↔ as = bs.toList
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
/-- The inclusion of a face of `∂Δ[n]`.  -/
SSet.boundary.faceι : {n : ℕ} → (i : Fin (n + 1)) → (SSet.stdSimplex.face {i}ᶜ).toSSet ⟶ (SSet.boundary n).toSSet
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Δ'' : SimplexCategory}
  {e : Opposite.unop Δ' ⟶ Δ''} {i : Δ'' ⟶ Opposite.unop A.fst} [inst_3 : CategoryTheory.Epi e]
  [inst_4 : CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp e i = CategoryTheory.CategoryStruct.comp θ.unop A.e →
    CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A)
        ((AlgebraicTopology.DoldKan.Γ₀.obj K).map θ) =
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i)
        (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj
          (CategoryTheory.SimplicialObject.Splitting.IndexSet.mk e))
-- Std.Http.Data.Status
/-- Checks if the type of the status code is a client error, meaning that the request contains bad syntax
or cannot be fulfilled.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes
 -/
Std.Http.Status.isClientError : Std.Http.Status → Bool
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
add_neg_lt_neg_add_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c d : α} [AddRightStrictMono α],
  a + -b < -d + c ↔ d + a < c + b
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- **Alias** of the forward direction of `SimpleGraph.deleteFar_iff`. -/
SimpleGraph.DeleteFar.le_card_sub_card : ∀ {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : Fintype ↑G.edgeSet] {p : SimpleGraph V → Prop} {r : 𝕜} [inst_3 : Fintype (Sym2 V)],
  G.DeleteFar p r →
    ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.Quotient.inhabited.eq_1 : ∀ {M : Type u_1} [inst : Add M] [inst_1 : Zero M] {c : AddCon M}, AddCon.Quotient.inhabited = { default := ↑0 }
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.frontier_preimage : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) (s : Set B),
  e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.le_compProd_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) (s : Set (β × γ)),
  ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a ≤ ((κ.compProd η) a) s
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If `0 ≤ r < 1`, then `n ^ k r ^ n` tends to zero for any natural `k`.
This is a specialized version of `tendsto_pow_const_mul_const_pow_of_abs_lt_one`, singled out
for ease of application.  -/
tendsto_pow_const_mul_const_pow_of_lt_one : ∀ (k : ℕ) {r : ℝ}, 0 ≤ r → r < 1 → Filter.Tendsto (fun n => ↑n ^ k * r ^ n) Filter.atTop (nhds 0)
-- Mathlib.LinearAlgebra.Prod
LinearMap.fst_comp_inr : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], LinearMap.fst R M M₂ ∘ₗ LinearMap.inr R M M₂ = 0
-- Init.Data.List.Lemmas
List.contains_append : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α} {x : α}, (l₁ ++ l₂).contains x = (l₁.contains x || l₂.contains x)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.dim : {R : Type u_7} → {S : Type u_8} → [inst : CommRing R] → [inst_1 : Ring S] → [inst_2 : Algebra R S] → PowerBasis R S → ℕ
-- Lean.Elab.Do.PatternVar
_private.Lean.Elab.Do.PatternVar.0.Lean.Elab.Do.getLetIdVars : Lean.TSyntax `Lean.Parser.Term.letId → Lean.Elab.TermElabM (Array Lean.Ident)
-- Init.Data.UInt.Lemmas
USize.toUInt8_ofFin : ∀ (n : Fin USize.size), (USize.ofFin n).toUInt8 = UInt8.ofNat ↑n
-- Mathlib.CategoryTheory.Filtered.Basic
/-- A category `IsCofiltered` if
1. for every pair of objects there exists another object "to the left",
2. for every pair of parallel morphisms there exists a morphism to the left so the compositions
   are equal, and
3. there exists some object.  -/
CategoryTheory.IsCofiltered : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Topology.MetricSpace.Bounded
/-- Spheres are bounded  -/
Metric.isBounded_sphere : ∀ {α : Type u} {x : α} {r : ℝ} [inst : PseudoMetricSpace α], Bornology.IsBounded (Metric.sphere x r)
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instConcreteCategoryMonoidHomCarrier.eq_1 : GrpCat.instConcreteCategoryMonoidHomCarrier =
  { hom := fun {X Y} => GrpCat.Hom.hom', ofHom := fun {X Y} => GrpCat.Hom.mk✝,
    hom_ofHom := @GrpCat.instConcreteCategoryMonoidHomCarrier._proof_1,
    ofHom_hom := @GrpCat.instConcreteCategoryMonoidHomCarrier._proof_2,
    id_apply := @GrpCat.instConcreteCategoryMonoidHomCarrier._proof_3,
    comp_apply := @GrpCat.instConcreteCategoryMonoidHomCarrier._proof_4 }
-- Init.Data.Dyadic.Basic
Dyadic.instNeg : Neg Dyadic
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
lt_max_of_sq_lt_mul : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftMono M] [MulRightMono M] {a b c : M},
  a ^ 2 < b * c → a < max b c
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.topMap_comp : ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T),
  AlgebraicGeometry.Spec.topMap (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.topMap g) (AlgebraicGeometry.Spec.topMap f)
-- Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
CategoryTheory.MorphismProperty.ofObjectProperty_map_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.ObjectProperty C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D),
  (CategoryTheory.MorphismProperty.ofObjectProperty P Q).map F ≤
    CategoryTheory.MorphismProperty.ofObjectProperty (P.map F) (Q.map F)
-- Mathlib.Topology.UniformSpace.Cauchy
CompleteSpace.prod : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] [CompleteSpace α] [CompleteSpace β],
  CompleteSpace (α × β)
-- Mathlib.Algebra.Homology.Embedding.Connect
/-- Auxiliary definition for `ConnectData.cochainComplex`.  -/
CochainComplex.ConnectData.d : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : ChainComplex C ℕ} →
        {L : CochainComplex C ℕ} →
          CochainComplex.ConnectData K L →
            (n m : ℤ) → CochainComplex.ConnectData.X K L n ⟶ CochainComplex.ConnectData.X K L m
-- Mathlib.Order.ModularLattice
IsModularLattice.to_isLowerModularLattice : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α], IsLowerModularLattice α
-- Mathlib.Order.Irreducible
SupPrime.le_finset_sup : ∀ {ι : Type u_1} {α : Type u_2} [inst : SemilatticeSup α] {a : α} [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  SupPrime a → (a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i)
-- Mathlib.Topology.Hom.ContinuousEvalConst
Filter.Tendsto.coeFun : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] {ι : Type u_5} {l : Filter ι} {f : ι → F} {g : F},
  Filter.Tendsto f l (nhds g) → Filter.Tendsto (fun i => ⇑(f i)) l (nhds ⇑g)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_sdiff_le_prod_sdiff : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {f : ι → M}
  {s t : Finset ι} [inst_3 : DecidableEq ι], ∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ContinuousFunctionalCalculus.predicate_zero : ∀ (R : Type u_1) {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : StarRing R}
  {inst_2 : MetricSpace R} {inst_3 : IsTopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A}
  {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A}
  [self : ContinuousFunctionalCalculus R A p], p 0
-- Mathlib.Algebra.Algebra.Unitization
Unitization.snd_neg : ∀ {R : Type u_3} {A : Type u_4} [inst : Neg R] [inst_1 : Neg A] (x : Unitization R A), (-x).toProd.2 = -x.toProd.2
-- Mathlib.Algebra.Category.Grp.Basic
AddEquiv.toAddCommGrpIso_inv : ∀ {X Y : AddCommGrpCat} (e : ↑X ≃+ ↑Y), e.toAddCommGrpIso.inv = AddCommGrpCat.ofHom e.symm.toAddMonoidHom
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.instCommMonoid.eq_1 : ∀ {α : Type u_1} {f : α → α},
  IterateMulAct.instCommMonoid =
    { mul := fun m n => { val := m.val + n.val }, mul_assoc := ⋯, one := { val := 0 }, one_mul := ⋯, mul_one := ⋯,
      npow := fun n a => { val := n * a.val }, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }
-- Mathlib.Data.PEquiv
/-- Composition of partial equivalences `f : α ≃. β` and `g : β ≃. γ`.  -/
PEquiv.trans : {α : Type u} → {β : Type v} → {γ : Type w} → (α ≃. β) → (β ≃. γ) → α ≃. γ
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceMulOpposite.eq_1 : ∀ {α : Type ua} [inst : UniformSpace α], instUniformSpaceMulOpposite = UniformSpace.comap MulOpposite.unop inst
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_eq_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, a ∉ m → m.getKey! a = default
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.map.instIsMonHom : ∀ {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} [inst_4 : F.LaxMonoidal] (X Y : C) [inst_5 : CategoryTheory.MonObj X]
  [inst_6 : CategoryTheory.MonObj Y] (f : X ⟶ Y) [CategoryTheory.IsMonHom f], CategoryTheory.IsMonHom (F.map f)
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableNeg.measurable_neg : ∀ {G : Type u_2} {inst : Neg G} {inst_1 : MeasurableSpace G} [self : MeasurableNeg G], Measurable Neg.neg
-- Mathlib.Data.Seq.Computation
Computation.BisimO.eq_1 : ∀ {α : Type u} (R : Computation α → Computation α → Prop) (a a' : α),
  Computation.BisimO R (Sum.inl a) (Sum.inl a') = (a = a')
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- If `f, g` are analytic on a neighbourhood of the preconnected open set `U`, and `f • g = 0`
on `U`, then either `f = 0` on `U` or `g = 0` on `U`.  -/
AnalyticOnNhd.eq_zero_or_eq_zero_of_smul_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {A : Type u_3} [inst_1 : NormedRing A] [IsDomain A]
  [inst_3 : NormedAlgebra 𝕜 A] {B : Type u_4} [inst_4 : NormedAddCommGroup B] [inst_5 : NormedSpace 𝕜 B]
  [inst_6 : Module A B] [Module.IsTorsionFree A B] {f : 𝕜 → A} {g : 𝕜 → B},
  AnalyticOnNhd 𝕜 f U →
    AnalyticOnNhd 𝕜 g U → (∀ z ∈ U, f z • g z = 0) → IsPreconnected U → (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
-- Mathlib.Analysis.Normed.Group.Basic
nsmul_mem_ball : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ} {n : ℕ},
  0 < n → a ∈ Metric.ball b r → n • a ∈ Metric.ball (n • b) (n • r)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥X) (hx : f x ∈ U) {Z : CommRingCat}
  (h : X.presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U (f x) hx)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx) h)
-- Std.Data.TreeMap.Raw.Iterator
Std.TreeMap.Raw.keysIter_toList : ∀ {α β : Type u_1} {cmp : α → α → Ordering} (m : Std.TreeMap.Raw α β cmp), m.keysIter.toList = m.keys
-- Mathlib.Analysis.InnerProductSpace.Affine
/-- Squared distance between two points on lines from a common origin,
given orthogonality of the direction vectors.  -/
dist_sq_lineMap_lineMap_of_inner_eq_zero : ∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c : P} (t₁ t₂ : ℝ),
  inner ℝ (b -ᵥ a) (c -ᵥ a) = 0 →
    dist ((AffineMap.lineMap a b) t₁) ((AffineMap.lineMap a c) t₂) ^ 2 = t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.functor_norm_proc : Lean.ParserDescr
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.AddSemigrp.Hom.mk.inj : ∀ {A B : AddSemigrp} {hom' hom'_1 : ↑A →ₙ+ ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.eq_1 : ∀ (f : ℕ → ℂ) (s : ℂ), LSeries f s = ∑' (n : ℕ), LSeries.term f s n
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.coe_extendScalarsOfSurjective : ∀ {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A ≃ₐ[R] B), ⇑((AlgEquiv.extendScalarsOfSurjective h) f) = ⇑f
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- The Yoneda lemma for sheaves.  -/
CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : J.Subcanonical] →
        J.yoneda.op.comp CategoryTheory.coyoneda ≅
          (CategoryTheory.evaluation Cᵒᵖ (Type v)).comp
            (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type v)) (Type v)
                      (Type (max v u))).obj
                  CategoryTheory.uliftFunctor.{u, v}).comp
              ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Sheaf J (Type v))
                    (CategoryTheory.Functor Cᵒᵖ (Type v)) (Type (max v u))).obj
                (CategoryTheory.sheafToPresheaf J (Type v))))
-- Mathlib.NumberTheory.FermatPsp
Nat.probablePrime_iff_modEq : ∀ (n : ℕ) {b : ℕ}, 1 ≤ b → (n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n])
-- Lean.Elab.Binders
Lean.Elab.Term.expandForall : Lean.Macro
-- Mathlib.CategoryTheory.Category.Basic
/-- Close the main goal with `sorry` if its type contains `sorry`, and fail otherwise.  -/
CategoryTheory.sorryIfSorry : Lean.ParserDescr
-- Mathlib.Topology.Connected.Basic
isConnected_univ : ∀ {α : Type u} [inst : TopologicalSpace α] [ConnectedSpace α], IsConnected Set.univ
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- Since a hom gives a loop, any homomorphism from the vertex group at the root
extends to a functor on the whole groupoid.  -/
IsFreeGroupoid.SpanningTree.functorOfMonoidHom : {G : Type u} →
  [inst : CategoryTheory.Groupoid G] →
    [inst_1 : IsFreeGroupoid G] →
      (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) →
        [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] →
          {X : Type u_1} →
            [inst_3 : Monoid X] →
              (CategoryTheory.End (IsFreeGroupoid.SpanningTree.root'✝ T) →* X) →
                CategoryTheory.Functor G (CategoryTheory.SingleObj X)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Let `adj : F ⊣ G` be an adjunction, with `F : C ⥤ D` coreflective.
Assume that `C` has finite colimits and `G` commutes with them.
If `D` has exact limits of shape `J`, then `C` also has exact limits of shape `J`.  -/
CategoryTheory.Adjunction.hasExactLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''} [inst_1 : CategoryTheory.Category.{v'', u''} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Full] [F.Faithful] (J : Type u')
  [inst_4 : CategoryTheory.Category.{v', u'} J] [inst_5 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_6 : CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.HasExactLimitsOfShape J D]
  [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits G],
  CategoryTheory.HasExactLimitsOfShape J C
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.addFeature : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Aesop.Frontend.RuleConfig → Aesop.Frontend.Feature → m Aesop.Frontend.RuleConfig
-- Mathlib.Data.Finsupp.ToDFinsupp
DFinsupp.toFinsupp_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Monoid R] [inst_2 : AddMonoid M]
  [inst_3 : DistribMulAction R M] [inst_4 : (m : M) → Decidable (m ≠ 0)] (r : R) (f : Π₀ (x : ι), M),
  (r • f).toFinsupp = r • f.toFinsupp
-- Lean.Meta.Tactic.Repeat
/-- `repeat' f` runs `f` on all of the goals to produce a new list of goals,
then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
or until `maxIters` total calls to `f` have occurred.
Always succeeds (returning the original goals if `f` fails on all of them).
 -/
Lean.Meta.repeat' : {m : Type → Type} →
  {ε : Type u_1} →
    {s : Type} →
      [Monad m] →
        [MonadExcept ε m] →
          [Lean.MonadBacktrack s m] →
            [Lean.MonadMCtx m] →
              (Lean.MVarId → m (List Lean.MVarId)) → List Lean.MVarId → optParam ℕ 100000 → m (List Lean.MVarId)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- Up to an equivalence, the type `Ext.{w} X Y n` does not depend on the universe `w`.  -/
CategoryTheory.Abelian.Ext.chgUniv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        [inst_3 : CategoryTheory.HasExt C] →
          {X Y : C} → {n : ℕ} → CategoryTheory.Abelian.Ext X Y n ≃ CategoryTheory.Abelian.Ext X Y n
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDelabTermInfo.sizeOf_spec : ∀ (i : Lean.Elab.DelabTermInfo), sizeOf (Lean.Elab.Info.ofDelabTermInfo i) = 1 + sizeOf i
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι_map_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C]
  {G : CategoryTheory.Functor J C} (α : F ⟶ G) (j : J) {Z : C} (h : CategoryTheory.Limits.colim.obj G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map α) h) =
    CategoryTheory.CategoryStruct.comp (α.app j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G j) h)
-- Mathlib.Tactic.Linter.PPRoundtrip
/-- `capSourceInfo s p` "shortens" all end-position information in the `SourceInfo` `s` to be
at most `p`, trimming down also the relevant substrings.  -/
_private.Mathlib.Tactic.Linter.PPRoundtrip.0.Mathlib.Linter.capSourceInfo : Lean.SourceInfo → ℕ → Lean.SourceInfo
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits_right_inverse : ∀ {M : Type u_1} [inst : AddMonoid M], Function.RightInverse AddSubgroup.ofAddUnits AddSubmonoid.addUnits
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_starClosure : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : IsScalarTower R A A]
  [inst_7 : SMulCommClass R A A] (S : NonUnitalSubalgebra R A) {x : A}, x ∈ S.starClosure ↔ x ∈ S ⊔ star S
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieAlgebra.IsKilling.sl2SubmoduleOfRoot.congr_simp : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K]
  {α α_1 : LieModule.Weight K (↥H) L} (e_α : α = α_1) (hα : α.IsNonZero),
  LieAlgebra.IsKilling.sl2SubmoduleOfRoot hα = LieAlgebra.IsKilling.sl2SubmoduleOfRoot ⋯
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.multivariateGaussian_of_not_posSemidef : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (μ : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ},
  ¬S.PosSemidef → ProbabilityTheory.multivariateGaussian μ S = MeasureTheory.Measure.dirac μ
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.curry_apply_left : ∀ {X : Type u} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {H : Type u_3} [inst_2 : Group H]
  (F : CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.SingleObj H)) (g : G) (b : X),
  ((CategoryTheory.ActionCategory.curry F) g).left b = F.map (CategoryTheory.ActionCategory.homOfPair b g)
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.isNaNBits_packedNaN : ∀ {spec : Float.Model.Format}, Float.Model.UnpackedFloat.isNaNBits (Float.Model.UnpackedFloat.packedNaN spec) = true
-- Init.Data.Array.Basic
Array.findIdx?.eq_1 : ∀ {α : Type u} (p : α → Bool) (as : Array α), Array.findIdx? p as = Array.findIdx?.loop p as 0
-- Mathlib.Data.Multiset.ZeroCons
Multiset.rel_cons_right : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {as : Multiset α} {b : β} {bs : Multiset β},
  Multiset.Rel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Multiset.Rel r as' bs ∧ as = a ::ₘ as'
-- Lean.Attributes
Lean.AttributeExtension : Type
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.link2_eq_link2! : ∀ {α : Type u} {β : α → Type v} [Ord α] {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced) (hrb : r.Balanced),
  (l.link2 r hlb hrb).impl = l.link2! r
-- Mathlib.Topology.Compactness.Lindelof
/-- **Alias** of `HereditarilyLindelofSpace.isLindelof`. -/
HereditarilyLindelof_LindelofSets : ∀ {X : Type u} [inst : TopologicalSpace X] [HereditarilyLindelofSpace X] (s : Set X), IsLindelof s