awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
rw :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree + 1 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree
rw₁ rw₂ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree + 1 = P.natDegree + 1

Tactic:
rw [← hndxP, natDegree_eraseLead_add_one hQ₁.ne]

Premises used: Polynomial.natDegree_eraseLead_add_one, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.natDegree = P.natDegree

Tactic:
have hndexP0 : natDegree (eraseLead ((X - C η) * P)) = P.natDegree := by
    apply Nat.add_right_cancel (m := 1)
    rw [← hndxP, natDegree_eraseLead_add_one hQ₁.ne]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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)
⊢ (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

Tactic:
suffices (coeffList (eraseLead ((X - C η) * P))).map SignType.sign =
      (coeffList ((X - C η) * P.eraseLead)).map SignType.sign by
        rw [signVariations, signVariations, this]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
⊢ 0 < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
⊢ 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
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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_1 :
  (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
this : 0 < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree
⊢ 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:
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]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.coeffList_eraseLead, Polynomial.ne_zero_of_natDegree_gt, sign_neg, Polynomial.leadingCoeff_X_sub_C, Polynomial.leadingCoeff_eraseLead_eq_nextCoeff, Polynomial.nextCoeff_eq_zero_of_eraseLead_eq_zero, one_mul, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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
⊢ (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

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]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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
⊢ (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:
rw [← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_eraseLead_eq_nextCoeff hQ₁.ne]

Premises used: Polynomial.self_sub_monomial_natDegree_leadingCoeff, Polynomial.leadingCoeff_eraseLead_eq_nextCoeff, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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
⊢ 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 [hndexP0, ← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_monic_mul (monic_X_sub_C η)]

Premises used: Polynomial.monic_X_sub_C, Polynomial.self_sub_monomial_natDegree_leadingCoeff, Polynomial.leadingCoeff_monic_mul
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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])
⊢ 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 [← self_sub_monomial_natDegree_leadingCoeff, leadingCoeff_monic_mul (monic_X_sub_C η)]

Premises used: Polynomial.monic_X_sub_C, Polynomial.self_sub_monomial_natDegree_leadingCoeff, Polynomial.leadingCoeff_monic_mul
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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])
⊢ 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 [hndxeP, hndxP]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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])
⊢ 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 [leadingCoeff_eraseLead_eq_nextCoeff hc.ne, ← self_sub_monomial_natDegree_leadingCoeff]

Premises used: Polynomial.self_sub_monomial_natDegree_leadingCoeff, Polynomial.leadingCoeff_eraseLead_eq_nextCoeff, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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])
⊢ 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 [hQ, mul_sub, sub_mul, sub_mul, X_mul_monomial, C_mul_monomial, monomial_sub]

Premises used: mul_sub, Polynomial.C_mul_monomial, sub_mul, Polynomial.X_mul_monomial, Polynomial.monomial_sub