mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.Lp.coeFn_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : PartialOrder E] (f g : ↥(MeasureTheory.Lp E p μ)), ↑↑f ≤ᵐ[μ] ↑↑g ↔ f ≤ g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, k ∈ Std.TreeMap.map f t → k ∈ t
-- Lean.Parser.Extension
Lean.Parser.AliasValue.const.inj : ∀ {α : Type} {p p_1 : α}, Lean.Parser.AliasValue.const p = Lean.Parser.AliasValue.const p_1 → p = p_1
-- Init.Data.String.Substring
/-- Removes leading and trailing whitespace from a substring by first moving its start position to the
first non-whitespace character, and then moving its end position to the last non-whitespace
character.

If the substring consists only of whitespace, then the resulting substring's start position is moved
to its end position.

“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.

Examples:
 * `" red green blue ".toRawSubstring.trim.toString = "red green blue"`
 * `" red green blue ".toRawSubstring.trim.startPos = ⟨1⟩`
 * `" red green blue ".toRawSubstring.trim.stopPos = ⟨15⟩`
 * `"     ".toRawSubstring.trim.startPos = ⟨5⟩`
 -/
Substring.Raw.trim : Substring.Raw → Substring.Raw
-- Mathlib.Algebra.Group.Torsion
IsMulTorsionFree.zpow_eq_one_iff_right : ∀ {G : Type u_2} [inst : Group G] [IsMulTorsionFree G] {n : ℤ} {a : G}, a ≠ 1 → (a ^ n = 1 ↔ n = 0)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.ext.inj : ∀ {ext₁? : Option Lean.Meta.SimpExtension} {ext₂? : Option Lean.Meta.Simp.SimprocExtension}
  {h : (ext₁?.isSome || ext₂?.isSome) = true} {ext₁?_1 : Option Lean.Meta.SimpExtension}
  {ext₂?_1 : Option Lean.Meta.Simp.SimprocExtension} {h_1 : (ext₁?_1.isSome || ext₂?_1.isSome) = true},
  Lean.Elab.Tactic.ElabSimpArgResult.ext ext₁? ext₂? h = Lean.Elab.Tactic.ElabSimpArgResult.ext ext₁?_1 ext₂?_1 h_1 →
    ext₁? = ext₁?_1 ∧ ext₂? = ext₂?_1
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.HasProjectiveResolutions.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} [self : CategoryTheory.HasProjectiveResolutions C] (Z : C),
  CategoryTheory.HasProjectiveResolution Z
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop} (j : J),
  CommRingCat.Colimits.Relation.below ⋯
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_or_distrib_right : ∀ (x y z : ℕ), (x ||| y) &&& z = x &&& z ||| y &&& z
-- Lean.Parser.Types
Lean.Parser.Error : Type
-- Init.Data.BitVec.Lemmas
BitVec.sub_sub_toNat_cancel : ∀ {w : ℕ} {x : BitVec w}, 2 ^ w - (2 ^ w - x.toNat) = x.toNat
-- Batteries.Data.List.Basic
List.Forall₂.below.cons : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}
  {motive : (a : List α) → (a_1 : List β) → List.Forall₂ R a a_1 → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β}
  (a_1 : R a b) (a_2 : List.Forall₂ R l₁ l₂), List.Forall₂.below a_2 → motive l₁ l₂ a_2 → List.Forall₂.below ⋯
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_norm_def : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α), ‖A‖ = (∑ i, ∑ j, ‖A i j‖ ^ 2) ^ (1 / 2)
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_mul : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : Mul β]
  [IsMulApply F α β] (f g : F), ⇑(f * g) = ⇑f * ⇑g
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_mk : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f : M →ₗ[R] N)
  (h : ∀ {x : L} {m : M}, f.toFun ⁅x, m⁆ = ⁅x, f.toFun m⁆), ⇑{ toLinearMap := f, map_lie' := h } = ⇑f
-- Mathlib.Topology.ContinuousMap.CocompactMap
Homeomorph.toCocompactMap_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β) (a : α),
  f.toCocompactMap a = f a
