mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.mem_ideal_span_monomial_image_iff_dvd : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {x : MvPolynomial σ R} {s : Set (σ →₀ ℕ)},
  x ∈ Ideal.span ((fun s => (MvPolynomial.monomial s) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ s, (MvPolynomial.monomial si) 1 ∣ (MvPolynomial.monomial xi) (MvPolynomial.coeff xi x)
-- Mathlib.Algebra.Algebra.Subalgebra.Rank
Subalgebra.finrank_sup_eq_finrank_left_mul_finrank_of_free : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  [Module.Free R ↥A] [Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)],
  Module.finrank R ↥(A ⊔ B) = Module.finrank R ↥A * Module.finrank ↥A ↥(Algebra.adjoin ↥A ↑B)
-- Mathlib.Data.Set.Restrict
/-- Restrict domain of a function `f` to a set `s`. Same as `Subtype.restrict` but this version
takes an argument `↥s` instead of `Subtype s`.  -/
Set.domRestrict : {α : Type u_1} → {π : α → Type u_6} → (s : Set α) → ((a : α) → π a) → (a : ↑s) → π ↑a
-- Mathlib.Topology.UniformSpace.Defs
/-- For every set `u ∈ uniformity`, there exists `v ∈ uniformity` such that `v ○ v ⊆ u`.  -/
UniformSpace.comp : ∀ {α : Type u} [self : UniformSpace α],
  (UniformSpace.uniformity.lift' fun s => SetRel.comp s s) ≤ UniformSpace.uniformity
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `sub_neg`.

---

For `a - -b = a + b`, see `sub_neg_eq_add`.  -/
sub_lt_zero : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, a - b < 0 ↔ a < b
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquivOfAlgEquiv_eq : ∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M : Submonoid R} {S : Type u_6} [inst_3 : CommSemiring S] [inst_4 : Algebra A S] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower A R S] [inst_7 : IsLocalization M S] {P : Type u_7} [inst_8 : CommSemiring P]
  [inst_9 : Algebra A P] {T : Submonoid P} {Q : Type u_8} [inst_10 : CommSemiring Q] [inst_11 : Algebra A Q]
  [inst_12 : Algebra P Q] [inst_13 : IsScalarTower A P Q] [inst_14 : IsLocalization T Q] {h : R ≃ₐ[A] P}
  (H : Submonoid.map h M = T) (x : R),
  (IsLocalization.algEquivOfAlgEquiv S Q h H) ((algebraMap R S) x) = (algebraMap P Q) (h x)
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.instInhabited : Inhabited NonemptyFinLinOrd
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instIteratorLoop.match_1.eq_2 : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] {n : Type u_1 → Type u_3} (γ : Type u_1)
  (Pl : α → γ → ForInStep γ → Prop)
  (motive :
    (it : Std.IterM Id α) → ((b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) → Sort u_2)
  (f : (b : α) → { internalState := { next := none } }.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c)))
  (h_1 :
    (next : α) →
      (f :
          (b : α) →
            { internalState := { next := some next } }.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := some next } } f)
  (h_2 :
    (f : (b : α) → { internalState := { next := none } }.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) →
      motive { internalState := { next := none } } f),
  (match { internalState := { next := none } }, f with
    | { internalState := { next := some next } }, f => h_1 next f
    | { internalState := { next := none } }, f => h_2 f) =
    h_2 f
-- Mathlib.Topology.UnitInterval
unitInterval.symmHomeomorph_apply : ∀ (a : ↑unitInterval), unitInterval.symmHomeomorph a = unitInterval.symm a
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNonUnitalCommSemiring : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalCommSemiring β] →
          [IsTopologicalSemiring β] → NonUnitalCommSemiring (ZeroAtInftyContinuousMap α β)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
/-- Equality of `finrank`s when the base is a domain.  -/
RootPairing.finrank_corootSpan_eq' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [IsDomain R] [inst_5 : Module R M] [inst_6 : Module R N]
  (P : RootPairing ι R M N) [P.IsAnisotropic], Module.finrank R ↥(P.corootSpan R) = Module.finrank R ↥(P.rootSpan R)
