mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_insertNth_smul : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂) (p : Fin (n + 1))
  (m : (i : Fin n) → M (p.succAbove i)) (c : R) (x : M p), f (p.insertNth (c • x) m) = c • f (p.insertNth x m)
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_iUnion : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {ι : Sort u_4} (f : ι → Set M), PointedCone.dual p (⋃ i, f i) = ⨅ i, PointedCone.dual p (f i)
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonUnitalNonAssocCommSemiring` instance along a surjective function.  -/
Function.Surjective.nonUnitalNonAssocCommSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : SMul ℕ S] →
                [inst_4 : NonUnitalNonAssocCommSemiring R] →
                  f 0 = 0 →
                    (∀ (x y : R), f (x + y) = f x + f y) →
                      (∀ (x y : R), f (x * y) = f x * f y) →
                        (∀ (n : ℕ) (x : R), f (n • x) = n • f x) → NonUnitalNonAssocCommSemiring S
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
/-- Like `evalPropStep`, but specialized for `@Eq.{u} α a b`. When the values are equal, uses
`eq_true rfl` which requires no kernel evaluation. When different, calls `mkNeProof` to build
a proof of `a ≠ b`.
 -/
Lean.Meta.Simp.evalEqPropStep : Lean.Expr → Bool → Lean.Meta.SimpM Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm'_le_eLpNorm'_of_exponent_le : ∀ {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} {f : α → ε} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {p q : ℝ},
  0 < p →
    p ≤ q →
      ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ],
        MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.eLpNorm' f p μ ≤ MeasureTheory.eLpNorm' f q μ
-- Mathlib.Data.Int.Cast.Lemmas
zsmul_eq_mul' : ∀ {α : Type u_3} [inst : NonAssocRing α] (a : α) (n : ℤ), n • a = a * ↑n
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.mem_of_prefix : ∀ {A : Type u_1} {T : ↥(Descriptive.tree A)} {x y : List A}, x <+: y → y ∈ T → x ∈ T
-- Mathlib.Data.Int.GCD
pow_gcd_eq_one : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {m n : ℕ}, a ^ m.gcd n = 1 ↔ a ^ m = 1 ∧ a ^ n = 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_eq_some_getElem!_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, t.contains a = true → t[a]? = some t[a]!
-- Lean.Meta.Match.SimpH
/-- State for the equational theorem hypothesis simplifier.

Recall that each equation contains additional hypotheses to ensure the associated case does not taken by previous cases.
We have one hypothesis for each previous case.

Each hypothesis is of the form `forall xs, eqs → False`

We use tactics to minimize code duplication.
 -/
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.State : Type
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
_private.Mathlib.RingTheory.MvPowerSeries.GaussNorm.0.MvPowerSeries.c_prod_nonneg : ∀ {σ : Type u_2} (c : σ → ℝ), 0 ≤ c → ∀ (t : σ →₀ ℕ), 0 ≤ t.prod fun x1 x2 => c x1 ^ x2
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- A general sufficient condition for bounding `levyProkhorovEDist` from above.  -/
MeasureTheory.levyProkhorovEDist_le_of_forall_add_pos_le : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ ν : MeasureTheory.Measure Ω)
  (δ : ENNReal),
  (∀ (ε : ENNReal) (B : Set Ω),
      0 < ε →
        ε < ⊤ →
          MeasurableSet B →
            μ B ≤ ν (Metric.thickening (δ + ε).toReal B) + δ + ε ∧
              ν B ≤ μ (Metric.thickening (δ + ε).toReal B) + δ + ε) →
    MeasureTheory.levyProkhorovEDist μ ν ≤ δ
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraRing.involute_eq_id : ∀ {R : Type u_1} [inst : CommRing R], CliffordAlgebra.involute = AlgHom.id R (CliffordAlgebra 0)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
/-- Auxiliary predicate to express that a morphism is purely a composition of `σ i`s.  -/
SimplexCategoryGenRel.P_σ : CategoryTheory.MorphismProperty SimplexCategoryGenRel
-- Mathlib.Algebra.Group.Subgroup.Actions
Subgroup.instFaithfulSMulSubtypeMem : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [FaithfulSMul G α] (S : Subgroup G),
  FaithfulSMul (↥S) α
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.LocallyDirected.property_trans : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X}
  {inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀} [self : 𝒰.LocallyDirected] {i j : 𝒰.I₀} (hij : i ⟶ j),
  P (AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans hij)
-- Init.Data.List.TakeDrop
List.take.eq_def : ∀ {α : Type u} (x : ℕ) (x_1 : List α),
  List.take x x_1 =
    match x, x_1 with
    | 0, x => []
    | n.succ, [] => []
    | n.succ, a :: as => a :: List.take n as
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instIsNegApplyForall : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Ring R] [inst_1 : (i : ι) → AddCommGroup (M₁ i)]
  [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)] [inst_4 : Module R M₂]
  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂] [inst_7 : IsTopologicalAddGroup M₂],
  IsNegApply (ContinuousMultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lmap_eq_map : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) (x : DirectSum ι fun i => M i),
  (DirectSum.lmap f) x = (DirectSum.map fun i => (f i).toAddMonoidHom) x
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial.eq_2 : ∀ (n n_1 : ℕ), n.descFactorial n_1.succ = (n - n_1) * n.descFactorial n_1
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.fourierMultiplierCLM.eq_1 : ∀ {E : Type u_3} (F : Type u_4) [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] (g : E → ℂ),
  TemperedDistribution.fourierMultiplierCLM F g =
    FourierTransform.fourierInvCLM ℂ (TemperedDistribution E F) ∘SL
      TemperedDistribution.smulLeftCLM F g ∘SL FourierTransform.fourierCLM ℂ (TemperedDistribution E F)
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a subgroup is less or equal to the nilpotency class of the group.  -/
Subgroup.nilpotencyClass_le : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [hG : Group.IsNilpotent G],
  Group.nilpotencyClass ↥H ≤ Group.nilpotencyClass G
-- Mathlib.Topology.Closure
closure_inter_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, closure (s ∩ t) ⊆ closure s ∩ closure t
-- Mathlib.Algebra.Module.LinearMap.Defs
AddMonoidHom.toIntLinearMap_injective : ∀ {M : Type u_8} {M₂ : Type u_10} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂],
  Function.Injective AddMonoidHom.toIntLinearMap
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_comp_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type uF} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} (n : ℕ) (a : 𝕜),
  iteratedFDerivWithin 𝕜 n (fun x => f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- A finite group of order dividing a prime is cyclic.  -/
isCyclic_of_card_dvd_prime : ∀ {α : Type u_1} [inst : Group α] {p : ℕ} [hp : Fact (Nat.Prime p)], Nat.card α ∣ p → IsCyclic α
-- Mathlib.Computability.NFA
DFA.toNFA_start : ∀ {α : Type u} {σ : Type v} (M : DFA α σ), M.toNFA.start = {M.start}
-- Mathlib.Order.Lattice
/-- Pointwise maximum of two antitone functions is an antitone function.  -/
Antitone.max : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β},
  Antitone f → Antitone g → Antitone fun x => max (f x) (g x)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
OpenPartialHomeomorph.subtypeRestr.eq_1 : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s),
  e.subtypeRestr hs = (s.openPartialHomeomorphSubtypeCoe hs).trans e
-- Mathlib.Tactic.Linarith.Parsing
/-- `toComp red e e_map monom_map` converts an expression of the form `t < 0`, `t ≤ 0`, or `t = 0`
into a `comp` object.

`e_map` maps atomic expressions to indices; `monom_map` maps monomials to indices.
Both of these are updated during processing and returned.
 -/
Mathlib.Tactic.Linarith.toComp : Lean.Meta.TransparencyMode →
  Lean.Expr →
    Mathlib.Tactic.Linarith.ExprMap →
      Std.TreeMap Mathlib.Tactic.Linarith.Monom ℕ compare →
        Lean.MetaM
          (Mathlib.Tactic.Linarith.Comp ×
            Mathlib.Tactic.Linarith.ExprMap × Std.TreeMap Mathlib.Tactic.Linarith.Monom ℕ compare)
-- Mathlib.NumberTheory.Real.Irrational
irrational_inv_iff : ∀ {x : ℝ}, Irrational x⁻¹ ↔ Irrational x
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : Subsingleton S],
  algebraMap (MvPolynomial PUnit.{u_2 + 1} R) S = (MvPolynomial.aeval fun x => 1).toRingHom
-- Std.Data.Internal.List.Associative
Std.Internal.List.perm_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
      (∀ (a : α), Std.Internal.List.containsKey a l = true → (List.map Sigma.fst toInsert).contains a = false) →
        (Std.Internal.List.insertList l toInsert).Perm (l ++ toInsert)
-- Lean.Widget.Commands
/-- Use `#widget <widget>` to display a panel widget,
and `#widget <widget> with <props>` to display it with the given props.
Useful for debugging widgets.