-- Mathlib.Order.UpperLower.Closure
LowerSet.sdiff_lt_left : ∀ {α : Type u_1} [inst : Preorder α] {s : LowerSet α} {t : Set α}, s.sdiff t < s ↔ ¬Disjoint (↑s) t
-- Mathlib.Order.OrderIsoNat
RelEmbedding.natLT.congr_simp : ∀ {α : Type u_1} {r : α → α → Prop} [inst : IsStrictOrder α r] (f f_1 : ℕ → α) (e_f : f = f_1)
  (H : ∀ (n : ℕ), r (f n) (f (n + 1))), RelEmbedding.natLT f H = RelEmbedding.natLT f_1 ⋯
-- Mathlib.Topology.Convenient.GeneratedBy
instTopologicalSpaceSigma.eq_1 : ∀ {ι : Type u_5} {X : ι → Type v} [t₂ : (i : ι) → TopologicalSpace (X i)],
  instTopologicalSpaceSigma = ⨆ i, TopologicalSpace.coinduced (Sigma.mk i) (t₂ i)
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (φ ψ : MvPolynomial σ R),
  (φ * ψ).vars ⊆ φ.vars ∪ ψ.vars
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.mk.injEq : ∀ {α : Type u_4} (Has : Set α → Prop) (has_empty : Has ∅) (has_compl : ∀ {a : Set α}, Has a → Has aᶜ)
  (has_iUnion_nat : ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has (f i)) → Has (⋃ i, f i))
  (Has_1 : Set α → Prop) (has_empty_1 : Has_1 ∅) (has_compl_1 : ∀ {a : Set α}, Has_1 a → Has_1 aᶜ)
  (has_iUnion_nat_1 :
    ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has_1 (f i)) → Has_1 (⋃ i, f i)),
  ({ Has := Has, has_empty := has_empty, has_compl := has_compl, has_iUnion_nat := has_iUnion_nat } =
      { Has := Has_1, has_empty := has_empty_1, has_compl := has_compl_1, has_iUnion_nat := has_iUnion_nat_1 }) =
    (Has = Has_1)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_neg : ∀ {R : Type u} [inst : Ring R] {f : Polynomial R} {k : ℕ},
  (⇑Polynomial.derivative)^[k] (-f) = -(⇑Polynomial.derivative)^[k] f
-- Mathlib.Topology.Sets.Closeds
/-- The type of clopen sets of a topological space.  -/
TopologicalSpace.Clopens : (α : Type u_4) → [TopologicalSpace α] → Type u_4
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    ∀ {fallback : β k},
      Std.Internal.List.getValueCastD k (List.filter (fun p => f p.fst p.snd) l) fallback =
        (Option.filter (f k) (Std.Internal.List.getValueCast? k l)).getD fallback
-- Mathlib.Algebra.Star.Basic
starRingEquiv_apply : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R] (x : R),
  starRingEquiv x = MulOpposite.op (star x)
-- Init.Data.Range.Polymorphic.PRange
/-- The upper bound of the range. `upper` is included in the range.
   -/
Std.Roc.upper : {α : Type u} → Std.Roc α → α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {a : α} {fallback : β a},
  ∅.getD a fallback = fallback
-- Mathlib.Order.Basic
forall_le_iff_le : ∀ {α : Type u_2} [inst : Preorder α] {a b : α}, (∀ ⦃c : α⦄, c ≤ a → c ≤ b) ↔ a ≤ b
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_nsmul_add : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommMonoid G]
  [inst_2 : AddMonoid H] [AddConstMapClass F G H a b] (f : F) (n : ℕ) (x : G), f (n • a + x) = f x + n • b
-- Mathlib.Topology.Algebra.Group.Matrix
Topology.IsInducing.specialLinearGroup_map : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] {f : R →+* S},
  Topology.IsInducing ⇑f → Topology.IsInducing ⇑(Matrix.SpecialLinearGroup.map f)
-- Mathlib.Tactic.NormNum.Result
/-- A "raw int cast" is an expression of the form:

