mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instAddMonoid.eq_1 : ∀ {α : Type u} [inst : AddMonoid α],
  AddUnits.instAddMonoid =
    { toAdd := inferInstance.toAdd, add_assoc := ⋯, toZero := inferInstance.toZero, zero_add := ⋯, add_zero := ⋯,
      nsmul := fun n a => { val := n • ↑a, neg := n • ↑(-a), val_neg := ⋯, neg_val := ⋯ }, nsmul_zero := ⋯,
      nsmul_succ := ⋯ }
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.basis.eq_1 : ∀ (G : Type u_1) [inst : Group G] [inst_1 : IsFreeGroup G],
  IsFreeGroup.basis G = { repr := (IsFreeGroup.mulEquiv G).symm }
-- Mathlib.GroupTheory.HNNExtension
MulAction.toEndHom.eq_1 : ∀ {M : Type u_2} {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M α],
  MulAction.toEndHom = { toFun := fun x1 x2 => x1 • x2, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.Adj.degree_pos_right : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V} [inst : Fintype ↑(G.neighborSet v)] {w : V}, G.Adj w v → 0 < G.degree v
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β}, t.isEmpty = true → (t.insertIfNew k v).minKey! = k
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightMono α] {a b c d : α},
  a ≤ b → c ≤ d → a + c ≤ b + d
