awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
hndxeP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree = P.natDegree
hQ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff < 0
hndexP0 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree = P.natDegree
this :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.eraseLead =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
have suffices : Eq (α := List SignType)
  (List.map (⇑SignType.sign : (a : R) → SignType)
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.coeffList)
  (List.map (⇑SignType.sign : (a : R) → SignType)
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList)
Tactic: suffices (coeffList (eraseLead ((X - C η) * P))).map SignType.sign =
      (coeffList ((X - C η) * P.eraseLead)).map SignType.sign by
        rw [signVariations, signVariations, this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
hndxeP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree = P.natDegree
hQ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff < 0
hndexP0 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree = P.natDegree
this :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.eraseLead =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead
⊢ Eq (α := List SignType)
    (List.map (⇑SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.coeffList)
    (List.map (⇑SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList)
have this₁ : 0 < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree
Tactic: have : 0 < natDegree ((X - C η) * P.eraseLead) := by lia
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
hndxeP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree = P.natDegree
hQ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff < 0
hndexP0 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree = P.natDegree
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
have suffices : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.eraseLead =
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead
Tactic: suffices eraseLead (eraseLead ((X - C η) * P)) = eraseLead ((X - C η) * P.eraseLead) by
    suffices (coeffList (eraseLead ((X - C η) * P))).map SignType.sign =
      (coeffList ((X - C η) * P.eraseLead)).map SignType.sign by
        rw [signVariations, signVariations, this]
    have : 0 < natDegree ((X - C η) * P.eraseLead) := by lia
    grind [leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, leadingCoeff_eraseLead_eq_nextCoeff,
      LT.lt.ne, sign_neg, coeffList_eraseLead, ne_zero_of_natDegree_gt,
      nextCoeff_eq_zero_of_eraseLead_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
hndxeP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree = P.natDegree
hQ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff < 0
hndexP0 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree = P.natDegree
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.eraseLead =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead
have rw : HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead
    ((monomial (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree :
          (a : R) → R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      R[X]) =
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead
Tactic: rw [← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_eraseLead_eq_nextCoeff hQ₁.ne]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
hndxeP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree = P.natDegree
hQ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff < 0
hndexP0 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree = P.natDegree
⊢ HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead
      ((monomial (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree :
            (a : R) → R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
        R[X]) =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead
have rw : HSub.hSub (β := R[X])
    (HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P)
      ((monomial (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree : (a : R) → R[X])
          P.leadingCoeff :
        R[X]))
    ((monomial P.natDegree : (a : R) → R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      R[X]) =
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead
Tactic: rw [hndexP0, ← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_monic_mul (monic_X_sub_C η)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
hndxeP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree = P.natDegree
hQ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff < 0
hndexP0 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree = P.natDegree
⊢ HSub.hSub (β := R[X])
      (HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P)
        ((monomial (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree : (a : R) → R[X])
            P.leadingCoeff :
          R[X]))
      ((monomial P.natDegree : (a : R) → R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
        R[X]) =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead
have rw : HSub.hSub (β := R[X])
    (HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P)
      ((monomial (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree : (a : R) → R[X])
          P.leadingCoeff :
        R[X]))
    ((monomial P.natDegree : (a : R) → R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      R[X]) =
  HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead)
    ((monomial (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree :
          (a : R) → R[X])
        P.eraseLead.leadingCoeff :
      R[X])
Tactic: rw [← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_monic_mul (monic_X_sub_C η)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
hndxeP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree = P.natDegree
hQ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff < 0
hndexP0 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree = P.natDegree
⊢ HSub.hSub (β := R[X])
      (HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P)
        ((monomial (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree : (a : R) → R[X])
            P.leadingCoeff :
          R[X]))
      ((monomial P.natDegree : (a : R) → R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
        R[X]) =
    HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead)
      ((monomial (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree :
            (a : R) → R[X])
          P.eraseLead.leadingCoeff :
        R[X])
have rw : HSub.hSub (β := R[X])
    (HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P)
      ((monomial (P.natDegree + 1) : (a : R) → R[X]) P.leadingCoeff : R[X]))
    ((monomial P.natDegree : (a : R) → R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      R[X]) =
  HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead)
    ((monomial P.natDegree : (a : R) → R[X]) P.eraseLead.leadingCoeff : R[X])
Tactic: rw [hndxeP, hndxP]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
hndxeP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree = P.natDegree
hQ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff < 0
hndexP0 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree = P.natDegree
⊢ HSub.hSub (β := R[X])
      (HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P)
        ((monomial (P.natDegree + 1) : (a : R) → R[X]) P.leadingCoeff : R[X]))
      ((monomial P.natDegree : (a : R) → R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
        R[X]) =
    HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead)
      ((monomial P.natDegree : (a : R) → R[X]) P.eraseLead.leadingCoeff : R[X])
have rw : HSub.hSub (β := R[X])
    (HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P)
      ((monomial (P.natDegree + 1) : (a : R) → R[X]) P.leadingCoeff : R[X]))
    ((monomial P.natDegree : (a : R) → R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      R[X]) =
  HSub.hSub (β := R[X])
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) *
      HSub.hSub (β := R[X]) P ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff : R[X]))
    ((monomial P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
Tactic: rw [leadingCoeff_eraseLead_eq_nextCoeff hc.ne, ← self_sub_monomial_natDegree_leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
hndxeP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree = P.natDegree
hQ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff < 0
hndexP0 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree = P.natDegree
⊢ HSub.hSub (β := R[X])
      (HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P)
        ((monomial (P.natDegree + 1) : (a : R) → R[X]) P.leadingCoeff : R[X]))
      ((monomial P.natDegree : (a : R) → R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
        R[X]) =
    HSub.hSub (β := R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) *
        HSub.hSub (β := R[X]) P ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff : R[X]))
      ((monomial P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
have rw : HSub.hSub (β := R[X]) (X * P - HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) η : R[X]) P)
      ((monomial (P.natDegree + 1) : (a : R) → R[X]) P.leadingCoeff : R[X]) -
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial P.natDegree : (a : R) → R[X]) (P.coeff d) : R[X])
      ((monomial P.natDegree : (a : R) → R[X]) (η * P.coeff (d + 1)) : R[X]) =
  HSub.hSub (β := R[X])
    (X * P - HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) η : R[X]) P -
      HSub.hSub (α := R[X]) (β := R[X]) ((monomial (P.natDegree + 1) : (a : R) → R[X]) P.leadingCoeff : R[X])
        ((monomial P.natDegree : (a : R) → R[X]) (η * P.leadingCoeff) : R[X]))
    ((monomial P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
Tactic: rw [hQ, mul_sub, sub_mul, sub_mul, X_mul_monomial, C_mul_monomial, monomial_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
hndxeP : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree = P.natDegree
hQ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff < 0
hndexP0 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree = P.natDegree
⊢ HSub.hSub (β := R[X]) (X * P - HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) η : R[X]) P)
        ((monomial (P.natDegree + 1) : (a : R) → R[X]) P.leadingCoeff : R[X]) -
      HSub.hSub (α := R[X]) (β := R[X]) ((monomial P.natDegree : (a : R) → R[X]) (P.coeff d) : R[X])
        ((monomial P.natDegree : (a : R) → R[X]) (η * P.coeff (d + 1)) : R[X]) =
    HSub.hSub (β := R[X])
      (X * P - HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) η : R[X]) P -
        HSub.hSub (α := R[X]) (β := R[X]) ((monomial (P.natDegree + 1) : (a : R) → R[X]) P.leadingCoeff : R[X])
          ((monomial P.natDegree : (a : R) → R[X]) (η * P.leadingCoeff) : R[X]))
      ((monomial P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
have rw : HSub.hSub (β := R[X]) (X * P - HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) η : R[X]) P)
      ((monomial (d + 1 + 1) : (a : R) → R[X]) (P.coeff (d + 1)) : R[X]) -
    HSub.hSub (α := R[X]) (β := R[X]) ((monomial (d + 1) : (a : R) → R[X]) (P.coeff d) : R[X])
      ((monomial (d + 1) : (a : R) → R[X]) (η * P.coeff (d + 1)) : R[X]) =
  HSub.hSub (β := R[X])
    (X * P - HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) η : R[X]) P -
      HSub.hSub (α := R[X]) (β := R[X]) ((monomial (d + 1 + 1) : (a : R) → R[X]) (P.coeff (d + 1)) : R[X])
        ((monomial (d + 1) : (a : R) → R[X]) (η * P.coeff (d + 1)) : R[X]))
    ((monomial (d + 1) : (a : R) → R[X]) (P.coeff d) : R[X])
Tactic: rw [leadingCoeff, nextCoeff_of_natDegree_pos (hd ▸ d.succ_pos), hd, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
⊢ (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).nextCoeff =
    -(η * c)
have h : (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
      ((monomial d : (a : R) → R[X]) c : R[X])).nextCoeff =
  (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).coeff
    (0 + d)
Tactic: convert! coeff_mul_monomial (X - C η) d 0 c using 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
h :
  (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).nextCoeff =
    (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
          ((monomial d : (a : R) → R[X]) c : R[X])).coeff
      (0 + d)
⊢ (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).nextCoeff =
    -(η * c)
have h₁ : -(η * c) = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).coeff 0 * c
Tactic: convert! coeff_mul_monomial (X - C η) d 0 c using 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
⊢ signVariations.{u_1} (R := R) ((monomial d : (a : R) → R[X]) c) + 1 ≤
    (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).signVariations
have h₁ : (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
      ((monomial d : (a : R) → R[X]) c : R[X])).nextCoeff =
  -(η * c)
Tactic: have h₁ : nextCoeff ((X - C η) * monomial d c) = -(η * c) := by
    convert! coeff_mul_monomial (X - C η) d 0 c using 1
    · simp [hc, nextCoeff, natDegree_mul (X_sub_C_ne_zero η)]
    · simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
h₁ :
  (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).nextCoeff =
    -(η * c)
⊢ (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).eraseLead ≠
    0
have apply : ¬(HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).nextCoeff =
    0
Tactic: apply mt nextCoeff_eq_zero_of_eraseLead_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
h₁ :
  (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).nextCoeff =
    -(η * c)
⊢ signVariations.{u_1} (R := R) ((monomial d : (a : R) → R[X]) c) + 1 ≤
    (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
        ((monomial d : (a : R) → R[X]) c : R[X])).signVariations
have h₂ : (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]))
      ((monomial d : (a : R) → R[X]) c : R[X])).eraseLead ≠
  0
Tactic: have h₂ : eraseLead ((X - C η) * monomial d c) ≠ 0 := by
    apply mt nextCoeff_eq_zero_of_eraseLead_eq_zero
    simp [h₁, hc, hη.ne']