mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.DifferentialForm.VectorField
/-- If `ω` is a differentiable `(n + 1)`-form and `V i` are `n + 2` differentiable vector fields, then

$$
  dω(V_0(x), \dots, V_{n + 1}(x)) =
    \sum_{i=0}^{n + 1} (-1)^i •
      D_x\left(ω\big(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)\big)\right)(V_i(x)) -
      \sum_{0 \le i \le j\le n} (-1)^{i + j}
        ω\big(x; [V_i, V_{j + 1}](x),
          V_0(x), …, \widehat{V_i(x)}, …, \widehat{V_{j + 1}(x)}, …, V_k(x)\big),
$$

where $[V_i, V_{j + 1}]$ is the commutator of the vector fields $V_i$ and $V_{j + 1}$.
As usual, $\widehat{V_i(x)}$ means that this item is removed from the sequence.

In informal texts, this formula is usually written as

$$
  dω(V_0(x), \dots, V_{n + 1}(x)) =
    \sum_{i=0}^{n + 1} (-1)^i •
      D_x\left(ω\big(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)\big)\right)(V_i(x)) -
      \sum_{0 \le i < j\le n + 1} (-1)^{i + j}
        ω\big(x; [V_i, V_j](x),
          V_0(x), …, \widehat{V_i(x)}, …, \widehat{V_j(x)}, …, V_k(x)\big).
$$

In the sum from our formalization,
each index `(i, j)` corresponds to the index `(Fin.castSucc i, Fin.succ j)`
in the sum used in informal texts.

For this reason, `i + j` in our sum has the opposite parity compared to informal texts,
which changes the sign before the sum from `+` to `-`.
 -/
extDerivWithin_apply_vectorField : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} {s : Set E} {x : E}
  {ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F} {V : Fin (n + 2) → E → E},
  DifferentiableWithinAt 𝕜 ω s x →
    (∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) s x) →
      UniqueDiffWithinAt 𝕜 s x →
        ((extDerivWithin ω s x) fun x_1 => V x_1 x) =
          ∑ i, (-1) ^ ↑i • (fderivWithin 𝕜 (fun x => (ω x) (i.removeNth fun x_1 => V x_1 x)) s x) (V i x) -
            ∑ i,
              ∑ j ≥ i,
                (-1) ^ (↑i + ↑j) •
                  (ω x)
                    (Matrix.vecCons (VectorField.lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
                      (j.removeNth (i.castSucc.removeNth fun x_1 => V x_1 x)))
-- Batteries.Tactic.GeneralizeProofs
/-- A copy of `propToFVar` from `GState`.  -/
Batteries.Tactic.GeneralizeProofs.AContext.propToFVar : Batteries.Tactic.GeneralizeProofs.AContext → Lean.ExprMap Lean.Expr
-- Mathlib.Algebra.Ring.Int.Parity
Int.odd_add : ∀ {m n : ℤ}, Odd (m + n) ↔ (Odd m ↔ Even n)
-- Lean.ResolveName
/-- Helper function for `resolveGlobalConstNoOverloadCore`  -/
Lean.ensureNoOverload : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.Name → List Lean.Name → m Lean.Name
-- Mathlib.Data.WSeq.Relation
/-- Definition of bisimilarity for weak sequences  -/
Stream'.WSeq.BisimO : {α : Type u} →
  (Stream'.WSeq α → Stream'.WSeq α → Prop) → Option (α × Stream'.WSeq α) → Option (α × Stream'.WSeq α) → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.toTruncated_edge : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : SSet.Edge x₀ x₁), e.toTruncated.edge = e.edge
-- Mathlib.Algebra.Order.GroupWithZero.Basic
monotone_mul_right_of_nonneg : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [MulPosMono M₀],
  0 ≤ a → Monotone fun x => x * a
