mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.H.map_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {F G : CategoryTheory.Sheaf J AddCommGrpCat}
  (f : F ⟶ G) {n : ℕ} (x : F.H n),
  (CategoryTheory.Sheaf.H.map f n) x = CategoryTheory.Abelian.Ext.comp x (CategoryTheory.Abelian.Ext.mk₀ f) ⋯
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.copy_sliceTo_eq : ∀ {t₁ t₂ : String} {s : String.Slice} {p : s.Pos}, p.Splits t₁ t₂ → (s.sliceTo p).copy = t₁
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.Limits.hasPushout_ofHasPushoutsAgainst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.MorphismProperty C} {c c' c'' : C}
  {f : c ⟶ c'} {g : c ⟶ c''} [P.HasPushoutsAgainst P'], P f → P' g → CategoryTheory.Limits.HasPushout f g
-- Init.Grind.AC
Lean.Grind.AC.Seq.insert_k : Lean.Grind.AC.Var → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.instIsEmptyMEmpty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_4} {H : Type u_5} {M : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M]
  [inst_7 : IsManifold I k M] [inst_8 : IsEmpty M], IsEmpty (SingularManifold.empty X M I).M
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.of_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (m : M i),
  Monoid.CoprodI.of m = (conGen (Monoid.CoprodI.Rel M)).mk' (FreeMonoid.of ⟨i, m⟩)
-- Mathlib.Data.List.Chain
List.isChain_pair : ∀ {α : Type u_1} {R : α → α → Prop} {x y : α}, List.IsChain R [x, y] ↔ R x y
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.add_lt_aleph0_iff : ∀ {a b : Cardinal.{u_1}}, a + b < Cardinal.aleph0 ↔ a < Cardinal.aleph0 ∧ b < Cardinal.aleph0
-- Lean.Server.Requests
Lean.Server.RequestError.mk.injEq : ∀ (code : Lean.JsonRpc.ErrorCode) (message : String) (code_1 : Lean.JsonRpc.ErrorCode) (message_1 : String),
  ({ code := code, message := message } = { code := code_1, message := message_1 }) =
    (code = code_1 ∧ message = message_1)
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inr_desc_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W)
  (k : Y ⟶ W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Q : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inr Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (hP.desc h k w) Q) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight k Q
-- Mathlib.Data.Prod.Basic
Prod.instAsymmLex_mathlib : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Asymm r] [Std.Asymm s],
  Std.Asymm (Prod.Lex r s)
-- Mathlib.Geometry.Manifold.Instances.Real
EuclideanQuadrant.ext : ∀ {n : ℕ} (x y : EuclideanQuadrant n), ↑x = ↑y → x = y
-- Init.Data.UInt.Lemmas
USize.toUInt16_div : ∀ (a b : USize), a < 65536 → b < 65536 → (a / b).toUInt16 = a.toUInt16 / b.toUInt16
-- Mathlib.CategoryTheory.Sites.Pretopology
/-- If `J` is a precoverage that has isomorphisms and is stable under composition and
base change, it defines a pretopology.  -/
CategoryTheory.Precoverage.toPretopology : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      (J : CategoryTheory.Precoverage C) →
        [J.HasIsos] → [J.IsStableUnderBaseChange] → [J.IsStableUnderComposition] → CategoryTheory.Pretopology C
-- Mathlib.Algebra.BigOperators.Fin
/-- Equivalence between `Fin n → Fin m` and `Fin (m ^ n)`.  -/
finFunctionFinEquiv : {m n : ℕ} → (Fin n → Fin m) ≃ Fin (m ^ n)
-- Mathlib.Order.Category.DistLat
_private.Mathlib.Order.Category.DistLat.0.DistLat.Hom.mk : {X Y : DistLat} → LatticeHom ↑X ↑Y → X.Hom Y
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.update_one : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → One (f i)] [inst_1 : DecidableEq I] (i : I), Function.update 1 i 1 = 1
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
Lean.Meta.RefinedDiscrTree.PreDiscrTree.mk.injEq : ∀ {α : Type} (root : Std.HashMap Lean.Meta.RefinedDiscrTree.Key ℕ)
  (tries : Array (Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α)))
  (root_1 : Std.HashMap Lean.Meta.RefinedDiscrTree.Key ℕ)
  (tries_1 : Array (Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α))),
  ({ root := root, tries := tries } = { root := root_1, tries := tries_1 }) = (root = root_1 ∧ tries = tries_1)
