-- 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 : P ≠ 0
d : ℕ
hd : P.natDegree = d
h :
  ∀ (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),
    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:
induction d using Nat.strong_induction_on generalizing P with | _ d ih =>
  -- can assume it starts positive, otherwise negate P
  wlog h_lC : 0 < leadingCoeff P generalizing P with H
  · simpa using @H (-P) (by simpa) (by simpa) (by grind [leadingCoeff_eq_zero, leadingCoeff_neg])
  --Adding a new root doesn't make the product zero, and increases degree by exactly one.
  have h_mul : (X - C η) * P ≠ 0 := mul_ne_zero (X_sub_C_ne_zero η) hP
  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]
  rcases d with _ | d
  · --P is zero degree, therefore a constant.
    have hcQ : 0 < coeff P 0 := by grind [leadingCoeff]
    have hxcQ : coeff ((X - C η) * P) 1 = coeff P 0 := by
      simp_all [coeff_X_sub_C_mul, coeff_eq_zero_of_natDegree_lt]
    dsimp [signVariations, coeffList]
    rw [withBotSucc_degree_eq_natDegree_add_one hP, withBotSucc_degree_eq_natDegree_add_one h_mul]
    simp [h_deg_mul, hxcQ, hη, hcQ, hd, List.range_succ]
  -- P is positive degree. Set up some temporary variables for signs for the nextCoeffs.
  generalize hs_nC : SignType.sign P.nextCoeff = s_nC
  generalize hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
  --We're really doing induction on `P.eraseLead` in a sense
  have h_ih : P.eraseLead.natDegree < d + 1 := by grind [eraseLead_natDegree_le]
  have h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1 := by simp [h_lC]
  have h_ηP : 0 < η * coeff P (d + 1) := by grind [leadingCoeff, mul_pos]
  rcases s_nC.trichotomy with rfl | rfl | rfl; rotate_left
  · -- P starts with [+,0,...] so (X-C)*P starts with [+,-,...].
    obtain rfl : s_nC_mul = -1 := by
      have : coeff P d = 0 := by simpa [nextCoeff, hd] using hs_nC
      simp [*, ← hs_nC_mul, nextCoeff, coeff_X_sub_C_mul]
    /- We would like to just `have : eraseLead P ≠ 0`, so that we can use the inductive
      hypothesis on eraseLead P. but that isn't actually true: we could have P a monomial
      and then eraseLead P = 0, and then the inductive hypothesis doesn't hold. (It's only
      true as written for P ≠ 0.) So we need to do a case-split and handle this separately. -/
    by_cases eraseLead P = 0
    · grind [succ_signVariations_X_sub_C_mul_monomial,
        eraseLead_add_monomial_natDegree_leadingCoeff, zero_add]
    · /- Dropping the lead of the product exactly drops the first two of the eraseLead. This
        decreases the sign variations of the eraseLead by at least one, and of the product by at
       most one, so we can induct. -/
      have : signVariations ((X - C η) * P).eraseLead + 1 =
          signVariations ((X - C η) * P) := by
        simp [-leadingCoeff_mul, ← sign_ne_zero,
          signVariations_eq_eraseLead_add_ite h_mul, leadingCoeff_eraseLead_eq_nextCoeff,
          hs_nC_mul, h_mul_lC]
      have : ((X - C η) * P.eraseLead).signVariations ≤
          ((X - C η) * P).eraseLead.signVariations := by
        have := signVariations_eraseLead_le (eraseLead ((X - C η) * P))
        rwa [← eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero hη.ne']
        grind [sign_eq_zero_iff]
      grind [signVariations_le_eraseLead_succ]
  all_goals (
    have h₁ : nextCoeff P ≠ 0 := by simp [← sign_ne_zero, hs_nC]
    specialize ih _ h_ih (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₁) rfl
    have : P.signVariations = P.eraseLead.signVariations + ?_ := by
      simp [signVariations_eq_eraseLead_add_ite hP, leadingCoeff_eraseLead_eq_nextCoeff h₁,
        hs_nC, h_lC]
      exact rfl)
  · /- P starts with [+,+,...]. (X-C)*P starts with [+,?,...]. After dropping the lead of P, this
      becomes [+,...] and [+,...]. So the sign variations on P are unchanged when we induct, while
      (X-C)*P can only lose at most one sign change. -/
    grind [sign_eq_one_iff, signVariations_X_sub_C_mul_eraseLead_le]
  · /- P starts with [+,-,...], so (X-C)*P starts with [+,-,...]. After dropping the lead of P, this
    becomes [-,...] and [-,...]. Dropping the first one of each decreases (X-C)*P by one and P by
    one, so we can induct. -/
    trans ((X - C η) * P).eraseLead.signVariations + 1
    · grind [signVariations_eraseLead_mul_X_sub_C, sign_eq_neg_one_iff]
    · suffices SignType.sign ((X - C η) * P).nextCoeff = -1 by
        simp +decide [signVariations_eq_eraseLead_add_ite h_mul, h_lC,
          leadingCoeff_eraseLead_eq_nextCoeff, ← sign_eq_zero_iff, this]
      grind [← sign_eq_neg_one_iff, coeff_X_sub_C_mul, nextCoeff]

Premises used: Polynomial.signVariations_le_eraseLead_succ, Polynomial.signVariations, Polynomial.coeff_X_sub_C_mul, Polynomial.leadingCoeff, Polynomial.eraseLead, Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff, zero_add, Polynomial.nextCoeff, Polynomial.signVariations_eraseLead_mul_X_sub_C, Polynomial.coeffList, Polynomial.signVariations_X_sub_C_mul_eraseLead_le, Polynomial.succ_signVariations_X_sub_C_mul_monomial, Polynomial.withBotSucc_degree_eq_natDegree_add_one, DFunLike.coe, SignType.sign, sign_eq_neg_one_iff, rfl, sign_eq_one_iff, List.range_succ