mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.Basic
nhdsGE_basis : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α),
  (nhdsWithin a (Set.Ici a)).HasBasis (fun u => a < u) fun u => Set.Ico a u
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_undef : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ}, ¬IntervalIntegrable f μ a b → ∫ (x : ℝ) in a..b, f x ∂μ = 0
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- For polynomial `f` and constant `a`, `Res(f, a) = a ^ m`.  -/
Polynomial.resultant_C_zero_left : ∀ {R : Type u_1} [inst : CommRing R] (g : Polynomial R) (r : R) (m : ℕ), (Polynomial.C r).resultant g 0 m = r ^ m
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.isSupClosedCompact_iff_wellFoundedGT : ∀ (α : Type u_2) [inst : CompleteLattice α], CompleteLattice.IsSupClosedCompact α ↔ WellFoundedGT α
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_pow : ∀ (z : Complex.UnitClosedDisc) (n : ℕ), ↑(z ^ n) = ↑z ^ n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdxD.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : ℕ) (x_2 : α),
  x.keyAtIdxD x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, fallback => fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback =>
      match compare n l.size with
      | Ordering.lt => l.keyAtIdxD n fallback
      | Ordering.eq => k
      | Ordering.gt => r.keyAtIdxD (n - l.size - 1) fallback
-- Mathlib.Algebra.Module.ULift
ULift.distribSMul : {R : Type u} → {M : Type v} → [inst : AddZeroClass M] → [DistribSMul R M] → DistribSMul (ULift.{u_1, u} R) M
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instIsScalarTower : ∀ {α : Type u_1} {R : Type u_3} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal] {R' : Type u_4}
  [inst_2 : SMul R' ENNReal] [inst_3 : IsScalarTower R' ENNReal ENNReal] [inst_4 : SMul R R']
  [IsScalarTower R R' ENNReal], IsScalarTower R R' (MeasureTheory.OuterMeasure α)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.equivSigma_symm_apply_left : ∀ (T : Type u) [inst : CategoryTheory.Category.{v, u} T] (x : (X : T) × (Y : T) × (X ⟶ Y)),
  ((CategoryTheory.Arrow.equivSigma T).symm x).left = x.fst
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.notMem_commonNeighbors_left : ∀ {V : Type u} (G : SimpleGraph V) (v w : V), v ∉ G.commonNeighbors v w
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_mul_left_closedBall : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ℝ),
  (fun x => a * x) ⁻¹' Metric.closedBall b r = Metric.closedBall (a⁻¹ * b) r
-- Init.Data.Vector.Lemmas
Vector.setIfInBounds_eq_of_size_le : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, n ≤ i → ∀ {a : α}, xs.setIfInBounds i a = xs
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.equivSubtype_apply_coe : ∀ (R : Type u_1) [inst : CommSemiring R] (I : PrimeSpectrum R), ↑((PrimeSpectrum.equivSubtype R) I) = I.asIdeal
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.forgetCreatesPullbackOfRight : {X Y Z : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      [H : AlgebraicGeometry.IsOpenImmersion f] →
        CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan g f)
          AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.xPrevIso_comp_dTo_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι}
  (r : c.Rel i j) {Z : V} (h : C.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (C.xPrevIso r).inv (CategoryTheory.CategoryStruct.comp (C.dTo j) h) =
    CategoryTheory.CategoryStruct.comp (C.d i j) h
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.Equiv.beq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap α (fun x => β) cmp} [inst : BEq β]
  [Std.TransCmp cmp] [ReflBEq β], m₁.Equiv m₂ → Std.DTreeMap.Const.beq m₁ m₂ = true
-- Init.System.IO
/-- Waits until any of the tasks in the list has finished, then returns its result.
 -/
IO.waitAny : {α : Type} → (tasks : List (Task α)) → autoParam (tasks.length > 0) IO.waitAny._auto_1 → BaseIO α
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.IsZeroAtImInfty.zero_at_infty_comp_ofComplex : ∀ {f : UpperHalfPlane → ℂ},
  UpperHalfPlane.IsZeroAtImInfty f → (Filter.comap Complex.im Filter.atTop).ZeroAtFilter (f ∘ ↑UpperHalfPlane.ofComplex)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.map_inf : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : Algebra R B]
  [inst_8 : StarRing B] [inst_9 : StarModule R B] (f : A →⋆ₐ[R] B),
  Function.Injective ⇑f →
    ∀ (S T : StarSubalgebra R A), StarSubalgebra.map f (S ⊓ T) = StarSubalgebra.map f S ⊓ StarSubalgebra.map f T