-- Init.Data.BitVec.Lemmas
/-- Unsigned division never overflows.  -/
BitVec.toNat_div_toNat_lt : ∀ {w : ℕ} {x y : BitVec w}, x.toNat / y.toNat < 2 ^ w
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmaKey : Type
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_smul`. -/
EMetric.infEdist_smul : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {M : Type u_2} [inst_1 : SMul M α] [IsIsometricSMul M α] (c : M) (x : α)
  (s : Set α), Metric.infEDist (c • x) (c • s) = Metric.infEDist x s
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_X : ∀ {F : Type u} [inst : Field F], Polynomial.X.natSepDegree = 1
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.support_eq_empty_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [HereditarilyLindelofSpace X], μ.support = ∅ ↔ μ = 0
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.isRegular_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), IsRegular (Polynomial.X ^ n)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_eq_getD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, Std.DTreeMap.Raw.Const.get! t a = Std.DTreeMap.Raw.Const.getD t a default
-- Mathlib.Computability.Primrec.Basic
Primcodable.mk : {α : Type u_1} →
  [toEncodable : Encodable α] → (Nat.Primrec fun n => Encodable.encode (Encodable.decode n)) → Primcodable α
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The fifth simplicial identity  -/
CategoryTheory.SimplicialObject.σ_comp_σ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i j : Fin (n + 1)},
  i ≤ j →
    CategoryTheory.CategoryStruct.comp (X.σ j) (X.σ i.castSucc) =
      CategoryTheory.CategoryStruct.comp (X.σ i) (X.σ j.succ)
-- Init.Data.Fin.Lemmas
Fin.eq_last_of_not_lt : ∀ {n : ℕ} {i : Fin (n + 1)}, ¬↑i < n → i = Fin.last n
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_univ : ∀ {α : Type u_3} {β : α → Type u_4} [inst : DecidableEq α] [inst_1 : Fintype α] [inst_2 : (a : α) → Fintype (β a)],
  (Fintype.piFinset fun a => Finset.univ) = Finset.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Coequifibered.comp : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G H : CategoryTheory.Functor J C} {α : F ⟶ G} {β : G ⟶ H},
  CategoryTheory.NatTrans.Coequifibered α →
    CategoryTheory.NatTrans.Coequifibered β →
      CategoryTheory.NatTrans.Coequifibered (CategoryTheory.CategoryStruct.comp α β)
-- Mathlib.Data.Nat.Factorization.Root
Nat.floorRoot_one_left : ∀ (a : ℕ), Nat.floorRoot 1 a = a
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.map_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D), (sq.map F).X₂ = F.obj sq.X₂
-- Init.Data.Option.Lemmas
Option.lt.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (x_2 : α) (y : β), Option.lt r (some x_2) (some y) = r x_2 y
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.coe_top : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G], ↑⊤ = Set.univ
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- A group extension is equivalent to itself.  -/
GroupExtension.Equiv.refl : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} → [inst : Group N] → [inst_1 : Group E] → [inst_2 : Group G] → (S : GroupExtension N E G) → S.Equiv S
-- Init.Data.Array.Lemmas
Array.filter_congr : ∀ {α : Type u_1} {xs ys : Array α},
  xs = ys →
    ∀ {f g : α → Bool},
      f = g →
        ∀ {start stop start' stop' : ℕ},
          start = start' → stop = stop' → Array.filter f xs start stop = Array.filter g ys start' stop'
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.baseChange_negAddY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Affine R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (x₁ y₁ x₂ ℓ : A),
  (W'.baseChange B).negAddY (f x₁) (f x₂) (f y₁) (f ℓ) = f ((W'.baseChange A).negAddY x₁ x₂ y₁ ℓ)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_diff_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₁, a ∉ m₂) → (m₁ \ m₂).size = m₁.size
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.nonpos_iff_eq_zero' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ ≤ 0 ↔ μ = 0
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftEq.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l l' : L₁ ⟶ L₂) (h : l = l'),
  CategoryTheory.Comma.mapLeftEq R l l' h =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.Comma.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Comma.mapLeft R l).obj X).left)
          (CategoryTheory.Iso.refl ((CategoryTheory.Comma.mapLeft R l).obj X).right) ⋯)
      ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.size + t₂.size = (t₁ ∪ t₂).size + (t₁ ∩ t₂).size
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_iff_zpow_tendsto_zero : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [inst : TopologicalSpace β] [inst_1 : Field β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop →
    (Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), Filter.Tendsto (fun a => k a ^ z * f a) l (nhds 0))
-- Mathlib.Geometry.Convex.Cone.Simplicial
/-- A pointed cone is simplicial if it equals the conic hull of a finite set that is linearly
independent over `R`.  -/
PointedCone.IsSimplicial : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] → [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → PointedCone R M → Prop
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Ici_iff_integrableOn_Ioi : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {b : α} [MeasureTheory.NullSingletonClass μ],
  autoParam (‖f b‖ₑ ≠ ⊤) integrableOn_Ici_iff_integrableOn_Ioi._auto_1 →
    (MeasureTheory.IntegrableOn f (Set.Ici b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioi b) μ)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.zero_tprodCoeff' : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (z : R) (f : (i : ι) → s i) (i : ι),
  f i = 0 → PiTensorProduct.tprodCoeff R z f = 0
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
/-- `0` is topologically nilpotent  -/
IsTopologicallyNilpotent.zero : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : MonoidWithZero R], IsTopologicallyNilpotent 0
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.mem_map_equiv : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {τ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair τ₁₂ τ₂₁] [inst_7 : RingHomInvPair τ₂₁ τ₁₂] (p : Submodule R M)
  {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂}, x ∈ Submodule.map (↑e) p ↔ e.symm x ∈ p
-- Mathlib.RingTheory.DividedPowers.DPMorphism
/-- If two divided power structures on the ideal `I` agree on a generating set, then they are
equal.
See [N. Roby, *Les algèbres à puissances dividées* (Corollary to Proposition 3)][Roby-1965].  -/
DividedPowers.dpow_eq_from_gens : ∀ {A : Type u_3} [inst : CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I) {S : Set A},
  I = Ideal.span S → (∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a) → hI' = hI
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.zero_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K), 0 = { left := 0, right := 0 }
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_subset_iff : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {s : Set ι} {f : Π₀ (i : ι), β i},
  ↑f.support ⊆ s ↔ ∀ i ∉ s, f i = 0
-- Mathlib.Logic.Equiv.Sum
Equiv.sumComm_symm : ∀ (α : Type u_9) (β : Type u_10), (Equiv.sumComm α β).symm = Equiv.sumComm β α
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context.mk : Lean.InductiveVal →
  List Lean.Level →
    Array Lean.Expr → Array Lean.Name → Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.Elab.ComputedFields.Context
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.Homotopic.symm : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} {f g : ↑(GenLoop N X x)},
  GenLoop.Homotopic f g → GenLoop.Homotopic g f
-- Lean.Environment
Lean.Kernel.Exception.deterministicTimeout.sizeOf_spec : sizeOf Lean.Kernel.Exception.deterministicTimeout = 1
-- Lean.Meta.Tactic.Grind.Injective
Lean.Meta.Grind.Extension.addInjectiveAttr : Lean.Meta.Grind.Extension → Lean.Name → Lean.AttributeKind → Lean.MetaM Unit
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.neg.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} [inst_1 : SizeOf J]
  (a : RingCat.Colimits.Prequotient F), sizeOf a.neg = 1 + sizeOf a
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.Martingale.ae_not_tendsto_atTop_atBot : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Martingale f ℱ μ →
    (∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) →
      ∀ᵐ (ω : Ω) ∂μ, ¬Filter.Tendsto (fun n => f n ω) Filter.atTop Filter.atBot
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter_eq_add_one : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  k ∉ t →
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true →
      (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.size = t.size + 1
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_add : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f g : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  μ.Integrable f → μ.Integrable g → ∫ᵛ (x : X), (f + g) x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.List.filterMapM_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_add_of_natDegree_lt_left : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R},
  q.natDegree < p.natDegree → (p + q).eraseLead = p.eraseLead + q
-- Init.Data.SInt.Bitwise
instAssociativeInt32HOr : Std.Associative fun x1 x2 => x1 ||| x2
-- Mathlib.FieldTheory.Minpoly.Field
Irreducible.dvd_iff_aeval_eq_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] [Nontrivial B]
  {p q : Polynomial A}, Irreducible p → ∀ {b : B}, (Polynomial.aeval b) p = 0 → ((Polynomial.aeval b) q = 0 ↔ p ∣ q)
-- Mathlib.Order.Concept
gc_upperPolar_lowerPolar : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop),
  GaloisConnection (⇑OrderDual.toDual ∘ upperPolar r) (lowerPolar r ∘ ⇑OrderDual.ofDual)
-- Init.Sym.Lemmas
Lean.Sym.Nat.eq_eq_false : ∀ (a b : ℕ), decide (a = b) = false → (a = b) = False
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae : ∀ {K : Type u_1} [inst : Field K] (A : Set (NumberField.mixedEmbedding.mixedSpace K)),
  (∀ (x : NumberField.mixedEmbedding.mixedSpace K), x ∈ A ↔ (fun w => ‖x.1 w‖, x.2) ∈ A) →
    ∀ [inst_1 : NumberField K],
      ⋃ s, ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A =ᵐ[MeasureTheory.volume] A
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ] {a b t : ℝ},
  AEMeasurable X μ →
    (∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) →
      ∫ (x : Ω), X x ∂μ = 0 → 0 < t → ProbabilityTheory.mgf X μ t ≤ Real.exp ((↑‖b - a‖₊ / 2) ^ 2 * t ^ 2 / 2)
-- Mathlib.Computability.DFA
DFA.inter_accept : ∀ {α : Type u} {σ1 σ2 : Type v} (M1 : DFA α σ1) (M2 : DFA α σ2),
  (M1.inter M2).accept = {s | s.1 ∈ M1.accept ∧ s.2 ∈ M2.accept}
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `sInf s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are nonnegative to show that `0 ≤ sInf s`.  -/
Real.sInf_nonneg : ∀ {s : Set ℝ}, (∀ x ∈ s, 0 ≤ x) → 0 ≤ sInf s
-- Init.Sym.Lemmas
Lean.Sym.UInt32.lt_eq_true : ∀ (a b : UInt32), decide (a < b) = true → (a < b) = True
-- Mathlib.Order.WithBot
WithBot.unbot.congr_simp : ∀ {α : Type u_1} (x x_1 : WithBot α) (e_x : x = x_1) (a : x ≠ ⊥), x.unbot a = x_1.unbot ⋯
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
_private.Mathlib.CategoryTheory.Triangulated.SpectralObject.0.CategoryTheory.ComposableArrows.Precomp.obj.match_1.eq_2 : ∀ {n : ℕ} (motive : Fin (n + 1 + 1) → Sort u_1) (i : ℕ) (hi : i + 1 < n + 1 + 1)
  (h_1 : (isLt : 0 < n + 1 + 1) → motive ⟨0, isLt⟩) (h_2 : (i : ℕ) → (hi : i + 1 < n + 1 + 1) → motive ⟨i.succ, hi⟩),
  (match ⟨i.succ, hi⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨i.succ, hi⟩ => h_2 i hi) =
    h_2 i hi
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.abs_valMinAbs_eq_abs_valMinAbs : ∀ {n : ℕ} {a b : ZMod n}, |a.valMinAbs| = |b.valMinAbs| ↔ a = b ∨ a = -b
-- Mathlib.RingTheory.TensorProduct.Free
Algebra.TensorProduct.instFree : ∀ (R : Type u_3) (A : Type u_4) (M : Type u_5) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : CommSemiring A] [inst_5 : Algebra R A], Module.Free A (TensorProduct R A M)
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.isEmpty.eq_2 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k' : α) (v : β k') (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).isEmpty = false
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.reindex_toPreSubmersivePresentation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} [inst_4 : Finite σ']
  (e : ι' ≃ ι) (f : σ' ≃ σ), (P.reindex e f).toPreSubmersivePresentation = P.reindex e f
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.trAux.match_1.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → σ → Sort u_4) (a : Γ → σ → σ)
  (q : Turing.TM1.Stmt Γ Λ σ) (v : σ)
  (h_1 : (d : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.move d q) v)
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.write a q) v)
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.load a q) v)
  (h_4 : (p : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → motive (Turing.TM1.Stmt.goto l) v) (h_6 : (v : σ) → motive Turing.TM1.Stmt.halt v),
  (match Turing.TM1.Stmt.load a q, v with
    | Turing.TM1.Stmt.move d q, v => h_1 d q v
    | Turing.TM1.Stmt.write a q, v => h_2 a q v
    | Turing.TM1.Stmt.load a q, v => h_3 a q v
    | Turing.TM1.Stmt.branch p q₁ q₂, v => h_4 p q₁ q₂ v
    | Turing.TM1.Stmt.goto l, v => h_5 l v
    | Turing.TM1.Stmt.halt, v => h_6 v) =
    h_3 a q v
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.natTransLift_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F G : CategoryTheory.Functor (CategoryTheory.Quotient r) D)
  (τ : (CategoryTheory.Quotient.functor r).comp F ⟶ (CategoryTheory.Quotient.functor r).comp G) (X : C),
  (CategoryTheory.Quotient.natTransLift r τ).app ((CategoryTheory.Quotient.functor r).obj X) = τ.app X
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_eq_re_of_isSelfAdjoint : ∀ {K : Type u_1} [inst : RCLike K] {x : K} {y : ℝ}, IsSelfAdjoint x → (y = RCLike.re x ↔ ↑y = x)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.one_le_div_ae : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : Group β] [inst_1 : LE β]
  [MulRightMono β] (f g : α → β), 1 ≤ᵐ[μ] g / f ↔ f ≤ᵐ[μ] g