-- Init.Data.Array.Lemmas
Array.replicate_inj : ∀ {n : ℕ} {α : Type u_1} {a : α} {m : ℕ} {b : α}, Array.replicate n a = Array.replicate m b ↔ n = m ∧ (n = 0 ∨ a = b)
-- Init.Data.BitVec.Lemmas
/-- If `x.toNat + y.toNat < 2^w`, then the addition `(x + y)` does not overflow.  -/
BitVec.toNat_add_of_lt : ∀ {w : ℕ} {x y : BitVec w}, x.toNat + y.toNat < 2 ^ w → (x + y).toNat = x.toNat + y.toNat
-- Mathlib.Algebra.Homology.HomologySequence
CategoryTheory.ShortComplex.ShortExact.δ_comp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j), CategoryTheory.CategoryStruct.comp (hS.δ i j hij) (HomologicalComplex.homologyMap S.f j) = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {fallback v : β}, Std.DTreeMap.Const.getD (t.insert k v) k fallback = v
-- Mathlib.Order.BooleanAlgebra.Basic
disjoint_sdiff_self_right : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], Disjoint x (y \ x)
-- Mathlib.Algebra.FreeMonoid.Count
FreeMonoid.countP_of : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (x : α),
  (FreeMonoid.countP p) (FreeMonoid.of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0
-- Mathlib.Analysis.Convex.Function
ConvexOn.convex_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ f x < r}
-- Mathlib.Data.Nat.Prime.Defs
Nat.le_minFac : ∀ {m n : ℕ}, n = 1 ∨ m ≤ n.minFac ↔ ∀ (p : ℕ), Nat.Prime p → p ∣ n → m ≤ p
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.mult_comap_le : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] (f : k →+* K) (w : NumberField.InfinitePlace K),
  (w.comap f).mult ≤ w.mult
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.notification.injEq : ∀ (method : String) (params? : Option Lean.Json.Structured) (method_1 : String)
  (params?_1 : Option Lean.Json.Structured),
  (Lean.JsonRpc.Message.notification method params? = Lean.JsonRpc.Message.notification method_1 params?_1) =
    (method = method_1 ∧ params? = params?_1)
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.map_comp_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K K' K'' : ChainComplex C ℕ} {L L' L'' : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L)
  (h' : CochainComplex.ConnectData K' L') (h'' : CochainComplex.ConnectData K'' L'') (fK : K ⟶ K') (fL : L ⟶ L')
  (f_comm : CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0))
  (fK' : K' ⟶ K'') (fL' : L' ⟶ L'')
  (f_comm' : CategoryTheory.CategoryStruct.comp (fK'.f 0) h''.d₀ = CategoryTheory.CategoryStruct.comp h'.d₀ (fL'.f 0)),
  CategoryTheory.CategoryStruct.comp (h.map h' fK fL f_comm) (h'.map h'' fK' fL' f_comm') =
    h.map h'' (CategoryTheory.CategoryStruct.comp fK fK') (CategoryTheory.CategoryStruct.comp fL fL') ⋯
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Class `ProperlyDiscontinuousVAdd Γ T` says that the additive action `(+ᵥ) : Γ → T → T`
is properly discontinuous, that is, for any pair of compact sets `K, L` in `T`, only finitely many
`γ : Γ` move `K` to have nontrivial intersection with `L`.
 -/
ProperlyDiscontinuousVAdd : (Γ : Type u_4) → (T : Type u_5) → [TopologicalSpace T] → [VAdd Γ T] → Prop
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_set_mem_vadd_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter β} {s : Set β} {a : α}, s ∈ f → a +ᵥ s ∈ a +ᵥ f
-- Mathlib.Order.WellFoundedSet
WellFounded.wellFoundedOn : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α}, WellFounded r → s.WellFoundedOn r
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreHomEquiv.mk.sizeOf_spec : ∀ {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} [inst_2 : SizeOf C] [inst_3 : SizeOf D]
  (homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
  (homEquiv_naturality_left_symm :
    autoParam
      (∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
        (homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (F.map f) ((homEquiv X Y).symm g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm._autoParam)
  (homEquiv_naturality_right :
    autoParam
      (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
        (homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp ((homEquiv X Y) f) (G.map g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right._autoParam),
  sizeOf
      { homEquiv := homEquiv, homEquiv_naturality_left_symm := homEquiv_naturality_left_symm,
        homEquiv_naturality_right := homEquiv_naturality_right } =
    1
-- Mathlib.Topology.Convenient.HomSpace
Topology.ContinuousMapGeneratedBy.mk.congr_simp : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] (toFun toFun_1 : Y → Z) (e_toFun : toFun = toFun_1)
  (prop : Topology.ContinuousGeneratedBy X toFun), { toFun := toFun, prop := prop } = { toFun := toFun_1, prop := ⋯ }
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.largeCategory : CategoryTheory.LargeCategory Bipointed
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- If `p` is an invariant submodule of an endomorphism `f`, then the `μ`-eigenspace of the
restriction of `f` to `p` is a submodule of the `μ`-eigenspace of `f`.  -/
Module.End.eigenspace_restrict_le_eigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p) (μ : R),
  Submodule.map p.subtype (Module.End.eigenspace (LinearMap.restrict f hfp) μ) ≤ f.eigenspace μ
-- Mathlib.Algebra.Free
FreeMagma.hom_ext : ∀ {α : Type u} {β : Type v} [inst : Mul β] {f g : FreeMagma α →ₙ* β}, ⇑f ∘ FreeMagma.of = ⇑g ∘ FreeMagma.of → f = g
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.op_whiskerRight_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor D E} (α : F ⟶ G) {Z : CategoryTheory.Functor Cᵒᵖ Eᵒᵖ} (h : (F.comp H).op ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.op (CategoryTheory.Functor.whiskerRight α H)) h =
    CategoryTheory.CategoryStruct.comp (G.opComp H).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op α) H.op)
        (CategoryTheory.CategoryStruct.comp (F.opComp H).inv h))
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.relabel_add : ∀ {α : Type u_1} {β : Type u_2} {f : Std.Sat.CNF α} {c : Std.Sat.CNF.Clause α} {r : α → β},
  Std.Sat.CNF.relabel r (Std.Sat.CNF.add c f) =
    Std.Sat.CNF.add (Std.Sat.CNF.Clause.relabel r c) (Std.Sat.CNF.relabel r f)
-- Lean.Data.PersistentArray
Lean.PersistentArray.Stats.mk.injEq : ∀ (numNodes depth tailSize numNodes_1 depth_1 tailSize_1 : ℕ),
  ({ numNodes := numNodes, depth := depth, tailSize := tailSize } =
      { numNodes := numNodes_1, depth := depth_1, tailSize := tailSize_1 }) =
    (numNodes = numNodes_1 ∧ depth = depth_1 ∧ tailSize = tailSize_1)
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.mulRight.congr_simp : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : Mul X] [inst_2 : SeparatelyContinuousMul X] (x x_1 : X),
  x = x_1 → ContinuousMap.mulRight x = ContinuousMap.mulRight x_1
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.faceOppositeCentroid_reindex : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex k P m)
  (e : Fin (m + 1) ≃ Fin (n + 1)), (s.reindex e).faceOppositeCentroid = s.faceOppositeCentroid ∘ ⇑e.symm
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.instIsIsoπTruncGEOfIsStrictlySupported : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [K.IsStrictlySupported e], CategoryTheory.IsIso (K.πTruncGE e)
-- Mathlib.Algebra.Quaternion
Quaternion.imK_nnratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ≥0), (↑q).imK = 0
-- Mathlib.Data.Int.GCD
Int.ne_zero_of_gcd : ∀ {x y : ℤ}, x.gcd y ≠ 0 → x ≠ 0 ∨ y ≠ 0
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.PostponeBehavior.no.sizeOf_spec : sizeOf Lean.Elab.Term.PostponeBehavior.no = 1
-- Mathlib.Analysis.Convex.Extreme
/-- A point `x` is an extreme point of a set `A`
iff `x ∈ A` and for any `x₁`, `x₂` such that `x` belongs to the open segment `(x₁, x₂)`,
we have `x₁ = x` and `x₂ = x`.