-- Lean.AuxRecursor
Lean.casesOnSuffix : String
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.newlineOrUnexpected : String → Lean.Parser.ParserFn
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- A version of `Set.indicator_sub` for `MeasureTheory.indicatorConstLp`  -/
MeasureTheory.indicatorConstLp_sub : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c c' : E},
  MeasureTheory.indicatorConstLp p hs hμs c - MeasureTheory.indicatorConstLp p hs hμs c' =
    MeasureTheory.indicatorConstLp p hs hμs (c - c')
-- Init.Data.Bool
Bool.eq_false_or_eq_true_self : ∀ (b : Bool), b = false ∨ b = true ↔ True
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.CandidateKind.termArg.sizeOf_spec : sizeOf Lean.Server.FileWorker.SignatureHelp.CandidateKind.termArg = 1
-- Init.Data.Int.DivMod.Lemmas
Int.lt_tdiv_add_one_mul_self : ∀ (a : ℤ) {b : ℤ}, 0 < b → a < (a.tdiv b + 1) * b
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Let `f` be a measurable function integrable on `a..b`. Choose `s ∈ {Iic a, Ici a, univ}`
and `t ∈ {Iic b, Ici b, univ}`. Suppose that `f` tends to `ca` and `cb` almost surely at the filters
`la` and `lb` from the table below. Then `fderivWithin ℝ (fun p ↦ ∫ x in p.1..p.2, f x) (s ×ˢ t)`
is equal to `(u, v) ↦ u • cb - v • ca`.

| `s`     | `la`     | `t`     | `lb`     |
| ------- | ----     | ---     | ----     |
| `Iic a` | `𝓝[≤] a` | `Iic b` | `𝓝[≤] b` |
| `Ici a` | `𝓝[>] a` | `Ici b` | `𝓝[>] b` |
| `{a}`   | `⊥`      | `{b}`   | `⊥`      |
| `univ`  | `𝓝 a`    | `univ`  | `𝓝 b`    |
 -/
intervalIntegral.fderivWithin_integral_of_tendsto_ae : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E}
  {la lb : Filter ℝ} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f la MeasureTheory.volume →
      StronglyMeasurableAtFilter f lb MeasureTheory.volume →
        ∀ {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) la]
          [intervalIntegral.FTCFilter b (nhdsWithin b t) lb],
          Filter.Tendsto f (la ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca) →
            Filter.Tendsto f (lb ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb) →
              autoParam (UniqueDiffWithinAt ℝ s a) intervalIntegral.fderivWithin_integral_of_tendsto_ae._auto_1 →
                autoParam (UniqueDiffWithinAt ℝ t b) intervalIntegral.fderivWithin_integral_of_tendsto_ae._auto_3 →
                  fderivWithin ℝ (fun p => ∫ (x : ℝ) in p.1..p.2, f x) (s ×ˢ t) (a, b) =
                    (ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca
-- Init.Data.Float.Model.Unpacked.Sign
Float.Model.UnpackedFloat.Sign.instMul : Mul Float.Model.UnpackedFloat.Sign
-- Std.Data.DTreeMap.Raw.Basic
/-- Dependent tree maps without a bundled well-formedness invariant, suitable for use in nested
inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt, prefer `DTreeMap`
over `DTreeMap.Raw`. Lemmas about the operations on `Std.DTreeMap.Raw` are available in the
module `Std.Data.DTreeMap.Raw.Lemmas`.

A tree map stores an assignment of keys to values. It depends on a comparator function that
defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval
of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function `cmp` should satisfy
certain laws that ensure a consistent ordering:

* If `a` is less than (or equal) to `b`, then `b` is greater than (or equal) to `a`
and vice versa (see the `OrientedCmp` typeclass).
* If `a` is less than or equal to `b` and `b` is, in turn, less than or equal to `c`, then `a`
is less than or equal to `c` (see the `TransCmp` typeclass).

Keys for which `cmp a b = Ordering.eq` are considered the same, i.e., there can be only one entry
with key either `a` or `b` in a tree map. Looking up either `a` or `b` always yields the same entry,
if any is present. The `get` operations of the _dependent_ tree map additionally require a
`LawfulEqCmp` instance to ensure that `cmp a b = .eq` always implies `a = b`, so that their
respective value types are equal.

To avoid expensive copies, users should make sure that the tree map is used linearly.

Internally, the tree maps are represented as size-bounded trees, a type of self-balancing binary
search tree with efficient order statistic lookups.
 -/
Std.DTreeMap.Raw : (α : Type u) → (α → Type v) → autoParam (α → α → Ordering) Std.DTreeMap.Raw._auto_1 → Type (max u v)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `Section` is a right inverse to `S.rightHom`  -/
GroupExtension.Section.rightInverse_rightHom : ∀ {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} (self : S.Section), Function.RightInverse self.toFun ⇑S.rightHom
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.measurableSet_blimsup : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : ℕ → Set α} {p : ℕ → Prop},
  (∀ (n : ℕ), p n → MeasurableSet (s n)) → MeasurableSet (Filter.blimsup s Filter.atTop p)
