mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MvPolynomial.Basic
/-- The `R`-submodule of multivariate polynomials whose coefficients lie in an `R`-submodule `M`.  -/
MvPolynomial.coeffsIn : {R : Type u_2} →
  {S : Type u_3} →
    (σ : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] → [inst_2 : Module R S] → Submodule R S → Submodule R (MvPolynomial σ S)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.exists_code.comp : ∀ {m n : ℕ} {f : List.Vector ℕ n →. ℕ} {g : Fin n → List.Vector ℕ m →. ℕ},
  (∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v) →
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> ((List.Vector.mOfFn fun i => g i v) >>= f)
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.mk.injEq : ∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} (toRingHom : A →+* B) (ideal_comp : Ideal.map toRingHom I ≤ J)
  (dpow_comp : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom a) = toRingHom (hI.dpow n a)) (toRingHom_1 : A →+* B)
  (ideal_comp_1 : Ideal.map toRingHom_1 I ≤ J)
  (dpow_comp_1 : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom_1 a) = toRingHom_1 (hI.dpow n a)),
  ({ toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := dpow_comp } =
      { toRingHom := toRingHom_1, ideal_comp := ideal_comp_1, dpow_comp := dpow_comp_1 }) =
    (toRingHom = toRingHom_1)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_add : ∀ {R : Type u} {M : Type v} [inst : Add R] [inst_1 : Add M] (x₁ x₂ : TrivSqZeroExt R M), (x₁ + x₂).snd = x₁.snd + x₂.snd
-- Mathlib.Algebra.Group.Hom.Defs
/-- Any type satisfying `MulHomClass` can be cast into `MulHom` via `MulHomClass.toMulHom`.  -/
instCoeTCMulHomOfMulHomClass : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} →
      [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : FunLike F M N] → [MulHomClass F M N] → CoeTC F (M →ₙ* N)
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.exists_comp_isoModSerre_eq_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y),
  (∃ Y' s, ∃ (_ : P.isoModSerre s), CategoryTheory.CategoryStruct.comp f s = 0) ↔ P (CategoryTheory.Abelian.image f)
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.mk.sizeOf_spec : ∀ (description : Unit → Lean.MessageData) (m : Lean.Elab.Do.DoElabM Lean.Expr)
  (stM runInBase : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr)
  (restoreCont : Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont),
  sizeOf { description := description, m := m, stM := stM, runInBase := runInBase, restoreCont := restoreCont } =
    1 + sizeOf description
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDifferentiableWithinAt_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {s : Set E}
  {x : E}, LineDifferentiableWithinAt 𝕜 f s x 0
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.RingMode.noConfusionType : Sort v✝ → Mathlib.Tactic.RingNF.RingMode → Mathlib.Tactic.RingNF.RingMode → Sort v✝
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_of_contains_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {f : (a : α) → β a → Bool} {k : α}, (Std.DTreeMap.filter f t).contains k = true → t.contains k = true
-- Mathlib.Data.List.Sort
_private.Mathlib.Data.List.Sort.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- This structure contains the data of three left fractions for
`W : MorphismProperty C` that have the same "denominator".  -/
CategoryTheory.MorphismProperty.LeftFraction₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.MorphismProperty C → C → C → Type (max u_1 v_1)
-- Mathlib.Algebra.Lie.Prod
LieHom.prodMap_apply : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L₃ : Type u_5} {L₄ : Type u_6} [inst : CommRing R]
  [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂]
  [inst_5 : LieRing L₃] [inst_6 : LieAlgebra R L₃] [inst_7 : LieRing L₄] [inst_8 : LieAlgebra R L₄] (f : L₁ →ₗ⁅R⁆ L₃)
  (g : L₂ →ₗ⁅R⁆ L₄) (x : L₁ × L₂), (f.prodMap g) x = (f x.1, g x.2)
-- Mathlib.Order.CompleteLattice.Basic
iSup_extend_bot : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] {e : ι → β},
  Function.Injective e → ∀ (f : ι → α), ⨆ j, Function.extend e f ⊥ j = ⨆ i, f i
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintTooltip.plaintext.sizeOf_spec : ∀ (text : String), sizeOf (Lean.Lsp.InlayHintTooltip.plaintext text) = 1 + sizeOf text
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Zero is a left absorbing element for multiplication  -/
MulZeroOneClass.zero_mul : ∀ {M₀ : Type u} [self : MulZeroOneClass M₀] (a : M₀), 0 * a = 0