mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.App
/-- User-provided arguments that still have to be processed.  -/
Lean.Elab.Term.ElabElim.State.args : Lean.Elab.Term.ElabElim.State → List Lean.Elab.Term.Arg
-- Init.Data.Array.DecidableEq
Array.instDecidableEqEmp_csimp : @Array.instDecidableEqEmp = @Array.instDecidableEqEmpImpl
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.neg_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ.[σ] F)
  (x : ↥(-f).domain), ↑(-f) x = -↑f x
-- Init.Data.List.TakeDrop
List.drop_of_length_le : ∀ {α : Type u_1} {i : ℕ} {l : List α}, l.length ≤ i → List.drop i l = []
-- Mathlib.CategoryTheory.Presentable.Type
CategoryTheory.Types.instIsPresentable : ∀ (X : Type u), CategoryTheory.IsPresentable.{u, u, u + 1} X
-- Lean.DocString.Markdown
Lean.Doc.instToMarkdownSnippet : Lean.Doc.ToMarkdown Lean.VersoModuleDocs.Snippet
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- A version of `dist_le_range_sum_dist` with each intermediate distance replaced
with an upper estimate.  -/
dist_le_range_sum_of_dist_le : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ},
  (∀ {k : ℕ}, k < n → dist (f k) (f (k + 1)) ≤ d k) → dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.prod_mono_left : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  (t : NonUnitalSubring S), Monotone fun s => s.prod t
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (φ : A ⟶ B) [CategoryTheory.IsIso φ], CategoryTheory.IsIso φ.hom₁
-- Mathlib.RingTheory.Extension.Generators
/-- See Note [custom simps projection]  -/
Algebra.Generators.Simps.σ : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Generators R S ι) → S → P.Ring
-- Mathlib.Computability.Encoding
/-- An equivalence between the "proxy type" `Computability.Γ'.proxyType` and `Computability.Γ'`. The proxy type is a reducible definition that represents the inductive type using `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum` (and whatever other inductive types appear within the inductive type), and the intended use is to define typeclass instances uses pre-existing instances on these. (Generated by the `proxy_equiv%` elaborator.) -/
Computability.Γ'.proxyTypeEquiv : Unit ⊕ Bool ⊕ Unit ⊕ Unit ⊕ Unit ≃ Computability.Γ'
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.id_dimension : ∀ {R : Type u} [inst : CommRing R], (Algebra.Presentation.id R).dimension = 0
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.Std.Do.PredTrans.pushExcept.match_1.eq_2 : ∀ {α ε : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_2 e