-- Mathlib.Topology.ContinuousMap.Algebra
continuousAddSubmonoid.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddZeroClass β]
  [inst_3 : ContinuousAdd β],
  continuousAddSubmonoid α β = { carrier := {f | Continuous f}, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y)
  (i : Fin (1 + 1)),
  (G.mapComposableArrowsObjMk₁Iso f).hom.app i =
    match i with
    | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj X)
    | ⟨1, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Y)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The intersection of two faces of two cones is a face of the intersection of the cones.  -/
PointedCone.IsFaceOf.inf : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C₁ C₂ F₁ F₂ : PointedCone R M},
  F₁.IsFaceOf C₁ → F₂.IsFaceOf C₂ → (F₁ ⊓ F₂).IsFaceOf (C₁ ⊓ C₂)
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.instInhabitedGCongrKey.default : Mathlib.Tactic.GCongr.GCongrKey
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_sups : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : DecidableEq α] {s t : Finset α} {a : α} [inst_2 : DecidableLE α]
  [inst_3 : BoundedOrder α],
  a ∈ upperClosure ↑s → a ∈ upperClosure ↑t → (s ⊻ t).truncatedInf a = s.truncatedInf a ⊔ t.truncatedInf a
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.braiding_hom_hom : ∀ (X Y : SFinKer), (β_ X Y).hom.hom = ProbabilityTheory.Kernel.swap X.carrier Y.carrier
-- Mathlib.Data.Real.Embedding
Archimedean.mkRat_mem_ratLt : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M] {num : ℤ}
  {den : ℕ}, den ≠ 0 → ∀ {x : M}, mkRat num den ∈ Archimedean.ratLt x ↔ num • 1 < den • x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_two_pi_sub : ∀ (x : ℝ), Real.cos (2 * Real.pi - x) = Real.cos x
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_intCast : ∀ (x : NNReal) (n : ℤ), x ^ ↑n = x ^ n
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.order_ineq : ∀ (p' : ℕ), lucasLehmerResidue (p' + 2) = 0 → 2 ^ (p' + 2) < ↑(LucasLehmer.q (p' + 2)) ^ 2
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coroot'_reflection : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {i j : ι} (y : M),
  (P.coroot' j) ((P.reflection i) y) = (P.coroot' ((P.reflectionPerm i) j)) y
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar.eq_1 : ∀ {Ω : Type u_1} {m₀ : MeasurableSpace Ω} (m : MeasurableSpace Ω) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.condVar m X μ = μ[(X - μ[X | m]) ^ 2 | m]
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- Variant with a weaker constraint, but on the prime upstairs instead.  -/
Ideal.inertiaDeg'_pos' : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [P.IsPrime] [Module.Finite R S] [P.LiesOver p], 0 < p.inertiaDeg' P
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- If `f` has temperate growth, then for any `N : ℕ` one can find `k` such that *all* iterated
derivatives of `f` of order `≤ N` are `O((1 + ‖x‖) ^ k)`.

Note that the `O` here is with respect to the `⊤` filter, meaning that the bound holds everywhere.
 -/
Function.HasTemperateGrowth.isBigO_uniform : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F},
  Function.HasTemperateGrowth f → ∀ (N : ℕ), ∃ k, ∀ n ≤ N, iteratedFDeriv ℝ n f =O[⊤] fun x => (1 + ‖x‖) ^ k
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundExceptTExceptPureOfLawfulMonad.match_5.splitter : {ε α : Type u_1} →
  {P : α → Prop} →
    (motive :
        (r : Except ε α) →
          (match r with
            | Except.ok a => P a
            | Except.error a => True) →
            Sort u_2) →
      (r : Except ε α) →
        (h :
            match r with
            | Except.ok a => P a
            | Except.error a => True) →
          ((a : α) →
              (hp :
                  match Except.ok a with
                  | Except.ok a => P a
                  | Except.error a => True) →
                motive (Except.ok a) hp) →
            ((e : ε) →
                (x :
                    match Except.error e with
                    | Except.ok a => P a
                    | Except.error a => True) →
                  motive (Except.error e) x) →
              motive r h
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.extend_eq : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤),
  (∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) →
    ∀ (n : ℕ), IsAdicComplete.StrictMono.extend ha f (a n) = f n
