mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.NonZeroDivisors
IsAddLeftRegular.nsmul_injective : ∀ {R : Type u_1} [inst : AddMonoid R] {r : R} [IsAddTorsionFree R],
  IsAddLeftRegular r → r ≠ 0 → Function.Injective fun n => n • r
-- Aesop.Search.Expansion
Aesop.RuleResult : Type
-- Std.Time.Format.Modifier
Std.Time.instInhabitedOffsetZ : Inhabited Std.Time.OffsetZ
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofArrowIso_toTransfiniteCompositionOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {X Y : C} {f : X ⟶ Y}
  (h : W.TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'),
  (h.ofArrowIso e).toTransfiniteCompositionOfShape = h.ofArrowIso e
-- Mathlib.Analysis.Meromorphic.Order
/-- Eta-expanded form of `meromorphicOrderAt_pow_id_sub_const`

---

The order of `(· - x) ^ n` at `x` is `n`.  -/
fun_meromorphicOrderAt_pow_id_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℕ}, meromorphicOrderAt (fun i => (i - x) ^ n) x = ↑n
-- Init.Grind.Ring.Basic
/-- Right distributivity of multiplication over addition.  -/
Lean.Grind.Semiring.right_distrib : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a b c : α), (a + b) * c = a * c + b * c
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.linearMap_apply : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (ij : ι₂ × ι₁), (b₁.linearMap b₂) ij = (Matrix.toLin b₁ b₂) ((Matrix.stdBasis R ι₂ ι₁) ij)
-- Mathlib.Analysis.Normed.Group.Defs
/-- The distance function is induced by the norm.  -/
SeminormedAddGroup.dist_eq : ∀ {E : Type u_8} [self : SeminormedAddGroup E] (x y : E), dist x y = ‖-x + y‖
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.hasCompactSupport : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E] [T2Space M], HasCompactSupport ↑f
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiable_of_differentiableOn_iUnion_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {ι : Type u_4} {s : ι → Set E},
  (∀ (i : ι), DifferentiableOn 𝕜 f (s i)) → (∀ (i : ι), IsOpen (s i)) → ⋃ i, s i = Set.univ → Differentiable 𝕜 f
-- Mathlib.CategoryTheory.Endomorphism
/-- `f.map` as a monoid hom between endomorphism monoids.  -/
CategoryTheory.Functor.mapEnd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      {D : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} D] →
          (f : CategoryTheory.Functor C D) → CategoryTheory.End X →* CategoryTheory.End (f.obj X)
-- Lean.Data.Lsp.Diagnostics
/-- The range at which the message applies.  -/
Lean.Lsp.DiagnosticWith.range : {α : Type} → Lean.Lsp.DiagnosticWith α → Lean.Lsp.Range
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_eq_one : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {f : Π₀ (i : ι), β i}
  {h : (i : ι) → β i → γ}, (∀ (i : ι), h i (f i) = 1) → f.prod h = 1
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatMarkerLong : Std.Time.DateFormatSymbols → Std.Time.HourMarker → String
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_insert : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α],
  a ∉ s → ∀ (f : α → ℕ), Nat.multinomial (insert a s) f = (f a + ∑ i ∈ s, f i).choose (f a) * Nat.multinomial s f
-- Mathlib.Order.Sublattice
/-- The range of `LatticeHom` is a sublattice.
 -/
Sublattice.LatticeHom.range : {α : Type u_2} → {β : Type u_3} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom α β → Sublattice β
-- Mathlib.Algebra.Ring.Defs
Ring.neg_add_cancel : ∀ {R : Type u} [self : Ring R] (a : R), -a + a = 0
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiff_of_subsingleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {n : WithTop ℕ∞} [Subsingleton M'], ContMDiff I I' n f
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.leadingCoeff_nonpos_iff : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : Zero R] [inst_2 : LinearOrder R]
  {x : Lex (HahnSeries Γ R)}, (ofLex x).leadingCoeff ≤ 0 ↔ x ≤ 0
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.mk.inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {inst : Monoid R} {inst_1 : NonUnitalNonAssocSemiring A}
  {inst_2 : DistribMulAction R A} {inst_3 : Star A} {inst_4 : NonUnitalNonAssocSemiring B}
  {inst_5 : DistribMulAction R B} {inst_6 : Star B} {toNonUnitalAlgHom : A →ₙₐ[R] B}
  {map_star' : ∀ (a : A), toNonUnitalAlgHom.toFun (star a) = star (toNonUnitalAlgHom.toFun a)}
  {toNonUnitalAlgHom_1 : A →ₙₐ[R] B}
  {map_star'_1 : ∀ (a : A), toNonUnitalAlgHom_1.toFun (star a) = star (toNonUnitalAlgHom_1.toFun a)},
  { toNonUnitalAlgHom := toNonUnitalAlgHom, map_star' := map_star' } =
      { toNonUnitalAlgHom := toNonUnitalAlgHom_1, map_star' := map_star'_1 } →
    toNonUnitalAlgHom = toNonUnitalAlgHom_1
-- Lean.Parser.Basic
Lean.Parser.nameLitNoAntiquot : Lean.Parser.Parser
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.ext_iff : ∀ {R : Type u_1} [inst : NonUnitalRing R] {p q : RingSeminorm R}, p = q ↔ ∀ (x : R), p x = q x
-- Mathlib.Order.CompleteBooleanAlgebra
biInf_inter_of_pairwise_codisjoint : ∀ {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} {f : ι → α},
  Pairwise (Function.onFun Codisjoint f) → ∀ (s t : Set ι), ⨅ i ∈ s ∩ t, f i = (⨅ i ∈ s, f i) ⊔ ⨅ i ∈ t, f i
-- Init.Data.List.SplitOn.Lemmas
List.splitOnPPrepend.induct_unfolding : ∀ {α : Type u_1} (p : α → Bool) (motive : List α → List α → List (List α) → Prop),
  (∀ (acc : List α), motive [] acc [acc.reverse]) →
    (∀ (a : α) (t acc : List α),
        p a = true →
          motive t [] (List.splitOnPPrepend p t []) →
            motive (a :: t) acc (acc.reverse :: List.splitOnPPrepend p t [])) →
      (∀ (a : α) (t acc : List α),
          ¬p a = true →
            motive t (a :: acc) (List.splitOnPPrepend p t (a :: acc)) →
              motive (a :: t) acc (List.splitOnPPrepend p t (a :: acc))) →
        ∀ (l acc : List α), motive l acc (List.splitOnPPrepend p l acc)
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The composition of the isomorphism `pullbackSpecIso R S T` (from the pullback of
`Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the morphism
`Spec (S ⊗[R] T) ⟶ Spec S` obtained by applying `Spec.map` to the ring morphism `s ↦ s ⊗ₜ[R] 1`
is the first projection.
 -/
AlgebraicGeometry.pullbackSpecIso_hom_fst_assoc : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of S) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))
      h
-- Mathlib.Data.Nat.Bits
Nat.boddDiv2.eq_def : ∀ (x : ℕ),
  x.boddDiv2 =
    match x with
    | 0 => (false, 0)
    | n.succ =>
      match n.boddDiv2 with
      | (false, m) => (true, m)
      | (true, m) => (false, m.succ)
-- Lean.Meta.Tactic.Intro
/-- Introduce one object from the goal `mvarid`, preserving the name used in the binder.
Returns a pair made of the newly introduced variable and the new goal.
This will fail if there is nothing to introduce, ie when the goal
does not start with a forall, lambda or let.  -/
Lean.MVarId.intro1P : Lean.MVarId → Lean.MetaM (Lean.FVarId × Lean.MVarId)