awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 < 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).natDegree = P.natDegree + 1
h₈ :
  (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 P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
this_1 :
  P.eraseLead.natDegree + 2 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList.length
this_2 : P.natDegree + 2 = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList.length
this_3 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff = P.leadingCoeff
h₉ : ¬(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = 0
this_4 :
  (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 :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff ::
      (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).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)
have this₁ : (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 := coeffList_eraseLead (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₉)
-- 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 < 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).natDegree = P.natDegree + 1
h₈ :
  (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 P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
this_1 :
  P.eraseLead.natDegree + 2 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList.length
this_2 : P.natDegree + 2 = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList.length
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff = P.leadingCoeff
h₉ : ¬(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).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)
have neg : (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 ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead by
        have := leadingCoeff_cons_eraseLead h₉
        have := coeffList_eraseLead (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₉)
        grind [leadingCoeff_eraseLead_eq_nextCoeff]
-- 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 < 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).natDegree = P.natDegree + 1
h₈ :
  (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 P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
this_1 :
  P.eraseLead.natDegree + 2 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList.length
this_2 : P.natDegree + 2 = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList.length
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff = P.leadingCoeff
h₉ : ¬(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.eraseLead =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead
have neg : (monomial P.natDegree : (a : R) → R[X])
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
  HSub.hSub (α := R[X]) ((monomial P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) η : R[X])
      ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff : R[X]))
Tactic: suffices monomial P.natDegree ((X - C η) * P).nextCoeff =
          monomial P.natDegree P.nextCoeff - C η * monomial P.natDegree P.leadingCoeff by
        grind [X_mul_monomial, sub_mul, mul_sub, self_sub_monomial_natDegree_leadingCoeff,
          natDegree_eraseLead_add_one, leadingCoeff_eraseLead_eq_nextCoeff]
-- 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 < 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.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)
have h : (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) =
  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: rw [h_cons, leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, h₂]
-- 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 < 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.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).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.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)
have h₇ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).leadingCoeff * 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) =
  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: rw [h_cons, leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, h₂]
-- 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 < 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.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).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)
h₇ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).leadingCoeff * 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) =
    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)
have h₈ : 1 * 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) =
  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: rw [h_cons, leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, h₂]
-- 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 < 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.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).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)
h₇ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).leadingCoeff * 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) =
    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₈ :
  1 * 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) =
    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)
have h₉ : 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) =
  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: rw [h_cons, leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, h₂]
-- 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 < 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.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).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)
h₇ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).leadingCoeff * 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) =
    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₈ :
  1 * 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) =
    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₉ :
  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) =
    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)
have h₁₀ : P.nextCoeff ::
    (List.replicate n 0 ++
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).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: rw [h_cons, leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, h₂]
-- 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 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
⊢ (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).signVariations
have obtain : ∀ (c₀ : R) (cs : List R)
  (hcs :
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs)
  (hecs :
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs),
  (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).signVariations
Tactic: obtain ⟨c₀, cs, ⟨hcs, hecs⟩⟩ := exists_cons_of_leadingCoeff_pos η h h₂.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 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
⊢ (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).signVariations
have simp : List.length (α := SignType)
    (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
      (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
  List.length (α := SignType)
    (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
          ((SignType.sign : (a : R) → SignType) c₀ :: List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
      List SignType)
Tactic: simp +decide only [hcs, hecs, h, h₂, signVariations, List.destutter, List.map_cons, sign_pos,
    List.filter_cons_of_pos, tsub_le_iff_right,
    Nat.sub_add_cancel (List.length_pos_of_ne_nil (List.destutter'_ne_nil _ _))]
-- 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 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
⊢ List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
    List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
          (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
            ((SignType.sign : (a : R) → SignType) c₀ :: List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType)
have rw : List.length (α := SignType)
    (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
      (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
  List.length (α := SignType)
    (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (if decide (Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) (0 : SignType)) = true then
          (SignType.sign : (a : R) → SignType) c₀ ::
            List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)
        else List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
      List SignType)
Tactic: rw [List.filter_cons]