The type of `<widget>` must implement `Widget.ToModule`,
and the type of `<props>` must implement `Server.RpcEncodable`.
In particular, `<props> : Json` works.  -/
Lean.Widget.widgetCmd : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
/-- Composition of two $C^{k+(α)}$ functions, `k ≠ 0`, is a $C^{k+(α)}$ function.  -/
ContDiffPointwiseHolderAt.comp : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {k : ℕ} {α : ↑unitInterval} {f : E → F} (a : E) {g : F → G},
  ContDiffPointwiseHolderAt k α g (f a) →
    ContDiffPointwiseHolderAt k α f a → k ≠ 0 → ContDiffPointwiseHolderAt k α (g ∘ f) a
-- Init.Data.BitVec.Lemmas
BitVec.rotateLeft.eq_1 : ∀ {w : ℕ} (x : BitVec w) (n : ℕ), x.rotateLeft n = x.rotateLeftAux (n % w)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.instCategoryWithHomologyOpposite : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.CategoryWithHomology C], CategoryTheory.CategoryWithHomology Cᵒᵖ
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.tprod_apply : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (x : Fin n → M), (TensorAlgebra.tprod R M n) x = (List.ofFn fun i => (TensorAlgebra.ι R) (x i)).prod
-- Mathlib.GroupTheory.Coset.Basic
mem_own_rightAddCoset : ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) (a : α), a ∈ AddOpposite.op a +ᵥ ↑s
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.range_asIdeal : ∀ (R : Type u) [inst : CommSemiring R], Set.range PrimeSpectrum.asIdeal = {J | J.IsPrime}
-- Batteries.Logic
not_nonempty_pempty : ¬Nonempty PEmpty.{u_1}
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (m₁ : Z₁₂ ⟶ Z₁₃) (m₃ : Z₁₃ ⟶ Z₂₃)
  (comm₁ : CategoryTheory.CategoryStruct.comp v₁₂ m₁ = CategoryTheory.CategoryStruct.comp u₂₃ v₁₃)
  (comm₂ : CategoryTheory.CategoryStruct.comp m₁ w₁₃ = w₁₂) (comm₃ : CategoryTheory.CategoryStruct.comp v₁₃ m₃ = v₂₃)
  (comm₄ :
    CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map u₁₂) =
      CategoryTheory.CategoryStruct.comp m₃ w₂₃)
  (mem :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
        (CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂)) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (m₁_1 : Z₁₂ ⟶ Z₁₃) (m₃_1 : Z₁₃ ⟶ Z₂₃)
  (comm₁_1 : CategoryTheory.CategoryStruct.comp v₁₂ m₁_1 = CategoryTheory.CategoryStruct.comp u₂₃ v₁₃)
  (comm₂_1 : CategoryTheory.CategoryStruct.comp m₁_1 w₁₃ = w₁₂)
  (comm₃_1 : CategoryTheory.CategoryStruct.comp v₁₃ m₃_1 = v₂₃)
  (comm₄_1 :
    CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map u₁₂) =
      CategoryTheory.CategoryStruct.comp m₃_1 w₂₃)
  (mem_1 :
    CategoryTheory.Pretriangulated.Triangle.mk m₁_1 m₃_1
        (CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂)) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles),
  ({ m₁ := m₁, m₃ := m₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃, comm₄ := comm₄, mem := mem } =
      { m₁ := m₁_1, m₃ := m₃_1, comm₁ := comm₁_1, comm₂ := comm₂_1, comm₃ := comm₃_1, comm₄ := comm₄_1,
        mem := mem_1 }) =
    (m₁ = m₁_1 ∧ m₃ = m₃_1)
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.composePath_toPath : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.composePath f.toPath = f
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.toListModel.eq_1 : ∀ {α : Type u} {β : α → Type v} (buckets : Array (Std.DHashMap.Internal.AssocList α β)),
  Std.DHashMap.Internal.toListModel buckets = List.flatMap Std.DHashMap.Internal.AssocList.toList buckets.toList