-- Mathlib.Algebra.Ring.Defs
ite_zero_mul_ite_zero : ∀ {α : Type u} [inst : MulZeroClass α] (P Q : Prop) [inst_1 : Decidable P] [inst_2 : Decidable Q] (a b : α),
  ((if P then a else 0) * if Q then b else 0) = if P ∧ Q then a * b else 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.self_le_maxKey!_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k}, (compare k (Std.Internal.List.maxKey! (Std.Internal.List.insertEntry k v l))).isLE = true
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
PowerBasis.equivAdjoinSimple.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (pb : PowerBasis K L),
  pb.equivAdjoinSimple = (IntermediateField.adjoin.powerBasis ⋯).equivOfMinpoly pb ⋯
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- A def to put an `One` instance on a type with a `Language.ring.Structure` instance.

To be used sparingly, usually only when defining a more useful definition like,
`[Language.ring.Structure K] -> [Theory.field.Model K] -> Field K`  -/
FirstOrder.Ring.oneOfRingStructure : (R : Type u_2) → [FirstOrder.Language.ring.Structure R] → One R
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompTriangle_obj₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  (CochainComplex.mappingConeCompTriangle f g).obj₃ = CochainComplex.mappingCone g
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_ofNatClamp_of_lt : ∀ {n : ℕ}, n < UInt32.size → (UInt32.ofNatClamp n).toUInt16 = UInt16.ofNat n
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.linearMap_ext_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f g : MvPolynomial σ R →ₗ[R] M}, f = g ↔ ∀ (s : σ →₀ ℕ), f ∘ₗ MvPolynomial.monomial s = g ∘ₗ MvPolynomial.monomial s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry!.eq_3 : ∀ {α : Type u} {β : Type v} [inst : Inhabited (α × β)] (size : ℕ) (k : α) (v : β)
  (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.maxEntry!
      (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) =
    Std.DTreeMap.Internal.Impl.Const.maxEntry! (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)
-- Mathlib.Order.Birkhoff
OrderIso.supIrredLowerSet_apply : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Finite α] (a : α), OrderIso.supIrredLowerSet a = ⟨LowerSet.Iic a, ⋯⟩
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.sub : {α : Type u_1} → [inst : Zero α] → [inst_1 : SemilatticeSup α] → [Sub α] → Sub { x // 0 ≤ x }
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_sup : ∀ {C : Type u_2} [inst : AddCommGroup C] {s t : AddSubgroup C} {x : C}, x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x
-- Lean.Meta.Sym.ExprPtr
Lean.Meta.Sym.hashPtrExpr.unsafe_impl_2 : Lean.Expr → UInt64
-- Std.Async.Select
Std.Async.Selectable.case.inj : ∀ {α β : Type} {selector : Std.Async.Selector β} {cont : β → Std.Async.Async α} {β_1 : Type}
  {selector_1 : Std.Async.Selector β_1} {cont_1 : β_1 → Std.Async.Async α},
  { β := β, selector := selector, cont := cont } = { β := β_1, selector := selector_1, cont := cont_1 } →
    β = β_1 ∧ selector ≍ selector_1 ∧ cont ≍ cont_1
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_one_mulSingle : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : One γ] (i : β)
  (c : γ), Sum.elim 1 (Pi.mulSingle i c) = Pi.mulSingle (Sum.inr i) c
-- Mathlib.Analysis.Normed.Module.Ray
SameRay.norm_smul_eq : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x y : E},
  SameRay ℝ x y → ‖x‖ • y = ‖y‖ • x
