mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mk.inj : ∀ {X : Type u_1} {R : Type u_2} {inst : Zero X} {inst_1 : Zero R} {inst_2 : TopologicalSpace X}
  {inst_3 : TopologicalSpace R} {toContinuousMap : C(X, R)} {map_zero' : toContinuousMap 0 = 0}
  {toContinuousMap_1 : C(X, R)} {map_zero'_1 : toContinuousMap_1 0 = 0},
  { toContinuousMap := toContinuousMap, map_zero' := map_zero' } =
      { toContinuousMap := toContinuousMap_1, map_zero' := map_zero'_1 } →
    toContinuousMap = toContinuousMap_1
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_le_add_iff : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a + b ↔ Cardinal.aleph0 ≤ a ∨ Cardinal.aleph0 ≤ b
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.mk.congr_simp : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (toLinearMap toLinearMap_1 : L →ₗ[R] M) (e_toLinearMap : toLinearMap = toLinearMap_1)
  (leibniz' : ∀ (a b : L), toLinearMap ⁅a, b⁆ = ⁅a, toLinearMap b⁆ - ⁅b, toLinearMap a⁆),
  { toLinearMap := toLinearMap, leibniz' := leibniz' } = { toLinearMap := toLinearMap_1, leibniz' := ⋯ }
-- Mathlib.FieldTheory.SeparableClosure
/-- The (relative) separable closure of `F` in `E`, or called maximal separable subextension
of `E / F`, is defined to be the intermediate field of `E / F` consisting of all separable
elements. The previous results prove that these elements are closed under field operations.  -/
separableClosure : (F : Type u) → (E : Type v) → [inst : Field F] → [inst_1 : Field E] → [inst_2 : Algebra F E] → IntermediateField F E
-- Mathlib.Geometry.Euclidean.MongePoint
/-- `mongePointVSubFaceCentroidWeightsWithCircumcenter` is the
result of subtracting `centroidWeightsWithCircumcenter` from
`mongePointWeightsWithCircumcenter`.  -/
Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub : ∀ {n : ℕ} {i₁ i₂ : Fin (n + 3)},
  i₁ ≠ i₂ →
    Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ =
      Affine.Simplex.mongePointWeightsWithCircumcenter n - Affine.Simplex.centroidWeightsWithCircumcenter {i₁, i₂}ᶜ
-- Mathlib.Algebra.Ring.Defs
/-- One is a right neutral element for multiplication  -/
NonAssocSemiring.mul_one : ∀ {α : Type u} [self : NonAssocSemiring α] (a : α), a * 1 = a
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.beq.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  [inst_3 : (k : α) → BEq (β k)] (m₁ m₂ : Std.DHashMap.Raw α β),
  m₁.beq m₂ =
    if h : 0 < m₁.buckets.size ∧ 0 < m₂.buckets.size then Std.DHashMap.Internal.Raw₀.beq ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩ else false
-- Mathlib.Topology.ContinuousMap.Polynomial
polynomialFunctions.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] (X : Set R),
  polynomialFunctions X = Subalgebra.map (Polynomial.toContinuousMapOnAlgHom X) ⊤
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.below.oracle : ∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop} (g : ℕ →. ℕ) (a : g ∈ O),
  Nat.RecursiveIn.below ⋯
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz
on a neighborhood of `x₀` then its derivative at `x₀` has norm bounded by `C`.
Version using `deriv`.  -/
norm_deriv_le_of_lipschitzOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x₀ : 𝕜} {s : Set 𝕜},
  s ∈ nhds x₀ → ∀ {C : NNReal}, LipschitzOnWith C f s → ‖deriv f x₀‖ ≤ ↑C
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.append.eq_2 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (x : Turing.ListBlank Γ) (a : Γ) (l : List Γ),
  Turing.ListBlank.append (a :: l) x = Turing.ListBlank.cons a (Turing.ListBlank.append l x)
-- Mathlib.Order.Hom.Bounded
BotHom.id_apply : ∀ {α : Type u_2} [inst : Bot α] (a : α), (BotHom.id α) a = a
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
Matrix.gram_apply : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : Inner 𝕜 E] (v : n → E) (i j : n),
  Matrix.gram 𝕜 v i j = inner 𝕜 (v i) (v j)
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.RiemannianMetric.mk : {B : Type u_4} →
  {E : B → Type u_6} →
    [inst : (b : B) → TopologicalSpace (E b)] →
      [inst_1 : (b : B) → AddCommGroup (E b)] →
        [inst_2 : (b : B) → Module ℝ (E b)] →
          (inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) →
            (∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v) →
              (∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v) →
                (∀ (b : B), ContinuousAt (fun v => ((inner b) v) v) 0) →
                  (∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1}) → Bundle.RiemannianMetric E
