mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- A non-unital subring of a `NonUnitalCommRing` is a `NonUnitalCommRing`.  -/
NonUnitalSubringClass.toNonUnitalCommRing : {S : Type v} →
  (s : S) →
    {R : Type u_1} →
      [inst : NonUnitalCommRing R] → [inst_1 : SetLike S R] → [NonUnitalSubringClass S R] → NonUnitalCommRing ↥s
-- Mathlib.Data.List.Sigma
List.dlookup_kerase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) {l : List (Sigma β)},
  l.NodupKeys → List.dlookup a (List.kerase a l) = none
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_comp_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (a : E), fderiv 𝕜 (fun x => f (x - a)) x = fderiv 𝕜 f (x - a)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rio_eq_none : ∀ {n i : ℕ}, n ≤ i → (*...n).toArray[i]? = none
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.instToFormat : {α : Type} → [Std.ToFormat α] → Std.ToFormat (Lean.Meta.DiscrTree α)
-- Mathlib.Data.FinEnum
FinEnum.card_empty : FinEnum.card Empty = 0
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.subset : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A₁ A₂ : Set α} {B₁ B₂ : Set β}
  {f : α → β} {n : ℕ}, A₁ ⊆ A₂ → IsMulFreimanHom n A₂ B₂ f → Set.MapsTo f A₁ B₁ → IsMulFreimanHom n A₁ B₁ f
-- Mathlib.GroupTheory.Coset.Basic
QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)),
  QuotientAddGroup.preimageMkEquivAddSubgroupProdSet s t =
    { toFun := fun a => (⟨-Quotient.out ↑↑a + ↑a, ⋯⟩, ⟨↑↑a, ⋯⟩), invFun := fun a => ⟨Quotient.out ↑a.2 + ↑a.1, ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D)
  {X Y : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))} (f : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).map f).right = f.base
-- Mathlib.Tactic.Change
/-- `change? term` unifies `term` with the current goal, then suggests explicit `change` syntax
that uses the resulting unified term.

If `term` is not present, `change?` suggests the current goal itself. This is useful after tactics
which transform the goal while maintaining definitional equality, such as `dsimp`; those preceding
tactic calls can then be deleted.
```lean
example : (fun x : Nat => x) 0 = 1 := by
  change? 0 = _  -- `Try this: change 0 = 1`
```
 -/
change? : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.isoCoproduct.eq_1 : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f],
  CategoryTheory.Limits.biproduct.isoCoproduct f =
    (CategoryTheory.Limits.biproduct.isColimit f).coconePointUniqueUpToIso
      (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor f))
-- Init.Data.Vector.Lemmas
Vector.append_flatten : ∀ {α : Type u_1} {n m₁ m₂ : ℕ} {xss₁ : Vector (Vector α n) m₁} {xss₂ : Vector (Vector α n) m₂},
  xss₁.flatten ++ xss₂.flatten = Vector.cast ⋯ (xss₁ ++ xss₂).flatten
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- The **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  -/
MeasureTheory.lintegral : {α : Type u_4} → {m : MeasurableSpace α} → MeasureTheory.Measure α → (α → ENNReal) → ENNReal
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.mem_invtSubmodule_iff_forall_mem_of_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p : Submodule R M}, p ∈ f.invtSubmodule ↔ ∀ x ∈ p, f x ∈ p
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.compCreatesFiniteLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                [CategoryTheory.Limits.CreatesFiniteLimits F] →
                  [CategoryTheory.Limits.CreatesFiniteLimits G] → CategoryTheory.Limits.CreatesFiniteLimits (F.comp G)
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- Linear disjointness is symmetric in a commutative ring.  -/
Submodule.linearDisjoint_comm : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M N : Submodule R S}, M.LinearDisjoint N ↔ N.LinearDisjoint M
-- Mathlib.InformationTheory.Hamming
Hamming.toHamming_smul : ∀ {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → SMul α (β i)] {r : α} {x : (i : ι) → β i},
  Hamming.toHamming (r • x) = r • Hamming.toHamming x
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- For an extension `E / F` of exponential characteristic `q` and a separable element `a : E`, the
minimal polynomial of `a ^ q ^ n` equals the minimal polynomial of `a` mapped via `(⬝ ^ q ^ n)`.  -/
minpoly.iterateFrobenius_of_isSeparable : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q]
  [inst_3 : ExpChar E q] (n : ℕ) {a : E},
  IsSeparable F a → minpoly F ((iterateFrobenius E q n) a) = Polynomial.map (iterateFrobenius F q n) (minpoly F a)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv.injEq : ∀ (e : Lean.Expr) (f g : Mathlib.Tactic.BicategoryLike.Mor₁) (η : Mathlib.Tactic.BicategoryLike.Mor₂Iso)
  (e_1 : Lean.Expr) (f_1 g_1 : Mathlib.Tactic.BicategoryLike.Mor₁) (η_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  (Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv e f g η = Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv e_1 f_1 g_1 η_1) =
    (e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ η = η_1)
-- Init.Data.Nat.Basic
Nat.eq_of_mul_eq_mul_left : ∀ {m k n : ℕ}, 0 < n → n * m = n * k → m = k
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.not_mem_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α}, k ∉ ∅
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.dist.eq_1 : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] (x y : E),
  Euclidean.dist x y = dist (toEuclidean x) (toEuclidean y)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
/-- `p.IsSubwalk q` means that the walk `p` is a contiguous subwalk of the walk `q`.  -/
SimpleGraph.Walk.IsSubwalk : {V : Type u_1} → {G : SimpleGraph V} → {u₁ v₁ u₂ v₂ : V} → G.Walk u₁ v₁ → G.Walk u₂ v₂ → Prop
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.instRpcEncodableAwaitRefreshParams : Lean.Server.RpcEncodable ProofWidgets.RefreshComponent.AwaitRefreshParams
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.coe_sub : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] (a b : α), ↑(a - b) = ↑a - ↑b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- An `IsPullback` square over a cospan `(f, g)` is equivalent to an isomorphism
`Over.mk fst ≅ Over.mk (pullback.fst f g)` in `Over X`, together with the
second projection being determined by the isomorphism.  -/
CategoryTheory.IsPullback.iff_exists_over_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong g] {P : C} {p : P ⟶ X} {q : P ⟶ Y},
  CategoryTheory.IsPullback p q f g ↔
    ∃ e,
      q =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left e.hom) (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- If `c` is a limiting pullback cone, then we have an `IsPullback c.fst c.snd f g`.  -/
CategoryTheory.IsPullback.of_isLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {c : CategoryTheory.Limits.PullbackCone f g} (h : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.IsPullback c.fst c.snd f g