Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
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
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ (if ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff then
          SignType.sign P.leadingCoeff ::
            List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
              (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))
        else
          List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (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

pp: case neg
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
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ (if ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff then
          SignType.sign P.leadingCoeff ::
            List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
              (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))
        else
          List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (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:
· grind [SignType.neg_eq_self_iff]

Goal state after:
case neg
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
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ (if ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff then
          SignType.sign P.leadingCoeff ::
            List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
              (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))
        else
          List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (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