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
η : R
hη : 0 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
H :
  ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = d) (h_lC : 0 < P.leadingCoeff),
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
h_lC : ¬0 < P.leadingCoeff
⊢ 0 < (-P).leadingCoeff

Tactic:
grind [leadingCoeff_eq_zero, leadingCoeff_neg]

Premises used: Polynomial.leadingCoeff_eq_zero, Polynomial.leadingCoeff_neg
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
H :
  ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = d) (h_lC : 0 < P.leadingCoeff),
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
h_lC : ¬0 < P.leadingCoeff
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
simpa using @H (-P) (by simpa) (by simpa) (by grind [leadingCoeff_eq_zero, leadingCoeff_neg])
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0

Tactic:
have h_mul : (X - C η) * P ≠ 0 := mul_ne_zero (X_sub_C_ne_zero η) hP
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
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 (X_sub_C_ne_zero η) hP, natDegree_X_sub_C, add_comm]

Premises used: Polynomial.natDegree_mul, Polynomial.natDegree_X_sub_C, add_comm, 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
hη : 0 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1

Tactic:
have h_deg_mul : natDegree ((X - C η) * P) = natDegree P + 1 := by
    rw [natDegree_mul (X_sub_C_ne_zero η) hP, 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
η : R
hη : 0 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
zero :
  ∀
    (ih :
      ∀ m < 0,
        ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
          P.signVariations + 1 ≤
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations)
    (hd : P.natDegree = 0),
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
succ :
  ∀ (d : ℕ)
    (ih :
      ∀ m < d + 1,
        ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
          P.signVariations + 1 ≤
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations)
    (hd : P.natDegree = d + 1),
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
rcases d with _ | d
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
ih :
  ∀ m < 0,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = 0
⊢ 0 < P.coeff 0

Tactic:
grind [leadingCoeff]

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
ih :
  ∀ m < 0,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = 0
⊢ 0 < P.coeff 0

Tactic:
have hcQ : 0 < coeff P 0 := by grind [leadingCoeff]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
ih :
  ∀ m < 0,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = 0
hcQ : 0 < P.coeff 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeff 1 = P.coeff 0

Tactic:
simp_all [coeff_X_sub_C_mul, coeff_eq_zero_of_natDegree_lt]

Premises used: Polynomial.coeff_X_sub_C_mul, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
ih :
  ∀ m < 0,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = 0
hcQ : 0 < P.coeff 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeff 1 = P.coeff 0

Tactic:
have hxcQ : coeff ((X - C η) * P) 1 = coeff P 0 := by
      simp_all [coeff_X_sub_C_mul, coeff_eq_zero_of_natDegree_lt]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
ih :
  ∀ m < 0,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = 0
hcQ : 0 < P.coeff 0
hxcQ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeff 1 = P.coeff 0
zero :
  List.length (α := SignType)
          (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
            (List.filter (fun (x : SignType) ↦ decide ¬x = 0)
              (List.map (⇑SignType.sign : (a : R) → SignType)
                (List.map P.coeff (List.range (P.natDegree + 1)).reverse)))) -
        1 +
      1 ≤
    List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
          (List.filter (fun (x : SignType) ↦ decide ¬x = 0)
            (List.map (⇑SignType.sign : (a : R) → SignType)
              (List.map (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeff
                (List.range
                    ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree +
                      1)).reverse)))) -
      1
⊢ List.length (α := SignType)
          (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
            (List.filter (fun (x : SignType) ↦ decide ¬x = 0)
              (List.map (⇑SignType.sign : (a : R) → SignType) (List.map P.coeff (List.range P.degree.succ).reverse)))) -
        1 +
      1 ≤
    List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
          (List.filter (fun (x : SignType) ↦ decide ¬x = 0)
            (List.map (⇑SignType.sign : (a : R) → SignType)
              (List.map (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeff
                (List.range
                    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).degree.succ).reverse)))) -
      1

Tactic:
rw [withBotSucc_degree_eq_natDegree_add_one hP, withBotSucc_degree_eq_natDegree_add_one h_mul]

Premises used: Polynomial.withBotSucc_degree_eq_natDegree_add_one
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
ih :
  ∀ m < 0,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = 0
hcQ : 0 < P.coeff 0
hxcQ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeff 1 = P.coeff 0
⊢ List.length (α := SignType)
          (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
            (List.filter (fun (x : SignType) ↦ decide ¬x = 0)
              (List.map (⇑SignType.sign : (a : R) → SignType)
                (List.map P.coeff (List.range (P.natDegree + 1)).reverse)))) -
        1 +
      1 ≤
    List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
          (List.filter (fun (x : SignType) ↦ decide ¬x = 0)
            (List.map (⇑SignType.sign : (a : R) → SignType)
              (List.map (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeff
                (List.range
                    ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree +
                      1)).reverse)))) -
      1

Tactic:
simp [h_deg_mul, hxcQ, hη, hcQ, hd, List.range_succ]

Premises used: List.range_succ
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
succ :
  ∀ (s_nC : SignType) (hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC),
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
generalize hs_nC : SignType.sign P.nextCoeff = s_nC

Premises used: Polynomial.nextCoeff, DFunLike.coe, SignType.sign
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
succ :
  ∀ (s_nC_mul : SignType)
    (hs_nC_mul :
      (SignType.sign : (a : R) → SignType)
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
        s_nC_mul),
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
generalize hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul

Premises used: DFunLike.coe, SignType.sign
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
⊢ P.eraseLead.natDegree < d + 1

Tactic:
grind [eraseLead_natDegree_le]

Premises used: Polynomial.eraseLead_natDegree_le
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
⊢ P.eraseLead.natDegree < d + 1

Tactic:
have h_ih : P.eraseLead.natDegree < d + 1 := by grind [eraseLead_natDegree_le]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
⊢ Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)

Tactic:
simp [h_lC]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
⊢ Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)

Tactic:
have h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1 := by simp [h_lC]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
⊢ 0 < η * P.coeff (d + 1)

Tactic:
grind [leadingCoeff, mul_pos]

Premises used: Polynomial.leadingCoeff, mul_pos
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
⊢ 0 < η * P.coeff (d + 1)

Tactic:
have h_ηP : 0 < η * coeff P (d + 1) := by grind [leadingCoeff, mul_pos]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
succ :
  ∀ (hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (-1 : SignType)),
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
succ₁ :
  ∀ (hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)),
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
succ₂ :
  ∀ (hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (1 : SignType)),
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
rcases s_nC.trichotomy with rfl | rfl | rfl

Premises used: SignType.trichotomy, rfl