Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case neg.cons
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
⊢ (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
          (match decide ¬False with
          | true =>
            SignType.sign P.leadingCoeff ::
              ((if (decide ¬SignType.sign 0 = 0) = true then
                  List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0)
                else []) ++
                match decide ¬SignType.sign c = 0 with
                | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
                | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))
          | false =>
            (if (decide ¬SignType.sign 0 = 0) = true then
                List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0)
              else []) ++
              match decide ¬SignType.sign c = 0 with
              | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
              | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
            (match decide ¬SignType.sign c = 0 with
            | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
            | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))).length -
        1 +
      if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

Tactic:
have h₁ : SignType.sign c ≠ 0 := by
    by_contra h₂
    suffices eraseLead P = 0 by grind [coeffList_zero]
    by_contra h
    have := coeffList_eq_cons_leadingCoeff h
    grind [leadingCoeff_eq_zero, sign_eq_zero_iff]

Goal state after:
case neg.cons
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₁ : SignType.sign c ≠ 0
⊢ (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
          (match decide ¬False with
          | true =>
            SignType.sign P.leadingCoeff ::
              ((if (decide ¬SignType.sign 0 = 0) = true then
                  List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0)
                else []) ++
                match decide ¬SignType.sign c = 0 with
                | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
                | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))
          | false =>
            (if (decide ¬SignType.sign 0 = 0) = true then
                List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0)
              else []) ++
              match decide ¬SignType.sign c = 0 with
              | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
              | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
            (match decide ¬SignType.sign c = 0 with
            | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
            | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))).length -
        1 +
      if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0