-- Init.Data.BEq
bne_comm : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {a b : α}, (a != b) = (b != a)
-- Mathlib.Tactic.TermCongr
Mathlib.Tactic.TermCongr.CongrType.eq : Mathlib.Tactic.TermCongr.CongrType
-- Mathlib.Order.RelSeries
/-- Given the series `a₀ -r→ … -r→ aᵢ -r→ … -r→ aₙ`, the series `aᵢ₊₁ -r→ … -r→ aₙ`.  -/
RelSeries.drop : {α : Type u_1} → {r : SetRel α α} → (p : RelSeries r) → Fin (p.length + 1) → RelSeries r
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.le_of_le : ∀ {α : Type u_1} {a a' b b' : α} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α],
  a ≤ b → a' + b ≤ b' + a → a' ≤ b'
-- Init.Data.List.Nat.TakeDrop
List.length_take_of_le : ∀ {i : ℕ} {α : Type u_1} {l : List α}, i ≤ l.length → (List.take i l).length = i
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
/-- The derivative of `polarCoord.symm` on `ι → ℝ × ℝ`, see `hasFDerivAt_pi_polarCoord_symm`.  -/
fderivPiPolarCoordSymm : {ι : Type u_1} → (ι → ℝ × ℝ) → (ι → ℝ × ℝ) →L[ℝ] ι → ℝ × ℝ
-- Mathlib.CategoryTheory.Square
/-- the bottom-right object  -/
CategoryTheory.Square.X₄ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C → C
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddMonoid : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [AddMonoid M] → AddMonoid (l.Germ M)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : K},
  x ≠ 0 →
    ∑ w,
        ↑NumberField.mixedEmbedding.fundamentalCone.expMap.symm
          (NumberField.mixedEmbedding.normAtAllPlaces ((NumberField.mixedEmbedding K) x)) w =
      Real.log ↑|(Algebra.norm ℚ) x|
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.instFintypeSubtypeMemOfDecidablePred.eq_1 : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) [inst_1 : DecidablePred fun x => x ∈ K] [inst_2 : Fintype G],
  K.instFintypeSubtypeMemOfDecidablePred = inferInstance