-- Mathlib.Data.Sigma.Basic
Prod.toSigma_mk : ∀ {α : Type u_7} {β : Type u_8} (x : α) (y : β), (x, y).toSigma = ⟨x, y⟩
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k k' : α} [hi : Inhabited β] {f : β → β},
      Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.Const.modify m k f) k' =
        if (k == k') = true then (Option.map f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).get!
        else Std.DHashMap.Internal.Raw₀.Const.get! m k'
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.close.sizeOf_spec : ∀ {β : Type} [inst : SizeOf β], sizeOf Std.Http.Server.Connection.Recv.close✝ = 1
-- Mathlib.RingTheory.Artinian.Module
instIsNoetherianRingMatrix : ∀ (n : Type u_1) (R : Type u_2) [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Ring R] [IsNoetherianRing R],
  IsNoetherianRing (Matrix n n R)
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypic.of_subsingleton : ∀ (R : Type u_2) (M : Type u) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Subsingleton M],
  IsIsotypic R M
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A shorthand for `toConeFunctor.obj`  -/
CategoryTheory.Limits.Bicone.toCone : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → CategoryTheory.Limits.Bicone F → CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor F)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
/-- The functorial (distinguished) triangle attached to a spectral object in
a pretriangulated category.  -/
CategoryTheory.Triangulated.SpectralObject.ω₂ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [inst_6 : CategoryTheory.Pretriangulated C] →
                  CategoryTheory.Triangulated.SpectralObject C ι →
                    CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 2)
                      (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.represents_iff : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] {b : ι → M} [inst_4 : DecidableEq ι] {A : Matrix ι ι R} {f : Module.End R M},
  Matrix.Represents b A f ↔
    ∀ (x : ι → R), (Fintype.linearCombination R b) (A.mulVec x) = f ((Fintype.linearCombination R b) x)
-- Mathlib.Data.Finset.Update
Function.restrict_updateFinset_of_subset : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : DecidableEq ι] {s t : Finset ι} (hst : s ⊆ t) (x : (i : ι) → π i)
  (y : (i : ↥t) → π ↑i), s.restrict (Function.updateFinset x t y) = Finset.restrict₂ hst y