-- Init.Data.Slice.Array.Lemmas
Subarray.toArray_mkSlice_rci : ∀ {α : Type u_1} {xs : Subarray α} {lo : ℕ},
  Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) = (Std.Slice.toArray xs).extract lo
-- Mathlib.Computability.ContextFreeGrammar
/-- Rule that rewrites a single nonterminal to any string (a list of symbols).  -/
ContextFreeRule : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Mathlib.Data.Finsupp.Single
/-- If `α` has a unique term, then finitely supported functions `α →₀ M` are in bijection with `M`.
 -/
Finsupp.uniqueEquiv : {α : Type u_1} → {M : Type u_5} → [inst : Zero M] → α → [Subsingleton α] → (α →₀ M) ≃ M
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instAddGroup : {R : Type u_1} → [inst : AddGroup R] → AddGroup (ArithmeticFunction R)
-- Std.Sat.CNF.Dimacs
/-- This function turns `cnf` into a DIMACS `String`.

Note: This function will add `1` to all literal identifiers by default. This is because `0` is an
illegal identifier in the DIMACS format and we can avoid producing invalid DIMACs like this.
 -/
Std.Sat.CNF.dimacs : Std.Sat.CNF ℕ → String
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.α_hom_inv : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y Z : CategoryTheory.FreeMonoidalCategory C}, CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
/-- Noether's generalization of Hilbert's Theorem 90: given a finite extension of fields `L/K`, the
first group cohomology `H¹(Aut_K(L), Lˣ)` is trivial.  -/
groupCohomology.H1ofAutOnUnitsUnique : (K L : Type) →
  [inst : Field K] →
    [inst_1 : Field L] →
      [inst_2 : Algebra K L] → [FiniteDimensional K L] → Unique ↑(groupCohomology.H1 (Rep.ofAlgebraAutOnUnits K L))
-- Mathlib.Topology.ClopenBox
TopologicalSpace.Clopens.exists_prod_subset : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace Y]
  (W : TopologicalSpace.Clopens (X × Y)) {a : X × Y}, a ∈ W → ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.mapRange_smul : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] [inst_2 : (i : ι) → AddCommMonoid (β₂ i)]
  [inst_3 : (i : ι) → Module R (β₁ i)] [inst_4 : (i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i → β₂ i)
  (hf : ∀ (i : ι), f i 0 = 0) (r : R),
  (∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x) →
    ∀ (g : Π₀ (i : ι), β₁ i), DFinsupp.mapRange f hf (r • g) = r • DFinsupp.mapRange f hf g
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.Pos.skipWhile.match_1.eq_2 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (h_1 : (nextCurr : s.Pos) → motive (some nextCurr))
  (h_2 : Unit → motive none),
  (match none with
    | some nextCurr => h_1 nextCurr
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.Limits.pushoutIsoUnopPullback f g).hom =
    (CategoryTheory.Limits.pullback.fst f.op g.op).unop
-- Mathlib.Topology.Algebra.Group.Defs
IsTopologicalAddGroup.toContinuousNeg : ∀ {G : Type u} {inst : TopologicalSpace G} {inst_1 : AddGroup G} [self : IsTopologicalAddGroup G], ContinuousNeg G
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddGroup.ofAddDist.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : AddGroup E] [inst_2 : MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 0 x)
  (h₂ : ∀ (x y z : E), dist x y ≤ dist (z + x) (z + y)),
  NormedAddGroup.ofAddDist h₁ h₂ =
    { toNorm := (SeminormedAddGroup.ofAddDist h₁ h₂).toNorm,
      toAddGroup := (SeminormedAddGroup.ofAddDist h₁ h₂).toAddGroup,
      toPseudoMetricSpace := (SeminormedAddGroup.ofAddDist h₁ h₂).toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯,
      dist_eq := ⋯ }
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.map_addHaar_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {r : ℝ},
  r ≠ 0 → MeasureTheory.Measure.map (fun x => r • x) μ = ENNReal.ofReal |(r ^ Module.finrank ℝ E)⁻¹| • μ