* `(Nat.rawCast lit : α)` where `lit` is a raw natural number literal
* `(Int.rawCast (Int.negOfNat lit) : α)` where `lit` is a nonzero raw natural number literal

(That is, we only actually use this function for negative integers.) This representation is used by
tactics like `ring` to decrease the number of typeclass arguments required in each use of a number
literal at type `α`.
 -/
Int.rawCast : {α : Type u} → [Ring α] → ℤ → α
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.activateTheorems : Lean.Name → ℕ → Lean.Meta.Grind.GoalM Unit
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.instInhabitedContext : Inhabited Lean.Meta.Grind.EMatch.Context
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.addCommMonoid : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (p : Submodule R M) → AddCommMonoid (M ⧸ p)
-- Lean.Server.InfoUtils
Lean.Elab.InfoTree.collectTermInfoM : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    [Monad m] → Lean.Elab.InfoTree → (Lean.Elab.ContextInfo → Lean.Elab.TermInfo → m (Option α)) → m (List α)
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
/-- The inclusion from an additive commutative monoid `M` to its Grothendieck group.

Note that this is only injective if `M` is cancellative.  -/
Algebra.GrothendieckAddGroup.of : {M : Type u_1} → [inst : AddCommMonoid M] → M →+ Algebra.GrothendieckAddGroup M
-- Mathlib.Algebra.Group.AddChar
AddChar.toMonoidHomEquiv_symm_apply : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : Multiplicative A →* M) (a : A),
  (AddChar.toMonoidHomEquiv.symm ψ) a = ψ (Multiplicative.ofAdd a)
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (i : J) (hi : i ≤ Order.succ j),
  CategoryTheory.SmallObject.SuccStruct.extendToSucc.map hj F τ i i ⋯ hi =
    CategoryTheory.CategoryStruct.id (CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj F X ⟨i, ⋯⟩)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {app : (a : B) → η.app a ⟶ θ.app a}
  {naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Oplax.StrongTrans.Modification.naturality._autoParam}
  {app_1 : (a : B) → η.app a ⟶ θ.app a}
  {naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b))
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f)))
      CategoryTheory.Oplax.StrongTrans.Modification.naturality._autoParam},
  { app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 } → app = app_1
-- Init.Core
Subtype.ext : ∀ {α : Sort u} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
-- Mathlib.Order.Category.HeytAlg
HeytAlg.coe_comp : ∀ {X Y Z : HeytAlg} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Lean.Parser.Do
/-- `assert! cond` panics if `cond` evaluates to `false`.
 -/
Lean.Parser.Term.doAssert : Lean.Parser.Parser
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvalues_eq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian) (i : n),
  hA.eigenvalues i = RCLike.re (star (hA.eigenvectorBasis i).ofLp ⬝ᵥ A.mulVec (hA.eigenvectorBasis i).ofLp)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_image : ∀ {f : ZFSet.{u} → ZFSet.{u}} [inst : ZFSet.Definable₁ f] {x y : ZFSet.{u}}, y ∈ ZFSet.image f x ↔ ∃ z ∈ x, f z = y