-- Init.Data.Option.Monadic
Option.elimM_map : ∀ {m : Type u_1 → Type u_2} {α β γ : Type u_1} [inst : Monad m] [LawfulMonad m] (x : m α) (f : α → Option β) (y : m γ)
  (z : β → m γ),
  Option.elimM (f <$> x) y z = do
    let __do_lift ← x
    (f __do_lift).elim y z
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun_iff : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {β : ι → Type u_7} (m : (x : ι) → MeasurableSpace (β x))
  (f : (x : ι) → Ω → β x) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndepFun f μ ↔
    ∀ (s : Finset ι) {f' : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f' i)) → μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.HasCokernels.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  autoParam (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasCokernel f)
      CategoryTheory.Limits.HasCokernels.has_colimit._autoParam →
    CategoryTheory.Limits.HasCokernels C
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- The index type of a `SmoothBumpCovering` of a compact manifold is finite.  -/
SmoothBumpCovering.fintype : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] →
                    [inst_5 : FiniteDimensional ℝ E] →
                      {s : Set M} → SmoothBumpCovering ι I M s → [CompactSpace M] → Fintype ι
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.map_exp_comap_re_atTop : Filter.map Complex.exp (Filter.comap Complex.re Filter.atTop) = Bornology.cobounded ℂ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.MultispanIndex.multispan.match_1.eq_2 : ∀ {J : CategoryTheory.Limits.MultispanShape}
  (motive : (x y : CategoryTheory.Limits.WalkingMultispan J) → (x ⟶ y) → Sort u_3) (b : J.L)
  (h_1 : (x : CategoryTheory.Limits.WalkingMultispan J) → motive x x (CategoryTheory.Limits.WalkingMultispan.Hom.id x))
  (h_2 :
    (b : J.L) →
      motive (CategoryTheory.Limits.WalkingMultispan.left b) (CategoryTheory.Limits.WalkingMultispan.right (J.fst b))
        (CategoryTheory.Limits.WalkingMultispan.Hom.fst b))
  (h_3 :
    (b : J.L) →
      motive (CategoryTheory.Limits.WalkingMultispan.left b) (CategoryTheory.Limits.WalkingMultispan.right (J.snd b))
        (CategoryTheory.Limits.WalkingMultispan.Hom.snd b)),
  (match CategoryTheory.Limits.WalkingMultispan.left b, CategoryTheory.Limits.WalkingMultispan.right (J.fst b),
      CategoryTheory.Limits.WalkingMultispan.Hom.fst b with
    | x, .(x), CategoryTheory.Limits.WalkingMultispan.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingMultispan.left b), .(CategoryTheory.Limits.WalkingMultispan.right (J.fst b)),
      CategoryTheory.Limits.WalkingMultispan.Hom.fst b => h_2 b
    | .(CategoryTheory.Limits.WalkingMultispan.left b), .(CategoryTheory.Limits.WalkingMultispan.right (J.snd b)),
      CategoryTheory.Limits.WalkingMultispan.Hom.snd b => h_3 b) =
    h_2 b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (w : ℕ) (input : aig.RefVec w)
  (newWidth curr : ℕ) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s).vec.get idx ⋯ =
    (s.get idx hidx).cast ⋯
-- Mathlib.Data.Vector.Basic
/-- Mapping under `id` does not change a vector.  -/
List.Vector.map_id : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n), List.Vector.map id v = v
-- Std.Data.TreeMap.Iterator
Std.TreeMap.valuesIter_toList : ∀ {α β : Type u_1} {cmp : α → α → Ordering} (m : Std.TreeMap α β cmp), m.valuesIter.toList = m.values
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
CochainComplex.Lifting.π_f_cochain₁_v_ι_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct) {Q : CochainComplex C ℤ} {π : B ⟶ Q} {hπ : CategoryTheory.CategoryStruct.comp i π = 0}
  (hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ)) {K : CochainComplex C ℤ}
  {ι : K ⟶ X} {hι : CategoryTheory.CategoryStruct.comp ι p = 0}
  (hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι)) (n m : ℤ) (hnm : n + 1 = m),
  CategoryTheory.CategoryStruct.comp (π.f n)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.Lifting.cochain₁ sq hsq hQ hK).v n m hnm) (ι.f m)) =
    (↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm
-- Mathlib.Tactic.Explode.Pretty
/-- Render a particular row of the Fitch table.  -/
Mathlib.Explode.rowToMessageData : List Lean.MessageData →
  List Lean.MessageData → List Lean.MessageData → List Mathlib.Explode.Entry → Lean.MetaM Lean.MessageData
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverEolAtErrPos : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedDoElemContKind : Inhabited Lean.Elab.Do.DoElemContKind
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.mem_carrier_iff : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (A : Projectivization.Subspace K V) (x : Projectivization K V), x ∈ A.carrier ↔ x ∈ A
-- Init.Data.List.Basic
List.reverseAux_nil : ∀ {α : Type u_1} {r : List α}, [].reverseAux r = r
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.map.eq_5 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (x : ℕ → C) (x_1 : (n : ℕ) → x n ⟶ x (n + 1)) (k l : ℕ),
  CategoryTheory.Functor.OfSequence.map x_1 k.succ l.succ = fun x_2 =>
    CategoryTheory.Functor.OfSequence.map (fun n => x_1 (n + 1)) k l ⋯
-- Mathlib.CategoryTheory.Subobject.FactorThru
/-- Given two subobjects `P Q : Subobject Y`, if `P` factors through `Q`, then there is a morphism of
subobjects from `P` to `Q`.
 -/
CategoryTheory.Subobject.homOfFactors : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y : C} → {P Q : CategoryTheory.Subobject Y} → Q.Factors P.arrow → (P ⟶ Q)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceOfNat : Lean.Meta.Simp.DSimproc
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (n : ℤ) (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast n))
  (h_3 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (x : Lean.Grind.CommRing.Expr) → motive x),
  (match Lean.Grind.CommRing.Expr.intCast n with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.intCast n => h_2 n
    | Lean.Grind.CommRing.Expr.natCast n => h_3 n
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | x => h_5 x) =
    h_2 n