-- Mathlib.Order.Filter.Curry
Filter.frequently_curry_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {s : Set α} {t : Set β},
  (∃ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ (x : α) in l, x ∈ s) ∧ ∃ᶠ (y : β) in m, y ∈ t
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α}, {a}.dedup = {a}
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.sub_eq_eval₃ : ∀ {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {a₁ : R × M}
  (a₂ : R × M) {l₁ l₂ l : Mathlib.Tactic.Module.NF R M},
  (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval → (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval
-- Mathlib.Algebra.Jordan.Basic
IsJordan.lmul_lmul_comm_lmul : ∀ {A : Type u_1} {inst : Mul A} [self : IsJordan A] (a b : A), a * a * (a * b) = a * (a * a * b)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
_private.Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory.0.CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse_map_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {X Y : CategoryTheory.Functor C (CategoryTheory.Comon D)} (α : X ⟶ Y)
  (X_1 : C), (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse✝.map α).hom.app X_1 = (α.app X_1).hom
-- Std.Data.TreeMap.Raw.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.TreeMap.Raw.entryAtIdx? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → ℕ → Option (α × β)
-- Mathlib.Data.Fintype.Quotient
/-- Given a collection of setoids indexed by a fintype `ι` and a function that for each `i : ι`
gives a term of the corresponding quotient type, then there is corresponding term in the quotient
of the product of the setoids.
See `Quotient.choice` for the noncomputable general version.  -/
Quotient.finChoice : {ι : Type u_1} →
  [Fintype ι] →
    [DecidableEq ι] → {α : ι → Sort u_2} → {S : (i : ι) → Setoid (α i)} → ((i : ι) → Quotient (S i)) → Quotient piSetoid
-- Std.Async.System
/-- CPU architecture.
 -/
Std.Async.System.OSInfo.machine : Std.Async.System.OSInfo → String
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.modifyGet_EStateM : ∀ {σ α ε : Type} (f : σ → α × σ) (post : α → σ → Prop) (epost : ε → σ → Prop),
  ⦃ fun s => post (f s).1 (f s).2 ⦄ MonadStateOf.modifyGet f ⦃ post; epost ⦄
-- Mathlib.Data.Int.GCD
Nat.xgcd_val : ∀ (x y : ℕ), x.xgcd y = (x.gcdA y, x.gcdB y)
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
/-- Adic completion of a Noetherian ring `R` is flat over `R`.  -/
AdicCompletion.flat_of_isNoetherian : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) [IsNoetherianRing R], Module.Flat R (AdicCompletion I R)
-- Mathlib.Order.CompleteLattice.Defs
sInf_eq_bot : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α}, sInf s = ⊥ ↔ ∀ (b : α), ⊥ < b → ∃ a ∈ s, a < b
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_eq : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι],
  MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.mk.injEq : ∀ (stx : Lean.TSyntax `Lean.Parser.Command.declModifiers)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (visibility : Lean.Elab.Visibility)
  (isProtected : Bool) (computeKind : Lean.Elab.ComputeKind) (recKind : Lean.Elab.RecKind) (isUnsafe : Bool)
  (attrs : Array Lean.Elab.Attribute) (stx_1 : Lean.TSyntax `Lean.Parser.Command.declModifiers)
  (docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (visibility_1 : Lean.Elab.Visibility)
  (isProtected_1 : Bool) (computeKind_1 : Lean.Elab.ComputeKind) (recKind_1 : Lean.Elab.RecKind) (isUnsafe_1 : Bool)
  (attrs_1 : Array Lean.Elab.Attribute),
  ({ stx := stx, docString? := docString?, visibility := visibility, isProtected := isProtected,
        computeKind := computeKind, recKind := recKind, isUnsafe := isUnsafe, attrs := attrs } =
      { stx := stx_1, docString? := docString?_1, visibility := visibility_1, isProtected := isProtected_1,
        computeKind := computeKind_1, recKind := recKind_1, isUnsafe := isUnsafe_1, attrs := attrs_1 }) =
    (stx = stx_1 ∧
      docString? = docString?_1 ∧
        visibility = visibility_1 ∧
          isProtected = isProtected_1 ∧
            computeKind = computeKind_1 ∧ recKind = recKind_1 ∧ isUnsafe = isUnsafe_1 ∧ attrs = attrs_1)
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.linearYoneda_obj_additive : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] (X : C),
  ((CategoryTheory.linearYoneda R C).obj X).Additive
-- Mathlib.AlgebraicGeometry.Noetherian
/-- Any morphism of schemes `f : X ⟶ Y` with `X` Noetherian is quasi-compact.  -/
AlgebraicGeometry.quasiCompact_of_noetherianSpace_source : ∀ {X Y : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥X] (f : X ⟶ Y), AlgebraicGeometry.QuasiCompact f
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.psumPart_zero : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ],
  MvPolynomial.psumPart σ R (Nat.Partition.indiscrete 0) = 1