-- Mathlib.Order.LiminfLimsup
Filter.limsup_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α] (u : β → α) (v : γ → β)
  (f : Filter γ), Filter.limsup (u ∘ v) f = Filter.limsup u (Filter.map v f)
-- Mathlib.Algebra.Group.Units.Defs
Units.val_eq_one : ∀ {α : Type u} [inst : Monoid α] {a : αˣ}, ↑a = 1 ↔ a = 1
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- An `R`-module `M` is faithfully flat iff it is flat and for all linear maps `f`, the map
`id ⊗ f = 0`, if and only if `f = 0`.  -/
Module.FaithfullyFlat.iff_zero_iff_rTensor_zero : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.FaithfullyFlat R M ↔
    Module.Flat R M ∧
      ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
        [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
-- Mathlib.Control.ULift
PLift.seq_up : ∀ {α : Sort u} {β : Sort v} (f : α → β) (x : α), ({ down := f }.seq fun x_1 => { down := x }) = { down := f x }
-- Std.Async.System
Std.Async.System.instDecidableEqCPUTimes : DecidableEq Std.Async.System.CPUTimes
-- Mathlib.Analysis.RCLike.Basic
AddChar.inv_apply_eq_conj : ∀ {K : Type u_1} [inst : RCLike K] {G : Type u_3} [Finite G] [inst_2 : AddLeftCancelMonoid G] (ψ : AddChar G K) (x : G),
  (ψ x)⁻¹ = (starRingEnd K) (ψ x)
-- Mathlib.Order.SuccPred.Basic
Order.Ico_succ_right_eq_insert_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  a ≤ b → ¬IsMax b → Set.Ico a (Order.succ b) = insert b (Set.Ico a b)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.IterM.step_drop.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : k.succ = 0 → motive 0) (h_2 : (k_1 : ℕ) → k.succ = k_1.succ → motive k_1.succ),
  (match h' : k.succ with
    | 0 => h_1 h'
    | k_1.succ => h_2 k_1 h') =
    h_2 k ⋯
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.trans_isBigOTVS : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G}, f =o[𝕜; l] g → g =O[𝕜; l] k → f =o[𝕜; l] k
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
SSet.Subcomplex.ofSimplexProd_eq_range : ∀ {X₁ X₂ : SSet} {p q : ℕ} (x₁ : X₁.obj (Opposite.op { len := p })) (x₂ : X₂.obj (Opposite.op { len := q })),
  (SSet.Subcomplex.ofSimplex x₁).prod (SSet.Subcomplex.ofSimplex x₂) =
    SSet.Subcomplex.range
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.yonedaEquiv.symm x₁) (SSet.yonedaEquiv.symm x₂))
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The cosine of the oriented angle between two nonzero vectors equals that of the unoriented
angle.  -/
Orientation.cos_oangle_eq_cos_angle : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  x ≠ 0 → y ≠ 0 → (o.oangle x y).cos = Real.cos (InnerProductGeometry.angle x y)
-- Init.Data.Fin.Lemmas
Fin.lt_def : ∀ {n : ℕ} {a b : Fin n}, a < b ↔ ↑a < ↑b
-- Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type v} [inst_1 : CategoryTheory.SmallCategory I]
  (F : CategoryTheory.Functor I (CategoryTheory.Functor Cᵒᵖ (Type v))) {J : Type v}
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
  (G :
    CategoryTheory.Functor J (CategoryTheory.CostructuredArrow CategoryTheory.yoneda (CategoryTheory.Limits.colimit F)))
  {K : Type v} [inst_4 : CategoryTheory.SmallCategory K]
  (H : CategoryTheory.Functor K (CategoryTheory.Over (CategoryTheory.Limits.colimit F))) [CategoryTheory.IsFiltered K]
  {c : CategoryTheory.Limits.Cocone H} (hc : CategoryTheory.Limits.IsColimit c)
  (T : CategoryTheory.Over (CategoryTheory.Limits.colimit F)) (hT : c.pt ≅ T),
  Nonempty
      (CategoryTheory.Limits.limit
        ((G.op.comp
              (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda (CategoryTheory.Limits.colimit F)).op).comp
          (CategoryTheory.yoneda.obj T))) →
    ∃ k,
      Nonempty
        (CategoryTheory.Limits.limit
          ((G.op.comp
                (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda
                    (CategoryTheory.Limits.colimit F)).op).comp
            (CategoryTheory.yoneda.obj (H.obj k))))
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.isPushout : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (self : HomotopicalAlgebra.AttachCells g f),
  CategoryTheory.IsPushout self.g₁ self.m f self.g₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square with `0 : 0 ⟶ 0` on the top and `𝟙 X` on the bottom is a pushout square.  -/