-- Init.Data.UInt.Bitwise
UInt32.or_eq_zero_iff : ∀ {a b : UInt32}, a ||| b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.op_eq_self_of_isPrincipal`. -/
Ordinal.op_eq_self_of_principal : ∀ {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  a < o → Order.IsNormal (op a) → Ordinal.IsPrincipal op o → Order.IsSuccLimit o → op a o = o
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Multiset.sup_powerset_len : ∀ {α : Type u_2} [inst : DecidableEq α] (x : Multiset α),
  ((Finset.range (x.card + 1)).sup fun k => Multiset.powersetCard k x) = x.powerset
-- Std.Data.HashMap.Lemmas
Std.HashMap.all_toList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {p : α → β → Bool},
  (m.toList.all fun x => p x.1 x.2) = m.all p
-- Mathlib.Logic.Equiv.Multiset
Denumerable.isChain_cons_raise : ∀ (l : List ℕ) (n : ℕ), List.IsChain (fun x1 x2 => x1 ≤ x2) (n :: Denumerable.raise l n)
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.isIntegralHom_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsIntegralHom f ↔
    AlgebraicGeometry.IsAffineHom f ∧
      ∀ (U : Y.Opens),
        AlgebraicGeometry.IsAffineOpen U → (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)).IsIntegral
-- Mathlib.Algebra.Module.PUnit
PUnit.smulWithZero : {R : Type u_1} → [inst : Zero R] → SMulWithZero R PUnit.{u_3 + 1}
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The functorial supremum on `MonoOver A` descends to a supremum on `Subobject A`.  -/
CategoryTheory.Subobject.sup : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasImages C] →
      [CategoryTheory.Limits.HasBinaryCoproducts C] →
        {A : C} →
          CategoryTheory.Functor (CategoryTheory.Subobject A)
            (CategoryTheory.Functor (CategoryTheory.Subobject A) (CategoryTheory.Subobject A))
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- A bordered minor is zero when its border column already occurs in the word.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.bminor_eq_zero_of_mem_range : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) {p : ℕ} {k : Fin n} (α : Fin p → Fin n)
  (i : Fin n), k ∈ Set.range α → BirdDet.bminor✝ A i k α = 0
-- Mathlib.NumberTheory.FactorisationProperties
Nat.instDecidablePseudoperfect : (n : ℕ) → Decidable n.Pseudoperfect
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.lift_eq_omega_one : ∀ {o : Ordinal.{u}}, Ordinal.lift.{v, u} o = Ordinal.omega 1 ↔ o = Ordinal.omega 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_le_size_insertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {l : List (α × β)}, t.size ≤ (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).size
-- Mathlib.Control.Traversable.Equiv
Equiv.naturality : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] [LawfulTraversable t]
  {F G : Type u → Type u} [inst_2 : Applicative F] [inst_3 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
  (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : t' α),
  (fun {α} => η.app α) (Equiv.traverse eqv f x) = Equiv.traverse eqv ((fun {α} => η.app α) ∘ f) x
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- A list of natural numbers `[i₀, ⋯, iₙ]` is said to be `m`-admissible (for `m : ℕ`) if
`i₀ < ⋯ < iₙ` and `iₖ ≤ m + k` for all `k`. This would suggest the definition
`L.IsChain (· < ·) ∧ ∀ k, (h : k < L.length) → L[k] ≤ m + k`.
However, we instead define `IsAdmissible` inductively and show, in
`isAdmissible_iff_isChain_and_le`, that this is equivalent to the non-inductive definition.
 -/
SimplexCategoryGenRel.IsAdmissible : ℕ → List ℕ → Prop
-- Init.Data.Nat.ToString
Nat.toList_repr : ∀ {n : ℕ}, n.repr.toList = Nat.toDigits 10 n
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.vandermonde_cons : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v0 : R) (v : Fin n → R),
  Matrix.vandermonde (Fin.cons v0 v) =
    Fin.cons (fun j => v0 ^ ↑j) fun i => Fin.cons 1 fun j => v i * Matrix.vandermonde v i j
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- A proof that `f` is equal, up to modification over a discrete set, to a product of `g`, canonical
factors prescribed by the divisor of `f`, and a factorized rational function with poles and zeros
only on the boundary of the ball.
 -/
Complex.ECanonicalDecomp.eventuallyEq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {R : ℝ},
  Complex.ECanonicalDecomp f g R →
    f =ᶠ[Filter.codiscreteWithin (Metric.closedBall 0 R)]
      ((∏ᶠ (u : ℂ), Complex.canonicalFactor R u ^ (-(MeromorphicOn.divisor f (Metric.ball 0 R)) u)) *
          ∏ᶠ (v : ℂ), (fun x => x - v) ^ (MeromorphicOn.divisor f (Metric.sphere 0 R)) v) •
        g
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the identity `Iso.refl f`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.id₂M : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.StructuralAtom
-- Mathlib.Control.LawfulFix
Part.Fix.le_f_of_mem_approx : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) {x : (a : α) → Part (β a)},
  x ∈ Part.Fix.approxChain f → x ≤ f x
-- Mathlib.Analysis.SpecificLimits.Normed
hasSum_geometric_of_norm_lt_one : ∀ {K : Type u_4} [inst : NormedDivisionRing K] {ξ : K}, ‖ξ‖ < 1 → HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_apply_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), toIcoDiv hp a (a + p) = 1
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.mk.sizeOf_spec : ∀ (toLocallyRingedSpace : AlgebraicGeometry.LocallyRingedSpace)
  (local_affine :
    ∀ (x : ↑toLocallyRingedSpace.toTopCat),
      ∃ U R,
        Nonempty (toLocallyRingedSpace.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))),
  sizeOf { toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine } =
    1 + sizeOf toLocallyRingedSpace
-- Aesop.Stats.Basic
Aesop.ForwardClusterStateStats.slots : Aesop.ForwardClusterStateStats → ℕ
-- Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
/-- `f □ (∅ ⟶ L)` lifts against `X ⟶ Y` if and only if `f` lifts against `L ⟹ X ⟶ L ⟹ Y`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [CategoryTheory.BraidedCategory C] {A B K L X Y : C} {f : A ⟶ B} {h : X ⟶ Y} (i : CategoryTheory.Limits.IsInitial K),
  CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk f □ CategoryTheory.Arrow.mk (i.to L)).hom h ↔
    CategoryTheory.HasLiftingProperty f ((CategoryTheory.ihom L).map h)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.restrict_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] (f : MeasureTheory.SimpleFunc α β),
  f.restrict ∅ = 0
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
BoundedContinuousFunction.toLp_norm_le : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ] [inst_5 : Fact (1 ≤ p)]
  {𝕜 : Type u_4} [inst_6 : NontriviallyNormedField 𝕜] [inst_7 : NormedSpace 𝕜 E],
  ‖BoundedContinuousFunction.toLp p μ 𝕜‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsMulTorsion`.

