mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
cfcₙL_integral : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NonUnitalNormedRing A] [inst_3 : StarRing A] [inst_4 : NormedSpace 𝕜 A]
  [inst_5 : IsScalarTower 𝕜 A A] [inst_6 : SMulCommClass 𝕜 A A] [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p]
  [inst_8 : CompleteSpace A] [inst_9 : NormedSpace ℝ A] (a : A) (f : X → ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜),
  MeasureTheory.Integrable f μ →
    ∀ (ha : autoParam (p a) cfcₙL_integral._auto_1), ∫ (x : X), (cfcₙL ha) (f x) ∂μ = (cfcₙL ha) (∫ (x : X), f x ∂μ)
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
_private.Mathlib.CategoryTheory.Sites.Point.Skyscraper.0.CategoryTheory.GrothendieckTopology.Point.isSheaf_skyscraperPresheaf_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ : J.Point}
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A] {M : A}
  {X : C},
  ∀ R ∈ J X,
    ∀ (s : CategoryTheory.Limits.Cone (R.arrows.diagram.op.comp (Φ.skyscraperPresheaf M))),
      ∃ l,
        ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj.left),
          CategoryTheory.CategoryStruct.comp l
              (CategoryTheory.Limits.Pi.π (fun x => M)
                ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map j.obj.hom)) y)) =
            CategoryTheory.CategoryStruct.comp (s.π.app (Opposite.op j)) (CategoryTheory.Limits.Pi.π (fun t => M) y)
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
/-- The submonoid functor defined by the image along a morphism of functors of monoids.  -/
CategoryTheory.SubmonoidFunctor.image : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M M' : CategoryTheory.Functor C MonCat} →
      (M ⟶ M') → CategoryTheory.SubmonoidFunctor M → CategoryTheory.SubmonoidFunctor M'
-- Init.Data.Order.Classes
Std.IsLinearOrder.le_total : ∀ {α : Type u} {inst : LE α} [self : Std.IsLinearOrder α] (a b : α), a ≤ b ∨ b ≤ a
-- Mathlib.Order.Lattice
/-- A type endowed with `⊔` is a `SemilatticeSup`, if it admits an injective map that
preserves `⊔` to a `SemilatticeSup`.
See note [reducible non-instances].  -/
Function.Injective.semilatticeSup : {α : Type u} →
  {β : Type v} →
    [inst : Max α] →
      [inst_1 : LE α] →
        [inst_2 : LT α] →
          [inst_3 : SemilatticeSup β] →
            (f : α → β) →
              Function.Injective f →
                (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                  (∀ {x y : α}, f x < f y ↔ x < y) → (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) → SemilatticeSup α
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.minKey? (Std.Internal.List.insertEntryIfNew k v l) =
      some ((Std.Internal.List.minKey? l).elim k fun k' => if compare k k' = Ordering.lt then k else k')
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app_assoc : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X) {Z : ↑Y} (h : G.toFunctor.obj A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.inv.toNatTrans.app A)
      (CategoryTheory.CategoryStruct.comp (e.hom.toNatTrans.app A) h) =
    h
-- Init.Grind.Module.Basic
/-- Scalar multiplication by natural numbers is consistent with scalar multiplication by integers.  -/
Lean.Grind.IntModule.zsmul_natCast_eq_nsmul : ∀ {M : Type u} [self : Lean.Grind.IntModule M] (n : ℕ) (a : M), ↑n • a = n • a
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1'_eq_setToL1SCLM : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : NormedRing 𝕜] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] [inst_7 : IsBoundedSMul 𝕜 E]
  [inst_8 : IsBoundedSMul 𝕜 F] [inst_9 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ}
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (f : ↥(α →₁ₛ[μ] E)),
  (MeasureTheory.L1.setToL1' 𝕜 hT h_smul) ↑f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.getModify_eq : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  (f : σ → σ),
  getModify f = do
    let s ← get
    set (f s)
    pure s
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`,
there is the natural `R`-algebra homomorphism
`A ⊗[R] B →ₐ[R] S` induced by multiplication in `S`.  -/
Subalgebra.mulMap : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → (A B : Subalgebra R S) → TensorProduct R ↥A ↥B →ₐ[R] S
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.termM : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- `limitIsoFlipCompLim` is natural with respect to diagrams.  -/
CategoryTheory.Limits.limIsoFlipCompWhiskerLim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] →
              CategoryTheory.Limits.lim ≅
                (CategoryTheory.flipFunctor J K C).comp
                  ((CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj
                    CategoryTheory.Limits.lim)
-- Lean.CoreM
Lean.Core.instInhabitedCache : Inhabited Lean.Core.Cache
-- Lean.Parser.Syntax
Lean.Parser.Command.elab_rules : Lean.Parser.Parser
-- Mathlib.Topology.Category.Compactum
/-- Given any compact Hausdorff space, we construct a Compactum.  -/
Compactum.ofTopologicalSpace : (X : Type u_1) → [inst : TopologicalSpace X] → [CompactSpace X] → [T2Space X] → Compactum
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.coker.condition_assoc : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasCokernels C] {Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C}
  (h : CategoryTheory.Limits.coker C ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow.leftToRight
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coker.π C) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x y : MonoidAlgebra R M}, x.coeff = y.coeff ↔ x = y
-- Std.Http.Protocol.H1
/-- Processes chunked transfer-encoding output (HTTP/1.1).
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processChunkedBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntThms : Inhabited Lean.Meta.Grind.Arith.Cutsat.ToIntThms
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Inversion operation for monomials.  -/
Tactic.ComputeAsymptotics.Monomial.inv : Tactic.ComputeAsymptotics.Monomial → Tactic.ComputeAsymptotics.Monomial
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.mapAlgHom'_residue : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsLocalRing S]
  [inst_3 : CommRing T] [inst_4 : IsLocalRing T] [inst_5 : Algebra R S] [inst_6 : Algebra R T]
  [inst_7 : IsLocalHom (algebraMap R S)] [inst_8 : IsLocalHom (algebraMap R T)] [inst_9 : IsLocalRing R] (e : S →ₐ[R] T)
  [inst_10 : IsLocalHom e] (x : S),
  (IsLocalRing.ResidueField.mapAlgHom' e) ((IsLocalRing.residue S) x) = (IsLocalRing.residue T) (e x)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posSemidef_conjTranspose_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {M : Matrix n n R},
  M.conjTranspose.PosSemidef ↔ M.PosSemidef
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- Formats a `CompSource` for printing.  -/
Mathlib.Tactic.Linarith.CompSource.toString : Mathlib.Tactic.Linarith.CompSource → String
-- Std.Internal.Do.Triple.SpecLemmas
/-- An invariant for a `repeatM` loop, given as a predicate over the `α ⊕ β` cursor:
`.inl a` is the `continue` case at `a`; `.inr b` is the `break` case with result `b`.
 -/
Std.Internal.Do.RepeatInvariant : Type u → Type u → Type u → Type u
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS.eq_3 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (v : Lean.Grind.CommRing.Var),
  Lean.Grind.CommRing.Expr.denoteS ctx (Lean.Grind.CommRing.Expr.var v) = Lean.Grind.CommRing.Var.denote ctx v
-- Mathlib.Algebra.Order.AddGroupWithTop
add_left_inj_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] {a b c : α}, a ≠ ⊤ → (b + a = c + a ↔ b = c)
-- Mathlib.GroupTheory.QuotientGroup.Basic
AddMonoidHom.domRestrictHomKerEquiv.eq_1 : ∀ {G : Type u} [inst : AddGroup G] (A : Type u_1) [inst_1 : AddCommGroup A] (H : AddSubgroup G) [inst_2 : H.Normal],
  AddMonoidHom.domRestrictHomKerEquiv A H =
    {
      toFun := fun x =>
        match x with
        | ⟨f, hf⟩ => QuotientAddGroup.lift H f ⋯,
      invFun := fun f => ⟨f.comp (QuotientAddGroup.mk' H), ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Constructions
Filter.Tendsto.matrixVecCons : ∀ {Y : Type v} {Z : Type u_1} [inst : TopologicalSpace Z] {n : ℕ} {f : Y → Z} {g : Y → Fin n → Z} {l : Filter Y} {x : Z}
  {y : Fin n → Z},
  Filter.Tendsto f l (nhds x) →
    Filter.Tendsto g l (nhds y) → Filter.Tendsto (fun a => Matrix.vecCons (f a) (g a)) l (nhds (Matrix.vecCons x y))
-- Mathlib.NumberTheory.Height.Basic
/-- The product formula. The archimedean absolute values are taken with their multiplicity.  -/
Height.AdmissibleAbsValues.product_formula : ∀ {K : Type u_1} {inst : Field K} [self : Height.AdmissibleAbsValues K] {x : K},
  x ≠ 0 →
    (Multiset.map (fun x_2 => x_2 x) Height.AdmissibleAbsValues.archAbsVal).prod *
        ∏ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), ↑v x =
      1
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.mem_closedBallAddSubgroup_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M}
  {c : FiniteArchimedeanClass M}, a ∈ c.closedBallAddSubgroup ↔ ∀ (h : a ≠ 0), c ≤ FiniteArchimedeanClass.mk a h
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.withLpProdAssoc_symm_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) (γ : Type u_4) [hp : Fact (1 ≤ p)] [inst : Semiring 𝕜]
  [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β] [inst_4 : Module 𝕜 β]
  [inst_5 : SeminormedAddCommGroup γ] [inst_6 : Module 𝕜 γ] (a : WithLp p (α × WithLp p (β × γ))),
  (LinearIsometryEquiv.withLpProdAssoc p 𝕜 α β γ).symm a = WithLp.toLp p (WithLp.toLp p (a.fst, a.snd.fst), a.snd.snd)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.coe_floor_self : ∀ {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [inst_3 : FloorRing K] [inst_4 : Fintype ι] [inst_5 : Unique ι] (k : K),
  ↑(ZSpan.floor (Module.Basis.singleton ι K) k) = ↑⌊k⌋
-- Mathlib.Topology.Compactness.CompactSystem
/-- In a `T2Space` the set of compact sets is a compact system.  -/
isCompactSystem_isCompact : ∀ (α : Type u_2) [inst : TopologicalSpace α] [T2Space α], IsCompactSystem {s | IsCompact s}
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
/-- Given a monic polynomial `f : k[X]`,
`subProdXSubC f` is the polynomial $f - \prod_i (X - X_{f,i})$.  -/
AlgebraicClosure.subProdXSubC : {k : Type u} → [inst : Field k] → AlgebraicClosure.Monics k → Polynomial (MvPolynomial (AlgebraicClosure.Vars k) k)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hf : AlgebraicGeometry.UniversallyOpen f],
  AlgebraicGeometry.UniversallyOpen (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.differentiable_sin : Differentiable ℂ Complex.sin
-- Mathlib.Algebra.Group.Defs
Group.toCancelMonoid.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  Group.toCancelMonoid = { toMonoid := inst.toMonoid, toIsLeftCancelMul := ⋯, toIsRightCancelMul := ⋯ }
-- Mathlib.Control.Functor.Multivariate
_private.Mathlib.Control.Functor.Multivariate.0.MvFunctor.f : {β : Type u} →
  (pp : β → Prop) →
    (n : ℕ) →
      (α : TypeVec.{u} n) →
        TypeVec.Arrow (fun i => { p_1 // TypeVec.ofRepeat (α.PredLast' pp i p_1) }) fun i =>
          { p_1 // α.PredLast pp p_1 }
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero,
and the `i`th coefficient is `0` for all `i < n`.  -/
PowerSeries.order_eq_nat : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} {n : ℕ},
  φ.order = ↑n ↔ (PowerSeries.coeff n) φ ≠ 0 ∧ ∀ i < n, (PowerSeries.coeff i) φ = 0
-- Mathlib.Order.KrullDimension
Order.one_lt_height_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, 1 < Order.height x ↔ ∃ y, ∃ z < y, y < x
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.toMeasurable_def : ∀ {α : Type u_6} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
  MeasureTheory.toMeasurable μ s =
    if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s then h.choose
    else
      if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose
      else ⋯.choose
-- Mathlib.Analysis.Convex.Strict.Extreme
/-- In a nontrivial normed space, the extreme points of the closed ball is contained in
the sphere.  -/
extremePoints_closedBall_subset_sphere : ∀ {A : Type u_1} [inst : NormedAddCommGroup A] [inst_1 : NormedSpace ℝ A] [Nontrivial A] {x : A} {r : ℝ},
  Set.extremePoints ℝ (Metric.closedBall x r) ⊆ Metric.sphere x r
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.comp_hom_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {R S T : CategoryTheory.Grp C} (f : R ⟶ S) (g : S ⟶ T) {Z : C} (h : T.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom.hom h =
    CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp g.hom.hom h)
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.congr : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f₁ f₂ : α → β}
  {n : ℕ}, IsMulFreimanHom n A B f₁ → Set.EqOn f₁ f₂ A → IsMulFreimanHom n A B f₂
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.inv_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {G H : CategoryTheory.Functor C D} (α : G ⟶ H)
  (F : CategoryTheory.Functor D E) [inst_3 : CategoryTheory.IsIso α],
  CategoryTheory.inv (CategoryTheory.Functor.whiskerRight α F) =
    CategoryTheory.Functor.whiskerRight (CategoryTheory.inv α) F
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If there is any isomorphism `⊥ ≅ G.obj ⊥`, then `G` preserves initial objects.  -/
CategoryTheory.Limits.preservesInitial_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasInitial C]
  [inst_3 : CategoryTheory.Limits.HasInitial D] (f : ⊥_ D ≅ G.obj (⊥_ C)),
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G
-- Init.Data.Range.Polymorphic.Basic
Std.Roi.mem_iff : ∀ {α : Type u} {r : Std.Roi α} {a : α} [inst : LT α], a ∈ r ↔ r.lower < a
-- Mathlib.Data.Int.GCD
_private.Mathlib.Data.Int.GCD.0.Nat.xgcdAux.match_1.eq_2 : ∀ (motive : (n : ℕ) → ((m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → Sort u_1) (k : ℕ)
  (ih : (m : ℕ) → m < k.succ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
  (h_1 : (ih : (m : ℕ) → m < 0 → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive 0 ih)
  (h_2 : (k : ℕ) → (ih : (m : ℕ) → m < k.succ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive k.succ ih),
  (match k.succ, ih with
    | 0, ih => h_1 ih
    | k.succ, ih => h_2 k ih) =
    h_2 k ih
-- Mathlib.RingTheory.DedekindDomain.Basic
IsDedekindRing.toDimensionLEOne : ∀ {A : Type u_2} {inst : CommRing A} [self : IsDedekindRing A], Ring.DimensionLEOne A
-- Lean.Meta.Tactic.Grind.MatchCond
/-- Returns `some (α?, lhs, rhs)` if `e` is of the form
- `Eq _ lhs rhs` (`?α := none`), or
- `HEq α lhs _ rhs` (`α? := some α`)
 -/
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.isEqHEq? : Lean.Expr → Option (Option Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.Order.Round
round_ofNat : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (n : ℕ)
  [inst_4 : n.AtLeastTwo], round (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- A constant sequence of functions is uniformly integrable in the probability sense.  -/
MeasureTheory.uniformIntegrable_const : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {g : α → β},
  1 ≤ p → p ≠ ⊤ → MeasureTheory.MemLp g p μ → MeasureTheory.UniformIntegrable (fun x => g) p μ
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.Hom.toImage_app_injective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : ↑Y.affineOpens) [AlgebraicGeometry.QuasiCompact f],
  Function.Injective
    ⇑(CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Scheme.Hom.toImage f)
          ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.imageι f).base).obj ↑U)))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_alter_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  k ∈ (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl ↔
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true
-- Mathlib.Topology.EMetricSpace.PairReduction
/-- A structure for carrying the data of `logSizeBallSeq`  -/
PairReduction.logSizeBallStruct : Type u_2 → Type u_2
-- Mathlib.Order.SuccPred.Archimedean
Pred.rec_iff : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [IsPredArchimedean α] {p : α → Prop},
  (∀ (a : α), p a ↔ p (Order.pred a)) → ∀ {a b : α}, b ≤ a → (p a ↔ p b)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.toS : {X : SSet} → X.N → X.S
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterWithPostcondition.match_1.splitter : {β : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → Std.Iterators.PostconditionT n (ULift.{u_1, 0} Bool)} →
      (out : β) →
        (motive : Subtype (f out).Property → Sort u_3) →
          (__do_lift : Subtype (f out).Property) →
            ((h' : (f out).Property { down := false }) → motive ⟨{ down := false }, h'⟩) →
              ((h' : (f out).Property { down := true }) → motive ⟨{ down := true }, h'⟩) → motive __do_lift
-- Mathlib.Algebra.Field.Basic
one_sub_div : ∀ {K : Type u_1} [inst : DivisionRing K] {a b : K}, b ≠ 0 → 1 - a / b = (b - a) / b
-- Init.Data.List.MinMaxIdx
List.apply_maxOn_lt_apply_getElem_of_lt_maxIdxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {k : ℕ} (hk : k < List.maxIdxOn f xs h),
  f xs[k] < f (List.maxOn f xs h)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.zero_comp : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R₁ M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂), 0 ∘ₛₗ f = 0
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.unit_app_commShiftIso_hom_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C a).obj (G.obj (F.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (F.comp G) a).hom.app X) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map (adj.unit.app X)) h
-- Init.Data.Range.Polymorphic.PRange
/-- `a<...<b` is the range of elements greater than `a` and less than `b`.
See also `Std.Roo`.
 -/
Std.«term_<...<_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.π₂_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  CategoryTheory.Pretriangulated.Triangle.π₂.map f = f.hom₂
-- Std.Do.WP.SimpLemmas
Std.Do.WP.liftWith_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ α : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (f : ({β : Type u} → StateT σ m β → m (β × σ)) → m α),
  (Std.Do.wp (MonadControl.liftWith f)).apply Q = fun s =>
    (Std.Do.wp (f fun {β} x => x.run s)).apply (fun a => Q.1 a s, Q.2)
-- Mathlib.Algebra.MvPolynomial.Basic
/-- See note [partially-applied ext lemmas].

We set the priority higher than that of `AddMonoidAlgebra.ringHom_ext'`.  -/
MvPolynomial.ringHom_ext' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A]
  {f g : MvPolynomial σ R →+* A},
  f.comp MvPolynomial.C = g.comp MvPolynomial.C → (∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) → f = g
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List α} {k : α}, (t.insertManyIfNewUnit l).contains k = (t.contains k || l.contains k)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraFunctorOfMonadHomEq.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} {f g : T₁ ⟶ T₂}
  (h : f = g), CategoryTheory.Monad.algebraFunctorOfMonadHomEq h = CategoryTheory.Monad.algebraFunctorOfMonadHomEq h