We used to use the RHS as the definition of `extremePoints`.
However, the conclusion `x₂ = x` is redundant,
so we changed the definition to the RHS of `mem_extremePoints_iff_left`.  -/
mem_extremePoints : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A : Set E} {x : E},
  x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.instFinalOppositeRightOpOfInitial : ∀ {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] (F : CategoryTheory.Functor Cᵒᵖ D) [F.Initial], F.rightOp.Final
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {a : α} [inst : Inhabited α], ∅.get! a = default
-- Mathlib.LinearAlgebra.TensorProduct.Basis
Module.Free.tensor : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S]
  [inst_2 : Algebra R S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M]
  [inst_6 : IsScalarTower R S M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [Module.Free S M] [Module.Free R N],
  Module.Free S (TensorProduct R M N)
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.mkUnder_ext_iff : ∀ {R : CommRingCat} {A : Type u} [inst : CommRing A] [inst_1 : Algebra (↑R) A] {B : CategoryTheory.Under R}
  {f g : R.mkUnder A ⟶ B},
  f = g ↔
    ∀ (a : A),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f)) a =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right g)) a
-- Mathlib.CategoryTheory.Monad.Equalizer
CategoryTheory.Comonad.beckCoalgebraFork_π_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra)
  (X_1 : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Comonad.beckCoalgebraFork X).π.app X_1 =
    CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t =>
      X_1 = t →
        (X ⟶
          (CategoryTheory.Limits.parallelPair (CategoryTheory.Comonad.CofreeEqualizer.topMap X)
                (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X)).obj
            X_1))
      (fun h => ⋯ ▸ CategoryTheory.Comonad.CofreeEqualizer.ι X)
      (fun h =>
        ⋯ ▸
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.CofreeEqualizer.ι X)
            (CategoryTheory.Comonad.CofreeEqualizer.topMap X))
      X_1 ⋯
