-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)
neg :
  List.length (α := SignType)
        (if
              ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
                  ((SignType.sign : (a : R) → SignType) c : SignType) then
            (SignType.sign : (a : R) → SignType) P.leadingCoeff ::
              List.destutter' (fun (x1 x2 : SignType) ↦ ¬x1 = x2) ((SignType.sign : (a : R) → SignType) c)
                (List.filter (fun (x : SignType) ↦ !decide (x = 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))
          else
            List.destutter' (fun (x1 x2 : SignType) ↦ ¬x1 = x2) ((SignType.sign : (a : R) → SignType) P.leadingCoeff)
              (List.filter (fun (x : SignType) ↦ !decide (x = 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
          List SignType) -
      1 =
    List.length (α := SignType)
          (List.destutter' (fun (x1 x2 : SignType) ↦ ¬x1 = x2) ((SignType.sign : (a : R) → SignType) c)
              (List.filter (fun (x : SignType) ↦ !decide (x = 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
            List SignType) -
        1 +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
⊢ List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
          (match (motive := Bool → List SignType) decide ¬False with
          | true =>
            (SignType.sign : (a : R) → SignType) P.leadingCoeff ::
              HAppend.hAppend (α := List SignType) (β := List SignType)
                (if
                      (decide ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) 0 : SignType) (0 : SignType)) =
                        true then
                    List.replicate (P.natDegree - P.eraseLead.degree.succ) ((SignType.sign : (a : R) → SignType) 0)
                  else [] :
                  List SignType)
                (match (motive := Bool → List SignType)
                    decide ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType) with
                  | true =>
                    (SignType.sign : (a : R) → SignType) c ::
                      List.filter (fun (x : SignType) ↦ decide ¬x = 0)
                        (List.map (⇑SignType.sign : (a : R) → SignType) cs)
                  | false =>
                    List.filter (fun (x : SignType) ↦ decide ¬x = 0)
                      (List.map (⇑SignType.sign : (a : R) → SignType) cs) :
                  List SignType)
          | false =>
            HAppend.hAppend (α := List SignType) (β := List SignType)
              (if
                    (decide ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) 0 : SignType) (0 : SignType)) =
                      true then
                  List.replicate (P.natDegree - P.eraseLead.degree.succ) ((SignType.sign : (a : R) → SignType) 0)
                else [] :
                List SignType)
              (match (motive := Bool → List SignType)
                  decide ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType) with
                | true =>
                  (SignType.sign : (a : R) → SignType) c ::
                    List.filter (fun (x : SignType) ↦ decide ¬x = 0) (List.map (⇑SignType.sign : (a : R) → SignType) cs)
                | false =>
                  List.filter (fun (x : SignType) ↦ decide ¬x = 0) (List.map (⇑SignType.sign : (a : R) → SignType) cs) :
                List SignType))) -
      1 =
    List.length (α := SignType)
          (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
            (match (motive := Bool → List SignType)
              decide ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType) with
            | true =>
              (SignType.sign : (a : R) → SignType) c ::
                List.filter (fun (x : SignType) ↦ decide ¬x = 0) (List.map (⇑SignType.sign : (a : R) → SignType) cs)
            | false =>
              List.filter (fun (x : SignType) ↦ decide ¬x = 0) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) -
        1 +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0

Tactic:
simp only [decide_not, sign_zero, List.destutter, Bool.false_eq_true, reduceIte, h₁,
    decide_false, Bool.not_false, List.nil_append, List.destutter', decide_true, Bool.not_true]

Premises used: Bool.not_false, sign_zero, Bool.false_eq_true, List.destutter, decide_false, decide_not, List.destutter', decide_true, List.nil_append, reduceIte, Bool.not_true