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
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 (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])
⊢ 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 [leadingCoeff, nextCoeff_of_natDegree_pos (hd ▸ d.succ_pos), hd, Nat.add_sub_cancel]

Premises used: Polynomial.nextCoeff_of_natDegree_pos, Polynomial.leadingCoeff, Nat.add_sub_cancel
-- 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
⊢ 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:
abel
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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])).coeff
      (0 + d) =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).coeff 0 * c

Tactic:
coeff_mul_monomial (X - C η) d 0 c

Premises used: Polynomial.C, HSub.hSub, Polynomial.coeff_mul_monomial, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)
h₁ : -(η * c) = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).coeff 0 * 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])).nextCoeff =
    -(η * c)

Tactic:
convert! coeff_mul_monomial (X - C η) d 0 c using 1

Premises used: Polynomial.C, HSub.hSub, Polynomial.coeff_mul_monomial, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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 =
    (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:
simp [hc, nextCoeff, natDegree_mul (X_sub_C_ne_zero η)]

Premises used: Polynomial.natDegree_mul, Polynomial.nextCoeff, Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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 < η
⊢ -(η * c) = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).coeff 0 * c

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)

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
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)
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
⊢ (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:
apply mt nextCoeff_eq_zero_of_eraseLead_eq_zero

Premises used: mt, Polynomial.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
η : 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])).nextCoeff =
      0

Tactic:
simp [h₁, hc, hη.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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

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']
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)
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
⊢ Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType)
    ((SignType.sign : (a : R) → SignType) (-(η * c)) : SignType)

Tactic:
simp [hη, hc, Left.sign_neg, sign_mul]

Premises used: sign_mul, Left.sign_neg
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)
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
⊢ Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType)
    ((SignType.sign : (a : R) → SignType) (-(η * c)) : SignType)

Tactic:
have h₃ : SignType.sign c ≠ SignType.sign (-(η * c)) := by
    simp [hη, hc, Left.sign_neg, sign_mul]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)
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
h₃ :
  Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType)
    ((SignType.sign : (a : R) → SignType) (-(η * c)) : SignType)
⊢ 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

Tactic:
simpa [h₁, h₂, h₃, hc, hη.ne', signVariations, List.destutter_cons_cons,
    ← leadingCoeff_cons_eraseLead, coeffList_eraseLead, leadingCoeff_eraseLead_eq_nextCoeff]
  using List.length_pos_of_ne_nil (List.destutter'_ne_nil _ _)

Premises used: Polynomial.signVariations, Polynomial.leadingCoeff_cons_eraseLead, Polynomial.coeffList_eraseLead, LT.lt.ne', Polynomial.leadingCoeff_eraseLead_eq_nextCoeff, List.length_pos_of_ne_nil, List.destutter'_ne_nil, List.destutter_cons_cons
-- 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 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
⊢ P ≠ 0

Tactic:
have h₃ := leadingCoeff_ne_zero.mp h₁.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 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
⊢ P.eraseLead.natDegree + 1 = P.natDegree

Tactic:
have h₄ := natDegree_eraseLead_add_one h₂
-- 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 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0

Tactic:
have h₅ : (X - C η) ≠ 0 := X_sub_C_ne_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 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
⊢ P.eraseLead ≠ 0

Tactic:
have h₆ : P.eraseLead ≠ 0 := mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₂
-- 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 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
obtain :
  ∀ (d : ℕ) (hd : P.natDegree = 0 + d + 1),
    ∃ (c₀ : R) (cs : List R),
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
          P.nextCoeff :: cs
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs

Tactic:
obtain ⟨d, hd⟩ := Nat.exists_eq_add_of_lt (natDegree_pos_of_nextCoeff_ne_zero h₂)

Premises used: Polynomial.natDegree_pos_of_nextCoeff_ne_zero, Nat.exists_eq_add_of_lt
-- 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 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
⊢ P.eraseLead.leadingCoeff = P.nextCoeff

Tactic:
apply leadingCoeff_eraseLead_eq_nextCoeff at h₂

Premises used: Polynomial.leadingCoeff_eraseLead_eq_nextCoeff
-- 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 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
⊢ (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).leadingCoeff ::
      (List.replicate
          ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree -
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.degree.succ)
          0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)

Tactic:
have h_cons := coeffList_eraseLead (mul_ne_zero h₅ h₆)
-- 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 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
h_cons :
  (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).leadingCoeff ::
      (List.replicate
          ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).natDegree -
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.degree.succ)
          0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
generalize :
  ∀ (n : ℕ)
    (h_cons :
      (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).leadingCoeff ::
          (List.replicate n 0 ++
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)),
    ∃ (c₀ : R) (cs : List R),
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
          P.nextCoeff :: cs
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs

Tactic:
generalize ((X - C η) * P.eraseLead).natDegree -
    ((X - C η) * P.eraseLead).eraseLead.degree.succ = n at h_cons ⊢
-- 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 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (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).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList =
      P.leadingCoeff ::
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff ::
          (List.replicate n 0 ++
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList) ∧
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
      P.nextCoeff ::
        (List.replicate n 0 ++
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
⊢ ∃ (c₀ : R) (cs : List R),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs

Tactic:
use nextCoeff ((X - C η) * P), .replicate n 0 ++ coeffList ((X - C η) * P.eraseLead).eraseLead

Premises used: Polynomial.C, HMul.hMul, HSub.hSub, Polynomial.nextCoeff, Polynomial.coeffList, Polynomial.X, DFunLike.coe
-- 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 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (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).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList =
    P.leadingCoeff ::
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff ::
        (List.replicate n 0 ++
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h₇ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    P.nextCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList =
      P.leadingCoeff ::
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff ::
          (List.replicate n 0 ++
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList) ∧
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
      P.nextCoeff ::
        (List.replicate n 0 ++
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)

Tactic:
constructor
-- 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 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (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).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).natDegree + P.natDegree = P.natDegree + 1
rw₁ : 1 + P.natDegree = P.natDegree + 1
rw₂ rw₃ : P.natDegree + 1 = P.natDegree + 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1

Tactic:
rw [natDegree_mul h₅ h₃, natDegree_X_sub_C, add_comm]

Premises used: Polynomial.natDegree_mul, Polynomial.natDegree_X_sub_C, add_comm
-- 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 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (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).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1

Tactic:
have h₇ : natDegree ((X - C η) * P) = P.natDegree + 1 := by
      rw [natDegree_mul h₅ h₃, natDegree_X_sub_C, add_comm]