-- Mathlib.Data.Finset.Card
Finset.card_filter_add_card_filter_not : ∀ {α : Type u_1} {s : Finset α} (p : α → Prop) [inst : DecidablePred p] [inst_1 : (x : α) → Decidable ¬p x],
  (Finset.filter p s).card + {a ∈ s | ¬p a}.card = s.card
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.a : ℕ
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal : {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → NatCast (ModularForm Γ 0)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.submodule_span_prod_dp_eq_top : ∀ {R : Type u_4} {M : Type u_5} {ι : Type u_6} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M},
  Submodule.span R (Set.range v) = ⊤ →
    Submodule.span R (Set.range fun n => n.prod fun i k => DividedPowerAlgebra.dp R k (v i)) = ⊤
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- Subtraction `y ↦ x - y` as an `IsometryEquiv`.  -/
IsometryEquiv.subLeft : {G : Type v} →
  [inst : AddGroup G] → [inst_1 : PseudoEMetricSpace G] → [IsIsometricVAdd G G] → [IsIsometricVAdd Gᵃᵒᵖ G] → G → G ≃ᵢ G
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.sort.loop.match_1.eq_1 : ∀ (motive : List ℕ → List ℕ → Sort u_1) (acc : List ℕ) (h_1 : (acc : List ℕ) → motive acc [])
  (h_2 : (acc : List ℕ) → (x : ℕ) → (xs : List ℕ) → motive acc (x :: xs)),
  (match acc, [] with
    | acc, [] => h_1 acc
    | acc, x :: xs => h_2 acc x xs) =
    h_1 acc
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Eta-expanded form of `TendstoLocallyUniformly.div₀` -/
TendstoLocallyUniformly.fun_div₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X]
  {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l →
      Continuous f →
        Continuous g →
          (∀ (x : X), g x ≠ 0) → TendstoLocallyUniformly (fun i i_1 => F i i_1 / G i i_1) (fun i => f i / g i) l
-- Mathlib.Combinatorics.Digraph.Orientation
Digraph.toSimpleGraphInclusive_top : ∀ {V : Type u_1}, ⊤.toSimpleGraphInclusive = ⊤
-- Mathlib.Combinatorics.Graph.Maps
Graph.Adj.map : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {u v : α} (f : α → α'),
  G.Adj u v → (Graph.map f G).Adj (f u) (f v)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstKey.mk : Lean.Name → Lean.Environment.RealizeConstKey✝
-- Mathlib.Algebra.Algebra.Operations
Submodule.pow_subset_pow : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A) {n : ℕ}, ↑M ^ n ⊆ ↑(M ^ n)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.isClosed_singleton_closedPoint : ∀ (R : Type u) [inst : CommSemiring R] [inst_1 : IsLocalRing R], IsClosed {IsLocalRing.closedPoint R}
-- Init.Data.Array.Lemmas
/-- Variant of `all_bne` with `!=` reversed.  -/
Array.all_bne' : ∀ {α : Type u_1} {a : α} [inst : BEq α] [PartialEquivBEq α] {xs : Array α}, (xs.all fun x => x != a) = !xs.contains a
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.toAlgHom_toNatAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S),
  ↑f.toNatAlgEquiv = (↑f).toNatAlgHom
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.apply_symm_apply : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (e : A ≃⋆+* B) (x : B), e (e.symm x) = x
-- Mathlib.Logic.UnivLE
Small.trans_univLE : ∀ (α : Type w) [hα : Small.{u, w} α] [h : UnivLE.{u, v}], Small.{v, w} α
-- Std.Tactic.BVDecide.Syntax
/-- This tactic works just like `bv_decide` but skips calling a SAT solver by using a proof that is
already stored on disk. It is called with the name of an LRAT file in the same directory as the
current Lean file:
```
bv_check "proof.lrat"
```
 -/