-- Mathlib.Algebra.Group.Ext
CommMonoid.ext_iff : ∀ {M : Type u_1} {m₁ m₂ : CommMonoid M}, m₁ = m₂ ↔ HMul.hMul = HMul.hMul
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_eq_singleton_append_iff : ∀ {xs : Array ℤ} {m n a : ℤ}, (m<...=n).toArray = #[a] ++ xs ↔ m + 1 = a ∧ m < n ∧ ((m + 1)<...=n).toArray = xs
-- Lean.PrettyPrinter.Delaborator.DeclWithSig
Lean.PrettyPrinter.Delaborator.declSigWithId.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Notation.Lemmas
ite_pos : ∀ {α : Type u_1} [inst : Zero α] {p : Prop} [inst_1 : Decidable p] {a b : α} [inst_2 : LT α],
  0 < a → 0 < b → 0 < if p then a else b
-- Lean.Parser.Extra
Lean.Parser.commandParser.formatter : optParam ℕ 0 → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.Hom.Ring
/-- The proposition that the function preserves the order.  -/
OrderRingHom.monotone' : ∀ {α : Type u_6} {β : Type u_7} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (self : α →+*o β), Monotone (↑↑self.toRingHom).toFun
-- Mathlib.Algebra.EuclideanDomain.Field
Field.gcd_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] (a b : K), EuclideanDomain.gcd a b = if a = 0 then b else a
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_le_inv_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a b : α} [MulRightMono α], a⁻¹ ≤ b⁻¹ ↔ b ≤ a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.darts_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v'),
  (p.copy hu hv).darts = p.darts
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.ballAddSubgroup.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (c : ArchimedeanClass M), c.ballAddSubgroup = ArchimedeanClass.addSubgroup (UpperSet.Ioi c)
-- Lean.Compiler.InitAttr
/-- Registers a builtin initialization procedure.

This attribute is used internally to define builtin initialization procedures for bootstrapping and
should not be used otherwise.
 -/
Lean.builtinInitAttr : Lean.ParametricAttribute Lean.Name
-- Mathlib.AlgebraicGeometry.QuasiAffine
AlgebraicGeometry.Scheme.IsQuasiAffine.of_isAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] [Y.IsQuasiAffine], X.IsQuasiAffine
-- Mathlib.GroupTheory.IsSubnormal
_private.Mathlib.GroupTheory.IsSubnormal.0.AddSubgroup.IsSubnormal.isSubnormal_iff.match_1_1.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ) (n : ℕ),
  x = n.succ →
    (match x with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_2 n
-- Batteries.Data.Vector.Lemmas
Vector.getElem_scanl_zero : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {f : β → α → β} {as : Vector α n}, (Vector.scanl f init as)[0] = init
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.coeff_hermite_of_odd_add : ∀ {n k : ℕ}, Odd (n + k) → (Polynomial.hermite n).coeff k = 0
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Pi.ι_π_of_ne : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasProduct f] {b c : β},
  b ≠ c → CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.Limits.Pi.π f c) = 0
-- Init.Data.UInt.Lemmas
USize.toUInt64_div : ∀ (a b : USize), (a / b).toUInt64 = a.toUInt64 / b.toUInt64
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
/-- Functors between costructured arrow categories induced by morphisms in the base category
composed with fibers of `grothendieckProj L` are isomorphic to the projection `proj L X`.  -/
CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          {X Y : D} →
            (f : X ⟶ Y) →
              (CategoryTheory.CostructuredArrow.map f).comp
                  ((CategoryTheory.Grothendieck.ι (CategoryTheory.CostructuredArrow.functor L) Y).comp
                    (CategoryTheory.CostructuredArrow.grothendieckProj L)) ≅
                CategoryTheory.CostructuredArrow.proj L X
-- Lean.ErrorExplanation
Lean.getErrorExplanationsRaw : Lean.Environment → Array (Lean.Name × Lean.ErrorExplanation)
-- Std.Http.Data.Chunk
/-- Creates a simple chunk without extensions.
 -/
Std.Http.Chunk.ofByteArray : ByteArray → Std.Http.Chunk
-- Init.Data.List.Basic
List.findSome?_nil : ∀ {α : Type u} {α_1 : Type u_1} {f : α → Option α_1}, List.findSome? f [] = none
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instLatticeOfSeparatelyContinuousAdd.eq_1 : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousAdd G],
  OpenNormalAddSubgroup.instLatticeOfSeparatelyContinuousAdd =
    { toSemilatticeSup := OpenNormalAddSubgroup.instSemilatticeSupOpenNormalAddSubgroup, inf := SemilatticeInf.inf,
      inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }
-- Mathlib.FieldTheory.Finite.Basic
ZMod.fieldRange_castHom_eq_bot : ∀ {K : Type u_1} (p : ℕ) [inst : Fact (Nat.Prime p)] [inst_1 : DivisionRing K] [inst_2 : CharP K p],
  (ZMod.castHom ⋯ K).fieldRange = ⊥
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- A rewrite with a local hypothesis  -/
Mathlib.Tactic.LibraryRewrite.Kind.hypothesis : Mathlib.Tactic.LibraryRewrite.Kind
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addSemigroup : {α : Type u} → [AddSemigroup α] → AddSemigroup (WithTop α)
-- Mathlib.GroupTheory.OrderOfElement
IsAddUnit.addOrderOf_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] [Subsingleton (AddUnits G)] {x : G}, IsAddUnit x → addOrderOf x = 1
-- Mathlib.FieldTheory.PrimitiveElement
AlgHom.card : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : FiniteDimensional F E] [Algebra.IsSeparable F E] (K : Type u_3) [inst_5 : Field K] [IsAlgClosed K]
  [inst_7 : Algebra F K], Fintype.card (E →ₐ[F] K) = Module.finrank F E
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β},
  m.WF →
    (Std.DHashMap.Raw.Const.alter m k f).getKey? k =
      if (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true then some k else none
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self : ∀ {α : Type u_1} {f : Equiv.Perm α} {x : α}, f x = x → ∀ (n : ℤ), (f ^ n) x = x
-- Init.Data.Array.Basic
/-- Return `true` if `as` is a prefix of `bs`, or `false` otherwise.

Examples:
* `#[0, 1, 2].isPrefixOf #[0, 1, 2, 3] = true`
* `#[0, 1, 2].isPrefixOf #[0, 1, 2] = true`
* `#[0, 1, 2].isPrefixOf #[0, 1] = false`
* `#[].isPrefixOf #[0, 1] = true`
 -/
Array.isPrefixOf : {α : Type u} → [BEq α] → Array α → Array α → Bool
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.projective_over : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.EnoughProjectives C] (X : C),
  CategoryTheory.Projective (CategoryTheory.Projective.over X)
-- Mathlib.CategoryTheory.Sites.Preserves
/-- If `F` is a presheaf which satisfies the sheaf condition with respect to the empty presieve on the
initial object, then `F` preserves terminal objects.
 -/
CategoryTheory.Presieve.preservesTerminal_of_isSheaf_for_empty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a) →
    ∀ (hI : CategoryTheory.Limits.IsInitial I),
      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty Cᵒᵖ) F
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- The S-polynomial of two polynomials.

Denoting

- the leading monomial of polynomial $f$ and $g$ as $lm(f)$ and $lm(g)$,
- the leading coefficient of $f$ and $g$ as $lc(f)$ and $lc(g)$
  (formalized as `m.leadingCoeff f` and `m.leadingCoeff g`), and
- the least common multiple of $lm(f)$ and $lm(g)$ as $lcm(lm(f),lm(g))$,

the S-polynomial of $f$ and $g$ is defined as
$$sPoly(f,g) := (lcm(lm(f),lm(g)) / lm(f)) * lc(g) * f - (lcm(lm(f),lm(g)) / lm(g)) * lc(f) * g.$$

$(lcm(lm(f),lm(g)) / lm(f))$ and $lcm(lm(f),lm(g)) / lm(g)$ is formalized as
`monomial (m.degree g - m.degree f) 1` and `monomial (m.degree g - m.degree f) 1`, while there is
also another more direct formalization in `sPolynomial_def`.

Notice that, when the polynomial ring is over a field, S-polynomial is usually defined as
$$sPoly'(f,g) :=
  (lcm(lm(f),lm(g)) / (lm(f) * lc(f))) * f - (lcm(lm(f),lm(g)) / (lm(g) * lc(g))) * g,$$
while we avoid inverting $lc(f)$ and $lc(g)$ in this formalization so that it doesn't require a
field or units (`IsUnit`) over ring.

An equality between these two versions holds: $$sPoly(f,g) = lc(f) * lc(g) * sPoly'(f,g).$$
 -/
MonomialOrder.sPolynomial : {σ : Type u_1} →
  MonomialOrder σ → {R : Type u_2} → [inst : CommRing R] → MvPolynomial σ R → MvPolynomial σ R → MvPolynomial σ R
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.isRadical : ∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) [IsReduced B],
  IsRadical (minpoly A x)