-- Mathlib.Topology.ClusterPt
mapClusterPt_comp : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {β : Type u_2} {F : Filter α} {x : X} {φ : α → β} {u : β → X},
  MapClusterPt x F (u ∘ φ) ↔ MapClusterPt x (Filter.map φ F) u
-- Batteries.Data.Fin.Fold
Fin.dfoldr_eq_dfoldrM : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} (f : (i : Fin n) → α i.succ → α i.castSucc) (x : α (Fin.last n)),
  Fin.dfoldr n α f x = Fin.dfoldrM n α f x
-- Init.Data.Slice.Basic
/-- This typeclass determines that some type `α` is equal to `β` and that `β` should be used in APIs
instead of `α`.

`Self` is used in the polymorphic slice library.
 -/
Std.Slice.Self : Type u → outParam (Type u) → Prop
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basis.congr_simp : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι] (s s_1 : Finset ι),
  s = s_1 → ∀ (v v_1 : ι → F), v = v_1 → ∀ (i i_1 : ι), i = i_1 → Lagrange.basis s v i = Lagrange.basis s_1 v_1 i_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_alter_le_size : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β}, (m.alter k f).size ≤ m.size + 1
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_hom_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_hom_app._auto_1)
  {Z : C} (h : (CategoryTheory.shiftFunctor C n).obj ((CategoryTheory.unopUnop C).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso C n).hom.app X) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app X).unop.unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app (Opposite.unop X)).unop h)
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- We state it as a simp lemma, which is regarded as an involved version of
`id_whiskerRight f g : 𝟙 f ▷ g = 𝟙 (f ≫ g)`.
 -/