Lean.Parser.Tactic.bvCheck : Lean.ParserDescr
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.number.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.number = 1
-- Init.Data.Order.MinMaxOn
/-- Returns either `x` or `y`, the one with the greater value under `f`.

If `f y ≤ f x`, it returns `x`, and otherwise returns `y`.
 -/
maxOn : {β : Type u_1} → {α : Sort u_2} → [i : LE β] → [DecidableLE β] → (α → β) → α → α → α
-- Mathlib.Analysis.Calculus.AddTorsor.AffineMap
/-- A continuous affine map between normed vector spaces is smooth.  -/
ContinuousAffineMap.contDiff : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : NormedAddCommGroup W] [inst_4 : NormedSpace 𝕜 W] {n : WithTop ℕ∞}
  (f : V →ᴬ[𝕜] W), ContDiff 𝕜 n ⇑f
-- Init.Data.SInt.Lemmas
Int8.toInt64_div_of_ne_left : ∀ (a b : Int8), a ≠ Int8.minValue → (a / b).toInt64 = a.toInt64 / b.toInt64
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.vadd_Lp_sub : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f g : ↥(MeasureTheory.Lp E p μ)), c +ᵥ f - g = (c +ᵥ f) - (c +ᵥ g)
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
/-- The group homomorphism `FreeAbelianGroup X →+ (X →₀ ℤ)`.  -/
FreeAbelianGroup.toFinsupp : {X : Type u_1} → FreeAbelianGroup X →+ X →₀ ℤ
-- Mathlib.Algebra.Homology.Homotopy
CategoryTheory.Functor.mapHomotopy_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W]
  [inst_3 : CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [inst_4 : F.Additive] {f g : C ⟶ D}
  (h : Homotopy f g) (i j : ι), (F.mapHomotopy h).hom i j = F.map (h.hom i j)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instReprExpr : Repr Lean.Grind.Linarith.Expr
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.ghDist.congr_simp : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : Nonempty X] [inst_2 : CompactSpace X]
  [inst_3 : MetricSpace Y] [inst_4 : Nonempty Y] [inst_5 : CompactSpace Y],
  GromovHausdorff.ghDist X Y = GromovHausdorff.ghDist X Y
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.d_fstX_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) {Z : C} (h : F.X k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ j k hjk) h) =
    CategoryTheory.CategoryStruct.comp
      (-CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij) (F.d j k)) h
-- Mathlib.Data.Prod.TProd
List.TProd.ext : ∀ {ι : Type u} {α : ι → Type v} [inst : DecidableEq ι] {l : List ι},
  l.Nodup → ∀ {v w : List.TProd α l}, (∀ (i : ι) (hi : i ∈ l), v.elim hi = w.elim hi) → v = w
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_dite_right : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} (P : Prop)
  [inst_2 : Decidable P] (x : β → ¬P → α),
  (∏'[L] (b : β), if h : P then 1 else x b h) = if h : P then 1 else ∏'[L] (b : β), x b h
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_left_injective : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (x : (i : Fin n) → α i.succ), Function.Injective fun x₀ => Fin.cons x₀ x