---

A predicate on a monoid saying that all elements are of finite order.  -/
Monoid.IsTorsion : (G : Type u_1) → [Monoid G] → Prop
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcConnected.sessionId : Lean.Lsp.RpcConnected → UInt64
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a non-degenerate right-angled triangle is positive, version subtracting
vectors.  -/
InnerProductGeometry.angle_sub_pos_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x = 0 ∨ y ≠ 0 → 0 < InnerProductGeometry.angle x (x - y)
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprodXIso_hom_fst_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) {Z : C} (h : K.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f i) h
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {fallback v : β}, (t.insert k v).getD a fallback = if cmp k a = Ordering.eq then v else t.getD a fallback
-- Mathlib.NumberTheory.RatFunc.Ostrowski
/-- A uniformizing element for the valuation `v`, as a polynomial in `K[X]`.  -/
_private.Mathlib.NumberTheory.RatFunc.Ostrowski.0.RatFunc.termπᵥ : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.removeZero_coeff_succ : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ), p.removeZero (n + 1) = p (n + 1)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_inf : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s t : TopologicalSpace.Closeds α), ↑(s ⊓ t) = ↑s ∩ ↑t
-- Mathlib.Algebra.Category.ModuleCat.AB
instHasSeparatorModuleCatOfSmall : ∀ (R : Type u) [inst : Ring R] [Small.{v, u} R], CategoryTheory.HasSeparator (ModuleCat R)
-- Mathlib.Analysis.Normed.Module.RCLike.Real
interior_closedBall' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ),
  interior (Metric.closedBall x r) = Metric.ball x r
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The identity linear change of variables given by the identity matrix.  -/
WeierstrassCurve.VariableChange.one_def : ∀ {R : Type u} [inst : CommRing R], 1 = { u := 1, r := 0, s := 0, t := 0 }
-- Mathlib.Computability.TuringMachine.Tape
/-- The tail of a `ListBlank` is well defined (up to the tail of blanks).  -/
Turing.ListBlank.tail : {Γ : Type u_1} → [inst : Inhabited Γ] → Turing.ListBlank Γ → Turing.ListBlank Γ