-- Mathlib.Algebra.Group.Basic
eq_add_neg_of_add_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a + c = b → a = b + -c
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.augmentOfIsInitial_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {T : C}
  (hT : CategoryTheory.Limits.IsInitial T), (X.augmentOfIsInitial hT).left = T
-- Mathlib.Order.Irreducible
/-- **Alias** of the reverse direction of `supIrred_toDual`. -/
InfIrred.dual : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, InfIrred a → SupIrred (OrderDual.toDual a)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
/-- A space is simply connected if and only if it is path-connected and every loop
at any basepoint is null-homotopic (i.e., homotopic to the constant loop).  -/
simply_connected_iff_loops_nullhomotopic : ∀ {Y : Type u_2} [inst : TopologicalSpace Y],
  SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.instMonoid : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V1] → [inst_2 : Module k V1] → [inst_3 : AddTorsor V1 P1] → Monoid (P1 →ᵃ[k] P1)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.smul_leftMulMatrix : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {m : Type u_3}
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (b : Module.Basis m R S) {G : Type u_4} [inst_5 : Group G]
  [inst_6 : DistribMulAction G S] [inst_7 : SMulCommClass G R S] [SMulCommClass G S S] (g : G) (x : S),
  (Algebra.leftMulMatrix (g • b)) x = (Algebra.leftMulMatrix b) x
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.instLiftingInverseUniq : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst_1 : CategoryTheory.Category.{v_4, u_4} D₁] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D₂] →
            (L₁ : CategoryTheory.Functor C D₁) →
              (L₂ : CategoryTheory.Functor C D₂) →
                (W' : CategoryTheory.MorphismProperty C) →
                  [inst_3 : L₁.IsLocalization W'] →
                    [inst_4 : L₂.IsLocalization W'] →
                      CategoryTheory.Localization.Lifting L₂ W' L₁ (CategoryTheory.Localization.uniq L₁ L₂ W').inverse
-- Init.Data.Array.Lemmas
Array.forIn'_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {xs : Array α} {b : β}
  {f : (a : α) → a ∈ xs.toList → β → m (ForInStep β)}, forIn' xs.toList b f = forIn' xs b fun a m b => f a ⋯ b
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.glScalar_smul : ∀ (u : ℝˣ) (z : UpperHalfPlane), (Matrix.GeneralLinearGroup.scalar (Fin 2)) u • z = z
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.reflection_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι) (x : M),
  RootPairing.Equiv.reflection P i • x = (P.reflection i) x
-- Mathlib.Topology.Homotopy.Product
Path.Homotopic.prod_projLeft_projRight : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {a₁ a₂ : α} {b₁ b₂ : β}
  (p : Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂)),
  Path.Homotopic.prod (Path.Homotopic.projLeft p) (Path.Homotopic.projRight p) = p
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.mk.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction} (state : Std.Http.Protocol.H1.Reader.State dir) (input : ByteArray.Iterator)
  (messageHead : Std.Http.Protocol.H1.Message.Head dir) (messageCount bodyBytesRead headerBytesRead : ℕ)
  (noMoreInput : Bool),
  sizeOf
      { state := state, input := input, messageHead := messageHead, messageCount := messageCount,
        bodyBytesRead := bodyBytesRead, headerBytesRead := headerBytesRead, noMoreInput := noMoreInput } =
    1 + sizeOf state + sizeOf input + sizeOf messageHead + sizeOf messageCount + sizeOf bodyBytesRead +
        sizeOf headerBytesRead +
      sizeOf noMoreInput
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.associator_def : ∀ (R : Type u) [inst : CommRing R] (X Y Z : HopfAlgCat R),
  CategoryTheory.MonoidalCategoryStruct.associator X Y Z =
    (Bialgebra.TensorProduct.assoc R R X.carrier Y.carrier Z.carrier).toHopfAlgIso
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- Compressing an element is idempotent.  -/
UV.compress_idem : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  (u v a : α), UV.compress u v (UV.compress u v a) = UV.compress u v a
-- Mathlib.Data.Set.Function
Set.SurjOn.forall : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {p : β → Prop},
  Set.SurjOn f s t → Set.MapsTo f s t → ((∀ y ∈ t, p y) ↔ ∀ x ∈ s, p (f x))