-- Mathlib.Order.Antisymmetrization
AntisymmRel.lt_congr : ∀ {α : Type u_1} {a b c d : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → AntisymmRel (fun x1 x2 => x1 ≤ x2) c d → (a < c ↔ b < d)
-- Mathlib.NumberTheory.GaussSum
/-- If `χ` is a multiplicative character of order `n` on a finite field `F`,
then `g(χ) * g(χ^(n-1)) = χ(-1)*#F`  -/
gaussSum_mul_gaussSum_pow_orderOf_sub_one : ∀ {R : Type u} [inst : Field R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] [IsDomain R']
  {χ : MulChar R R'} {ψ : AddChar R R'},
  χ ≠ 1 → ψ.IsPrimitive → gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * ↑(Fintype.card R)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getSubThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_int_mul_pi : ∀ (n : ℤ), Real.cos (↑n * Real.pi) = (-1) ^ n
-- Mathlib.Data.Finsupp.Ext
/-- If two additive homomorphisms from `α →₀ M` are equal on each `single a b`,
then they are equal.

We formulate this using equality of `AddMonoidHom`s so that `ext` tactic can apply a type-specific
extensionality lemma after this one.  E.g., if the fiber `M` is `ℕ` or `ℤ`, then it suffices to
verify `f (single a 1) = g (single a 1)`.  -/
Finsupp.addHom_ext' : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄,
  (∀ (x : α), f.comp (Finsupp.singleAddHom x) = g.comp (Finsupp.singleAddHom x)) → f = g
-- Mathlib.Data.List.Zip
List.revzip_map_fst : ∀ {α : Type u} (l : List α), List.map Prod.fst l.revzip = l
-- Lean.Elab.Command
Lean.Elab.Command.State.snapshotTasks : Lean.Elab.Command.State → Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_leadingTerm_mul' : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
  (p₁ p₂ q₁ q₂ : MvPolynomial σ R),
  m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    (MvPolynomial.monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
        (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
      m.sPolynomial q₁ q₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey! =
    t.minKey?.elim k fun k' => if compare k k' = Ordering.lt then k else k'
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.measure_preimage_neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G)
  [μ.IsNegInvariant] (A : Set G), μ (Neg.neg ⁻¹' A) = μ A
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `isClosed_setOfPred_map_zero`. -/
isClosed_setOf_map_zero : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : Zero M₁] [inst_3 : Zero M₂],
  IsClosed {f | f 0 = 0}
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply' : ∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [inst_1 : Fact (Nat.Prime p)]
  [inst_2 : NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial (ZMod p)}
  (hQ : Q ∈ RingOfIntegers.monicFactorsMod θ p),
  (↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩)).inertiaDeg ℤ = Q.natDegree
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.Entry.origType : Lean.Meta.SimpAll.Entry → Lean.Expr
-- Mathlib.Topology.Bornology.Absorbs
absorbs_neg_neg : ∀ {M : Type u_1} {E : Type u_2} [inst : Monoid M] [inst_1 : AddGroup E] [inst_2 : DistribMulAction M E]
  [inst_3 : Bornology M] {s t : Set E}, Absorbs M (-s) (-t) ↔ Absorbs M s t
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.simprocSEvalExtension : Lean.Meta.Simp.SimprocExtension
-- Mathlib.Algebra.Group.Action.Defs
instVAddCommClassOfVAddAssocClass : ∀ {R : Type u_9} {M : Type u_10} [inst : AddCommMonoid M] [inst_1 : VAdd R M] [VAddAssocClass R M M],
  VAddCommClass R M M
-- Lean.Meta.Tactic.Simp.Main
/-- Process the given congruence theorem hypothesis. Return true if it made "progress".  -/
Lean.Meta.Simp.processCongrHypothesis : Lean.Expr → Lean.Expr → Lean.Meta.SimpM Bool
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseOffsetO : (Std.Time.OffsetO → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Mathlib.Lean.Expr.Basic
/-- The brackets corresponding to a given `BinderInfo`.  -/
Lean.BinderInfo.brackets : Lean.BinderInfo → String × String
-- Mathlib.GroupTheory.PushoutI
/-- Given a word in `CoprodI`, if every letter is in the transversal and when
we multiply by an element of the base group it still has this property,
then the element of the base group we multiplied by was one.  -/
Monoid.PushoutI.NormalWord.eq_one_of_smul_normalized : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] (w : Monoid.CoprodI.Word G) {i : ι} (h : H),
  (∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) →
    (∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (Monoid.CoprodI.of ((φ i) h) • w).toList → g ∈ d.set j) → h = 1
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- Adjoining a finite subset is compact in the lattice of intermediate fields.  -/
IntermediateField.adjoin_finite_isCompactElement : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
  S.Finite → IsCompactElement (IntermediateField.adjoin F S)
-- Mathlib.Topology.Order.LowerUpperTopology
/-- Left-infinite right-closed intervals $(-∞,a]$ are closed in the upper topology.  -/
Topology.IsUpper.instClosedIicTopology : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α], ClosedIicTopology α
-- Mathlib.Logic.Equiv.Set
/-- An empty set is equivalent to a `PEmpty` type.  -/
Equiv.Set.pempty : (α : Type u_3) → ↑∅ ≃ PEmpty.{u_4}
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The even part of the Hurwitz zeta function, i.e. the meromorphic function of `s` which agrees
with `1 / 2 * ∑' (n : ℤ), 1 / |n + a| ^ s` for `1 < re s`  -/
HurwitzZeta.hurwitzZetaEven : UnitAddCircle → ℂ → ℂ
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Complex.volume_sum_rpow_lt_one : ∀ (ι : Type u_1) [inst : Fintype ι] {p : ℝ},
  1 ≤ p →
    MeasureTheory.volume {x | ∑ i, ‖x i‖ ^ p < 1} =
      ENNReal.ofReal ((Real.pi * Real.Gamma (2 / p + 1)) ^ Fintype.card ι / Real.Gamma (2 * ↑(Fintype.card ι) / p + 1))
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.map_apply : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) (v : V), (SimpleGraph.Embedding.map f G) v = f v
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.verify₂ : UInt8 → UInt8 → Bool
-- Init.Data.Vector.Lemmas
Vector.toArray_emptyWithCapacity : ∀ {α : Type u_1} {cap : ℕ}, (Vector.emptyWithCapacity cap).toArray = Array.emptyWithCapacity cap
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictMono_comp_ofDual_iff`. -/
StrictAnti.dual_left : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti f → StrictMono (f ∘ ⇑OrderDual.ofDual)
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_le_norm_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a‖ - ‖b‖ ≤ ‖a + b‖
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_insert_le : ∀ {α : Type u} {s : Set α} {a : α}, Cardinal.mk ↑(insert a s) ≤ Cardinal.mk ↑s + 1
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.sylvesterDeriv.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R),
  f.sylvesterDeriv =
    if hn : f.natDegree = 0 then 0
    else
      ((Polynomial.derivative f).sylvester f (f.natDegree - 1) f.natDegree).updateRow ⟨2 * f.natDegree - 2, ⋯⟩ fun j =>
        if ↑j = f.natDegree - 2 then 1 else if ↑j = 2 * f.natDegree - 2 then ↑f.natDegree else 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_ofList_le : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)}, (Std.DHashMap.ofList l).size ≤ l.length
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.neg_one_notMem' : ∀ {R : Type u_1} [inst : CommRing R] (self : RingPreordering R), -1 ∉ (↑self).carrier
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.first_contAux_eq_h_one : ∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K], g.contsAux 1 = { a := g.h, b := 1 }
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.inv' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {z : M} {F' : Type u_21}
  [inst_6 : NormedDivisionRing F'] [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'} {p' : TangentSpace I z →L[𝕜] F'},
  HasMFDerivAt[s] p z p' → p z ≠ 0 → HasMFDerivAt[s] p⁻¹ z (-(MulOpposite.op (p z)⁻¹ • (p z)⁻¹ • p'))
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.le_hittingAfter : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} (ω : Ω), ↑n ≤ MeasureTheory.hittingAfter u s n ω
-- Mathlib.Topology.MetricSpace.Closeds
/-- **Alias** of `Metric.hausdorffEDist_le_of_mem_hausdorffEntourage`. -/
EMetric.hausdorffEdist_le_of_mem_hausdorffEntourage : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {s t : Set α} {δ : ENNReal},
  (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ} → Metric.hausdorffEDist s t ≤ δ
-- Mathlib.Analysis.Normed.Group.Basic
nndist_eq_nnnorm_inv_mul : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), nndist a b = ‖a⁻¹ * b‖₊
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.eq_4 : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α),
  Lean.Grind.Linarith.Expr.denoteN ctx Lean.Grind.Linarith.Expr.zero = 0
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `a ≠ 0`. See `inv_mul_cancel_left`.  -/
le_inv_mul_left : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] {a b : G₀}, b ≤ 0 → b ≤ a⁻¹ * (a * b)
-- Mathlib.Data.Finset.Filter
Finset.filter_nonempty_iff : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, (Finset.filter p s).Nonempty ↔ ∃ a ∈ s, p a
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapLM_zero_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {f : ContDiffMapSupportedIn E F n K}
  {x : E}, ((ContDiffMapSupportedIn.structureMapLM 𝕜 n 0) f) x = ContinuousMultilinearMap.uncurry0 ℝ E (f x)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.eps_pow_five_pos : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ} {ε : ℝ},
  100 ≤ 4 ^ P.parts.card * ε ^ 5 → 0 < ε ^ 5
-- Mathlib.Algebra.Category.Grp.EpiMono
_private.Mathlib.Algebra.Category.Grp.EpiMono.0.GrpCat.SurjectiveOfEpiAuxs.«term∞» : Lean.ParserDescr
-- Mathlib.Order.Defs.Unbundled
antisymm : ∀ {α : Sort u_1} {r : α → α → Prop} {a b : α} [Std.Antisymm r], r a b → r b a → a = b
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_X : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], Polynomial.X.support = {1}
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β},
  m₁.WF →
    m₂.WF →
      ∀ (f : α → β → Option γ), m₁.Equiv m₂ → (Std.HashMap.Raw.filterMap f m₁).Equiv (Std.HashMap.Raw.filterMap f m₂)
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M`, the natural hom sending `y : M`, `M` a `CommMonoid`, to the equivalence class
of `(y, 1)` in the Localization of `M` at the Submonoid generated by `x`.  -/
Localization.Away.monoidOf : {M : Type u_1} → [inst : CommMonoid M] → (x : M) → Submonoid.LocalizationMap.AwayMap x (Localization.Away x)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.ext_iff : ∀ {𝕜 : Type u} {A : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  {a b : DoubleCentralizer 𝕜 A}, a = b ↔ a.toProd = b.toProd
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Sheaf.isLocallySurjective_iff_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F G : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ G),
  CategoryTheory.Sheaf.IsLocallySurjective f ↔ CategoryTheory.IsIso (CategoryTheory.Sheaf.imageι f)
