-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
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)
neg :
  ∀ (h_eL : P.eraseLead.coeffList = []),
    List.length (α := SignType)
          (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
              (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
                ((SignType.sign : (a : R) → SignType) P.leadingCoeff ::
                  HAppend.hAppend (α := List SignType) (β := List SignType)
                    (List.replicate (P.natDegree - P.eraseLead.degree.succ) ((SignType.sign : (a : R) → SignType) 0) :
                      List SignType)
                    (List.map.{u_1, 0} (α := R) (⇑SignType.sign : (a : R) → SignType) [] : List SignType))) :
            List SignType) -
        1 =
      List.length (α := SignType)
            (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
              (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
                (List.map.{u_1, 0} (α := R) (⇑SignType.sign : (a : R) → 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)
            (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
              ((SignType.sign : (a : R) → SignType) P.leadingCoeff ::
                HAppend.hAppend (α := List SignType) (β := List SignType)
                  (List.replicate (P.natDegree - P.eraseLead.degree.succ) ((SignType.sign : (a : R) → SignType) 0) :
                    List SignType)
                  (List.map (⇑SignType.sign : (a : R) → SignType) P.eraseLead.coeffList : List SignType))) :
          List SignType) -
      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) P.eraseLead.coeffList))) -
        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
have neg₁ : ∀ (c : R) (cs : List R) (h_eL : P.eraseLead.coeffList = c :: cs),
  List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
            (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
              ((SignType.sign : (a : R) → SignType) P.leadingCoeff ::
                HAppend.hAppend (α := List SignType) (β := List SignType)
                  (List.replicate (P.natDegree - P.eraseLead.degree.succ) ((SignType.sign : (a : R) → SignType) 0) :
                    List SignType)
                  (List.map (⇑SignType.sign : (a : R) → SignType) (c :: cs) : List SignType))) :
          List SignType) -
      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) (c :: 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: rcases h_eL : P.eraseLead.coeffList with _ | ⟨c, cs⟩