-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
pos :
  j = f.natDegree - 2 →
    j < f.natDegree - 1 →
      j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2 →
        f.coeff f.natDegree = f.coeff (2 * f.natDegree - 2 - j)
neg :
  j = f.natDegree - 2 →
    j < f.natDegree - 1 → ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2) → f.coeff f.natDegree = 0
pos₁ :
  j = f.natDegree - 2 →
    ¬j < f.natDegree - 1 →
      j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2 →
        f.coeff f.natDegree =
          f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
            HAdd.hAdd (α := R) (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) : R) 1
neg₁ :
  j = f.natDegree - 2 →
    ¬j < f.natDegree - 1 →
      ¬(j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2) →
        f.coeff f.natDegree = 0
pos₂ :
  ¬j = f.natDegree - 2 →
    j = 2 * f.natDegree - 2 →
      j < f.natDegree - 1 →
        j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2 →
          f.coeff f.natDegree * (↑f.natDegree : R) = f.coeff (2 * f.natDegree - 2 - j)
neg₂ :
  ¬j = f.natDegree - 2 →
    j = 2 * f.natDegree - 2 →
      j < f.natDegree - 1 →
        ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2) →
          f.coeff f.natDegree * (↑f.natDegree : R) = 0
pos₃ :
  ¬j = f.natDegree - 2 →
    j = 2 * f.natDegree - 2 →
      ¬j < f.natDegree - 1 →
        j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2 →
          f.coeff f.natDegree * (↑f.natDegree : R) =
            f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
              HAdd.hAdd (α := R) (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) : R) 1
neg₃ :
  ¬j = f.natDegree - 2 →
    j = 2 * f.natDegree - 2 →
      ¬j < f.natDegree - 1 →
        ¬(j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧
              2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2) →
          f.coeff f.natDegree * (↑f.natDegree : R) = 0
pos₄ :
  ¬j = f.natDegree - 2 →
    ¬j = 2 * f.natDegree - 2 →
      j < f.natDegree - 1 →
        j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2 → 0 = f.coeff (2 * f.natDegree - 2 - j)
neg₄ :
  ¬j = f.natDegree - 2 →
    ¬j = 2 * f.natDegree - 2 →
      j < f.natDegree - 1 →
        ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2) → Eq.{u_1 + 1} (α := R) 0 0
pos₅ :
  ¬j = f.natDegree - 2 →
    ¬j = 2 * f.natDegree - 2 →
      ¬j < f.natDegree - 1 →
        j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2 →
          0 =
            f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
              HAdd.hAdd (α := R) (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) : R) 1
⊢ (if j = f.natDegree - 2 then f.coeff f.natDegree
    else if j = 2 * f.natDegree - 2 then f.coeff f.natDegree * (↑f.natDegree : R) else 0) =
    if j < f.natDegree - 1 then
      if j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2 then f.coeff (2 * f.natDegree - 2 - j) else 0
    else
      if
          j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧
            2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2 then
        f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
          HAdd.hAdd (α := R) (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) : R) 1
      else 0
have neg₅ : ¬j = f.natDegree - 2 →
  ¬j = 2 * f.natDegree - 2 →
    ¬j < f.natDegree - 1 →
      ¬(j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2) →
        Eq.{u_1 + 1} (α := R) 0 0
Tactic: split_ifs