-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
i : ℕ
hi : i < 5
j : ℕ
hj : j < 5
hi' : i ∈ Finset.range 5
hj' : j ∈ Finset.range 5
a :
  ∀ (hi : 0 < 5),
    (if 0 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
      else
        if j < 2 then if j ≤ 0 ∧ 0 ≤ j + 3 then f.coeff (0 - j) else 0
        else
          if j ≤ 0 + 2 ∧ 0 ≤ j - 2 + 2 then f.coeff (0 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (j - 2)) : R) 1
          else 0) =
      Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
        (fun (i : Fin 4) ↦
          Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
            (fun (i : Fin 3) ↦
              Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
                (fun (i : Fin 2) ↦
                  Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                    (fun (i : Fin 1) ↦ ![0, 1, 0, 0, 3] (⟨j, hj⟩ : Fin 5)) i)
                i)
            i)
        (⟨0, hi⟩ : Fin 5)
a₁ :
  ∀ (hi : 1 < 5),
    (if 1 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
      else
        if j < 2 then if j ≤ 1 ∧ 1 ≤ j + 3 then f.coeff (1 - j) else 0
        else
          if j ≤ 1 + 2 ∧ 1 ≤ j - 2 + 2 then f.coeff (1 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (j - 2)) : R) 1
          else 0) =
      Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
        (fun (i : Fin 4) ↦
          Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
            (fun (i : Fin 3) ↦
              Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
                (fun (i : Fin 2) ↦
                  Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                    (fun (i : Fin 1) ↦ ![0, 1, 0, 0, 3] (⟨j, hj⟩ : Fin 5)) i)
                i)
            i)
        (⟨1, hi⟩ : Fin 5)
⊢ (if i = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ i ∧ i ≤ j + 3 then f.coeff (i - j) else 0
      else
        if j ≤ i + 2 ∧ i ≤ j - 2 + 2 then f.coeff (i - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(i - (j - 2)) : R) 1
        else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun (i : Fin 4) ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun (i : Fin 3) ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun (i : Fin 2) ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun (i : Fin 1) ↦ ![0, 1, 0, 0, 3] (⟨j, hj⟩ : Fin 5)) i)
              i)
          i)
      (⟨i, hi⟩ : Fin 5)
have a₂ : ∀ (hi : 2 < 5),
  (if 2 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 2 ∧ 2 ≤ j + 3 then f.coeff (2 - j) else 0
      else
        if j ≤ 2 + 2 ∧ 2 ≤ j - 2 + 2 then f.coeff (2 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(2 - (j - 2)) : R) 1
        else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun (i : Fin 4) ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun (i : Fin 3) ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun (i : Fin 2) ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun (i : Fin 1) ↦ ![0, 1, 0, 0, 3] (⟨j, hj⟩ : Fin 5)) i)
              i)
          i)
      (⟨2, hi⟩ : Fin 5)
Tactic: fin_cases hi'
Cleared hypotheses: i, hi, hi'