-- Mathlib.Data.Int.Cast.Lemmas
/-- If `α` is commutative, `zpowersHom` is a multiplicative equivalence.  -/
zpowersMulHom : (α : Type u_3) → [inst : CommGroup α] → α ≃* (Multiplicative ℤ →* α)
-- Mathlib.Algebra.Group.Defs
neg_add_rev : ∀ {G : Type u_1} [inst : SubtractionMonoid G] (a b : G), -(a + b) = -b + -a
-- Mathlib.Data.Nat.Factorization.LCM
Nat.factorizationLCMLeft_dvd_left : ∀ (a b : ℕ), a.factorizationLCMLeft b ∣ a
-- Batteries.Data.List.Lemmas
List.max!_eq_max_of_ne_nil : ∀ {α : Type u_1} [inst : Inhabited α] [inst_1 : Max α] (l : List α) (hl : l ≠ []), l.max! = l.max hl
-- Mathlib.GroupTheory.Complement
/-- A right transversal is in bijection with right cosets.  -/
Subgroup.IsComplement.rightQuotientEquiv : {G : Type u_1} →
  [inst : Group G] →
    {H : Subgroup G} → {T : Set G} → Subgroup.IsComplement (↑H) T → Quotient (QuotientGroup.rightRel H) ≃ ↑T