CategoryTheory.IsPushout.zero_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.IsPushout 0 0 0 (CategoryTheory.CategoryStruct.id X)
-- Init.Data.Int.DivMod.Lemmas
Int.le_of_mul_le_mul_right : ∀ {a b c : ℤ}, b * a ≤ c * a → 0 < a → b ≤ c
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, k ∈ Std.ExtTreeMap.map f t → k ∈ t
-- Init.Grind.Order
Lean.Grind.Order.le_eq_false_of_le_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b : α} {k₁ k₂ : ℤ},
  (k₂ + k₁).blt' 0 = true → a ≤ b + ↑k₁ → (b ≤ a + ↑k₂) = False
-- Mathlib.Order.Fin.Basic
Fin.compare_eq_compare_val : ∀ {n : ℕ} (a b : Fin n), compare a b = compare ↑a ↑b
-- Init.Data.Iterators.Basic
/-- Internal implementation detail of the iterator.  -/
Std.Iter.internalState : {α β : Type w} → Std.Iter β → α
-- Mathlib.Topology.MetricSpace.Contracting
/-- A posteriori estimates on the convergence of iterates to the fixed point.  -/
ContractingWith.aposteriori_dist_iterate_fixedPoint_le : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [inst_1 : Nonempty α]
  [inst_2 : CompleteSpace α] (x : α) (n : ℕ),
  dist (f^[n] x) (ContractingWith.fixedPoint f hf) ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - ↑K)
-- Mathlib.Analysis.InnerProductSpace.PiL2
stdOrthonormalBasis_def : ∀ (𝕜 : Type u_7) [inst : RCLike 𝕜] (E : Type u_8) [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E],
  stdOrthonormalBasis 𝕜 E =
    have b := Classical.choose ⋯;
    ⋯.mpr (b.reindex (Fintype.equivFinOfCardEq ⋯))
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.comap_ker : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {P : Type u_8} [inst_2 : AddZeroClass P]
  (g : N →+ P) (f : G →+ N), AddSubgroup.comap f g.ker = (g.comp f).ker
-- Mathlib.RingTheory.Perfection
Perfection.lift_apply_apply_coe : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [inst : CommSemiring R] [inst_1 : CharP R p]
  [inst_2 : PerfectRing R p] (S : Type u₂) [inst_3 : CommSemiring S] [inst_4 : CharP S p] (f : R →+* S) (r : R) (n : ℕ),
  ↑(((Perfection.lift p R S) f) r) n = f ((⇑↑(frobeniusEquiv R p).symm)^[n] r)
-- Mathlib.GroupTheory.SchurZassenhaus
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime`  -/
_private.Mathlib.GroupTheory.SchurZassenhaus.0.Subgroup.SchurZassenhausInduction.step0 : ∀ {G : Type u} [inst : Group G] {N : Subgroup G} [N.Normal],
  (Nat.card ↥N).Coprime N.index → (∀ (H : Subgroup G), ¬N.IsComplement' H) → N ≠ ⊥
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.inl_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl P.i = P.i₀
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α}
  (h₁ : (List.map Prod.fst l).contains k = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯) = true},
  Std.DTreeMap.Internal.Impl.Const.get (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k h' =
    Std.DTreeMap.Internal.Impl.Const.get t k ⋯