-- Mathlib.Order.PFilter
Order.PFilter.instPartialOrder : {P : Type u_1} → [inst : Preorder P] → PartialOrder (Order.PFilter P)
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZifV1.mk : Std.Time.TimeZone.TZif.Header →
  Array ℤ →
    Array UInt8 →
      Array Std.Time.TimeZone.TZif.LocalTimeType →
        Array String → Array Std.Time.TimeZone.TZif.LeapSecond → Array Bool → Array Bool → Std.Time.TimeZone.TZif.TZifV1
-- Mathlib.Analysis.Complex.ReImTopology
Complex.isQuotientMap_re : Topology.IsQuotientMap Complex.re
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.δlastFunctor_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1))
  {X Y : Fin (n + 1)} (f : X ⟶ Y), (CategoryTheory.ComposableArrows.δlastFunctor.obj F).map f = F.map f
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- If a function converges along a filter to a limit `a`, is integrable along this filter, and
all elements of the filter have infinite measure, then the limit has to vanish.  -/
MeasureTheory.IntegrableAtFilter.eq_zero_of_tendsto : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {l : Filter α} {f : α → E},
  MeasureTheory.IntegrableAtFilter f l μ → (∀ s ∈ l, μ s = ⊤) → ∀ {a : E}, Filter.Tendsto f l (nhds a) → a = 0
-- Init.Data.List.Nat.Modify
List.getElem?_modify : ∀ {α : Type u_1} (f : α → α) (i : ℕ) (l : List α) (j : ℕ),
  (l.modify i f)[j]? = (fun a => if i = j then f a else a) <$> l[j]?
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.leadingCoeff_comp : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} [NoZeroDivisors R],
  q.natDegree ≠ 0 → (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofBdd_E : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) (indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n),
  (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground indep_bdd).E = E