-- Mathlib.Order.Cover
/-- An `iff` version of `WCovBy.eq_or_eq` and `wcovBy_of_eq_or_eq`.  -/
wcovBy_iff_le_and_eq_or_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b ↔ a ≤ b ∧ ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b
-- Mathlib.Algebra.Regular.Prod
Prod.isLeftRegular_mk : ∀ {R : Type u_2} {S : Type u_3} [inst : Mul R] [inst_1 : Mul S] {a : R} {b : S},
  IsLeftRegular (a, b) ↔ IsLeftRegular a ∧ IsLeftRegular b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addXYZ_X : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P Q : Fin 3 → R), W'.addXYZ P Q 0 = W'.addX P Q
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.dirac_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] (x : α), (MeasureTheory.Measure.dirac x).prod ν = MeasureTheory.Measure.map (Prod.mk x) ν
-- Mathlib.Probability.Distributions.Pareto
ProbabilityTheory.paretoMeasure.eq_1 : ∀ (t r : ℝ), ProbabilityTheory.paretoMeasure t r = MeasureTheory.volume.withDensity (ProbabilityTheory.paretoPDF t r)
-- Mathlib.Algebra.Symmetrized
/-- The symmetrization of a real (unital, associative) algebra is a non-associative ring.  -/
SymAlg.instNonAssocRingOfInvertibleOfNat : {α : Type u_1} → [inst : Ring α] → [Invertible 2] → NonAssocRing αˢʸᵐ
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.discard.eq_1 : ∀ (α : Type u_4) [inst : MeasurableSpace α],
  ProbabilityTheory.Kernel.discard α = ProbabilityTheory.Kernel.deterministic (fun x => PUnit.unit) ⋯