-- Mathlib.Data.List.Sigma
List.nodupKeys_flatten : ∀ {α : Type u} {β : α → Type v} {L : List (List (Sigma β))},
  L.flatten.NodupKeys ↔ (∀ l ∈ L, l.NodupKeys) ∧ List.Pairwise List.Disjoint (List.map List.keys L)
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R),
  ↑(TensorProduct.quotTensorEquivQuotSMul M I) ∘ₗ LinearMap.rTensor M (Submodule.mkQ I) =
    (I • ⊤).mkQ ∘ₗ ↑(TensorProduct.lid R M)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.coe_trans_mulEquiv : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Mul α] [inst_4 : Mul β] [inst_5 : Mul γ] (f : α ≃*o β) (g : β ≃*o γ), ↑(f.trans g) = (↑f).trans ↑g
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_pi : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {ι : Type u_4} {φ : ι → Type u_5} [inst_4 : (i : ι) → TopologicalSpace (φ i)]
  [inst_5 : (i : ι) → AddCommMonoid (φ i)] [inst_6 : (i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i),
  ↑(ContinuousLinearMap.pi f) = LinearMap.pi fun i => ↑(f i)
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithBot.decidableLT.match_1.eq_2 : ∀ {α : Type u_1} (motive : WithBot α → WithBot α → Sort u_2) (a : α) (h_1 : (x : WithBot α) → motive x none)
  (h_2 : (a : α) → motive none (some a)) (h_3 : (a b : α) → motive (some a) (some b)),
  (match none, some a with
    | x, none => h_1 x
    | none, some a => h_2 a
    | some a, some b => h_3 a b) =
    h_2 a
-- Mathlib.Analysis.Convex.Extreme
inter_extremePoints_subset_extremePoints_of_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A B : Set E}, B ⊆ A → B ∩ Set.extremePoints 𝕜 A ⊆ Set.extremePoints 𝕜 B