CategoryTheory.Bicategory.leftUnitor_whiskerRight_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).hom g) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).hom h)
-- Init.Data.List.Monadic
List.zipWithM_cons_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {a : α} {as : List α} {b : β} {bs : List β}
  [inst : Monad m] [LawfulMonad m] {f : α → β → m γ},
  List.zipWithM f (a :: as) (b :: bs) = do
    let __do_lift ← f a b
    let __do_lift_1 ← List.zipWithM f as bs
    pure (__do_lift :: __do_lift_1)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.combine : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.exists_nil_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, (∃ p, p.Nil) ↔ u = v
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Unique.mk.congr_simp : ∀ {α : Sort u} (toInhabited toInhabited_1 : Inhabited α) (e_toInhabited : toInhabited = toInhabited_1)
  (uniq : ∀ (a : α), a = default),
  { toInhabited := toInhabited, uniq := uniq } = { toInhabited := toInhabited_1, uniq := ⋯ }
-- Mathlib.Data.Finsupp.MonomialOrder
/-- A `WithBot m.syn` version of `m.toSyn`.  -/
MonomialOrder.toWithBotSyn : {σ : Type u_1} → (m : MonomialOrder σ) → WithBot (σ →₀ ℕ) ≃+ WithBot m.syn
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.decidableMemCentralizer.eq_1 : ∀ {M : Type u_1} {S : Set M} [inst : AddSemigroup M] (a : M) [inst_1 : Decidable (∀ b ∈ S, b + a = a + b)],
  AddSubsemigroup.decidableMemCentralizer a = decidable_of_iff' (∀ g ∈ S, g + a = a + g) ⋯
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.PrimeSpectrum.comap_residue : ∀ (T : Type u) [inst : CommRing T] [inst_1 : IsLocalRing T] (x : PrimeSpectrum (IsLocalRing.ResidueField T)),
  PrimeSpectrum.comap (IsLocalRing.residue T) x = IsLocalRing.closedPoint T
-- Mathlib.Order.Basic
LE.le.ge_or_lt : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, a ≤ b → ∀ (c : α), a ≤ c ∨ c < b
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pos.skipWhile.eq_def : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  pos.skipWhile pat =
    match pos.skip? pat with
    | some nextCurr => if pos < nextCurr then nextCurr.skipWhile pat else pos
    | none => pos
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toLinearMap_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (v : V), f.toLinearMap v = f v
-- Mathlib.Data.Nat.Nth
Nat.filter_range_nth_subset_insert : ∀ (p : ℕ → Prop) [inst : DecidablePred p] (k : ℕ),
  {n ∈ Finset.range (Nat.nth p (k + 1)) | p n} ⊆ insert (Nat.nth p k) ({n ∈ Finset.range (Nat.nth p k) | p n})
-- Mathlib.Order.Filter.AtTopBot.Monoid
/-- If `f` is eventually bounded from above along `l` and `f * g` tends to `+∞`,
then `g` tends to `+∞`.  -/
Filter.Tendsto.atTop_of_isBoundedUnder_le_mul : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f →
    Filter.Tendsto (fun x => f x * g x) l Filter.atTop → Filter.Tendsto g l Filter.atTop
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.inj : Lean.Meta.Grind.InjectiveTheorem → Lean.Meta.Grind.Entry
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.codeSupp'.match_1.eq_1 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.zero' → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.succ → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.tail → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (c f fs : Turing.ToPartrec.Code) → c = f.cons fs → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (c f g : Turing.ToPartrec.Code) → c = f.comp g → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (c f g : Turing.ToPartrec.Code) → c = f.case g → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (c f : Turing.ToPartrec.Code) → c = f.fix → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match Turing.ToPartrec.Code.zero', k with
    | c@h:Turing.ToPartrec.Code.zero', k => h_1 c h k
    | c@h:Turing.ToPartrec.Code.succ, k => h_2 c h k
    | c@h:Turing.ToPartrec.Code.tail, k => h_3 c h k
    | c@h:(f.cons fs), k => h_4 c f fs h k
    | c@h:(f.comp g), k => h_5 c f g h k
    | c@h:(f.case g), k => h_6 c f g h k
    | c@h:f.fix, k => h_7 c f h k) =
    h_1 Turing.ToPartrec.Code.zero' ⋯ k
-- Mathlib.Computability.TuringMachine.Computable
Turing.inhabitedTM2EvalsTo : Inhabited (StateTransition.EvalsTo (fun x => some PUnit.unit) PUnit.unit (some PUnit.unit))