awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq (α := R)
    (((Matrix.reindex (finCongr ⋯) (finCongr ⋯) :
            Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R ≃
              Matrix (Fin 5) (Fin 5) R) :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 5) (Fin 5) R)
        f.sylvesterDeriv ⟨i, hi⟩ ⟨j, hj⟩ :
      R)
    (!![f.coeff 0, 0, 1 * f.coeff 1, 0, 0;
          f.coeff 1, f.coeff 0, 2 * f.coeff 2, 1 * f.coeff 1, 0;
          f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, 1 * f.coeff 1;
          f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2;
          0, 1, 0, 0, 3]
        ⟨i, hi⟩ ⟨j, hj⟩ :
      R)
have a : (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)
Tactic: simp only [sylvesterDeriv, hf, OfNat.ofNat_ne_zero, ↓reduceDIte, sylvester, Fin.addCases,
    Nat.add_one_sub_one, Fin.val_castLT, mem_Icc, Fin.val_fin_le, Fin.val_subNat, Fin.val_cast,
    tsub_le_iff_right, coeff_derivative, eq_rec_constant, dite_eq_ite, Nat.reduceMul, Nat.reduceSub,
    Nat.cast_ofNat, Matrix.reindex_apply, finCongr_symm, Matrix.submatrix_apply, finCongr_apply,
    Fin.cast_mk, Matrix.updateRow_apply, Fin.mk.injEq, Matrix.of_apply, Fin.mk_le_mk, one_mul,
    Matrix.cons_val', Matrix.cons_val_fin_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
i : ℕ
hi : i < 5
j : ℕ
hj : j < 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 hi' : i ∈ Finset.range 5
Tactic: have hi' : i ∈ Finset.range 5 := Finset.mem_range.mpr hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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
⊢ (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 hj' : j ∈ Finset.range 5
Tactic: have hj' : j ∈ Finset.range 5 := Finset.mem_range.mpr hj
-- 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
⊢ (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 : 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)
Tactic: fin_cases hi'
Cleared hypotheses: i, hi, hi'
-- 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)
⊢ (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 : 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)
Tactic: fin_cases hi'
Cleared hypotheses: i, hi, hi'
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
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)
have a : (if j < 2 then if j = 0 then f.coeff (0 - j) else 0
  else if j ≤ 2 then f.coeff (0 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (j - 2)) : R) 1 else 0) =
  ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩
Tactic: simp only [and_true, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, Fin.zero_eta,
      le_add_iff_nonneg_left, Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.cons_val,
      Nat.reduceAdd, Nat.reduceEqDiff, Nat.reduceLeDiff, nonpos_iff_eq_zero,
      OfNat.one_ne_ofNat, ↓reduceIte, zero_add, zero_le]
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 0 < 5
⊢ (if j < 2 then if j = 0 then f.coeff (0 - j) else 0
    else if j ≤ 2 then f.coeff (0 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩
have a : ∀ (hj : 0 < 5),
  (if 0 < 2 then if 0 = 0 then f.coeff (0 - 0) else 0
    else if 0 ≤ 2 then f.coeff (0 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (0 - 2)) : R) 1 else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨0, hj⟩
Tactic: fin_cases hj'
Cleared hypotheses: j, hj, hj'
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 0 < 5
a :
  ∀ (hj : 0 < 5),
    (if 0 < 2 then if 0 = 0 then f.coeff (0 - 0) else 0
      else if 0 ≤ 2 then f.coeff (0 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (0 - 2)) : R) 1 else 0) =
      ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨0, hj⟩
⊢ (if j < 2 then if j = 0 then f.coeff (0 - j) else 0
    else if j ≤ 2 then f.coeff (0 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩
have a₁ : ∀ (hj : 1 < 5),
  (if 1 < 2 then if 1 = 0 then f.coeff (0 - 1) else 0
    else if 1 ≤ 2 then f.coeff (0 - (1 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (1 - 2)) : R) 1 else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨1, hj⟩
Tactic: fin_cases hj'
Cleared hypotheses: j, hj, hj'
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 0 < 5
a :
  ∀ (hj : 0 < 5),
    (if 0 < 2 then if 0 = 0 then f.coeff (0 - 0) else 0
      else if 0 ≤ 2 then f.coeff (0 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (0 - 2)) : R) 1 else 0) =
      ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨0, hj⟩
a₁ :
  ∀ (hj : 1 < 5),
    (if 1 < 2 then if 1 = 0 then f.coeff (0 - 1) else 0
      else if 1 ≤ 2 then f.coeff (0 - (1 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (1 - 2)) : R) 1 else 0) =
      ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨1, hj⟩
⊢ (if j < 2 then if j = 0 then f.coeff (0 - j) else 0
    else if j ≤ 2 then f.coeff (0 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩
have a₂ : ∀ (hj : 2 < 5),
  (if 2 < 2 then if 2 = 0 then f.coeff (0 - 2) else 0
    else if 2 ≤ 2 then f.coeff (0 - (2 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (2 - 2)) : R) 1 else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨2, hj⟩
Tactic: fin_cases hj'
Cleared hypotheses: j, hj, hj'
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 0 < 5
a :
  ∀ (hj : 0 < 5),
    (if 0 < 2 then if 0 = 0 then f.coeff (0 - 0) else 0
      else if 0 ≤ 2 then f.coeff (0 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (0 - 2)) : R) 1 else 0) =
      ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨0, hj⟩
a₁ :
  ∀ (hj : 1 < 5),
    (if 1 < 2 then if 1 = 0 then f.coeff (0 - 1) else 0
      else if 1 ≤ 2 then f.coeff (0 - (1 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (1 - 2)) : R) 1 else 0) =
      ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨1, hj⟩
a₂ :
  ∀ (hj : 2 < 5),
    (if 2 < 2 then if 2 = 0 then f.coeff (0 - 2) else 0
      else if 2 ≤ 2 then f.coeff (0 - (2 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (2 - 2)) : R) 1 else 0) =
      ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨2, hj⟩
⊢ (if j < 2 then if j = 0 then f.coeff (0 - j) else 0
    else if j ≤ 2 then f.coeff (0 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩
have a₃ : ∀ (hj : 3 < 5),
  (if 3 < 2 then if 3 = 0 then f.coeff (0 - 3) else 0
    else if 3 ≤ 2 then f.coeff (0 - (3 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (3 - 2)) : R) 1 else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨3, hj⟩
Tactic: fin_cases hj'
Cleared hypotheses: j, hj, hj'
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 0 < 5
a :
  ∀ (hj : 0 < 5),
    (if 0 < 2 then if 0 = 0 then f.coeff (0 - 0) else 0
      else if 0 ≤ 2 then f.coeff (0 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (0 - 2)) : R) 1 else 0) =
      ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨0, hj⟩
a₁ :
  ∀ (hj : 1 < 5),
    (if 1 < 2 then if 1 = 0 then f.coeff (0 - 1) else 0
      else if 1 ≤ 2 then f.coeff (0 - (1 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (1 - 2)) : R) 1 else 0) =
      ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨1, hj⟩
a₂ :
  ∀ (hj : 2 < 5),
    (if 2 < 2 then if 2 = 0 then f.coeff (0 - 2) else 0
      else if 2 ≤ 2 then f.coeff (0 - (2 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (2 - 2)) : R) 1 else 0) =
      ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨2, hj⟩
a₃ :
  ∀ (hj : 3 < 5),
    (if 3 < 2 then if 3 = 0 then f.coeff (0 - 3) else 0
      else if 3 ≤ 2 then f.coeff (0 - (3 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (3 - 2)) : R) 1 else 0) =
      ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨3, hj⟩
⊢ (if j < 2 then if j = 0 then f.coeff (0 - j) else 0
    else if j ≤ 2 then f.coeff (0 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩
have a₄ : ∀ (hj : 4 < 5),
  (if 4 < 2 then if 4 = 0 then f.coeff (0 - 4) else 0
    else if 4 ≤ 2 then f.coeff (0 - (4 - 2) + 1) * HAdd.hAdd (α := R) (↑(0 - (4 - 2)) : R) 1 else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨4, hj⟩
Tactic: fin_cases hj'
Cleared hypotheses: j, hj, hj'
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
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)
have a : (if j < 2 then if j ≤ 1 then f.coeff (1 - j) else 0
  else if j ≤ 3 then f.coeff (1 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (j - 2)) : R) 1 else 0) =
  ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩
Tactic: simp only [and_true, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, Fin.zero_eta,
      le_add_iff_nonneg_left, Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.cons_val,
      Nat.reduceAdd, Nat.reduceEqDiff, Nat.reduceLeDiff, nonpos_iff_eq_zero,
      OfNat.one_ne_ofNat, ↓reduceIte, zero_add, zero_le]
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 1 < 5
⊢ (if j < 2 then if j ≤ 1 then f.coeff (1 - j) else 0
    else if j ≤ 3 then f.coeff (1 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩
have a : ∀ (hj : 0 < 5),
  (if 0 < 2 then if 0 ≤ 1 then f.coeff (1 - 0) else 0
    else if 0 ≤ 3 then f.coeff (1 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (0 - 2)) : R) 1 else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨0, hj⟩
Tactic: fin_cases hj'
Cleared hypotheses: j, hj, hj'
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 1 < 5
a :
  ∀ (hj : 0 < 5),
    (if 0 < 2 then if 0 ≤ 1 then f.coeff (1 - 0) else 0
      else if 0 ≤ 3 then f.coeff (1 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (0 - 2)) : R) 1 else 0) =
      ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨0, hj⟩
⊢ (if j < 2 then if j ≤ 1 then f.coeff (1 - j) else 0
    else if j ≤ 3 then f.coeff (1 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩
have a₁ : ∀ (hj : 1 < 5),
  (if 1 < 2 then if 1 ≤ 1 then f.coeff (1 - 1) else 0
    else if 1 ≤ 3 then f.coeff (1 - (1 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (1 - 2)) : R) 1 else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨1, hj⟩
Tactic: fin_cases hj'
Cleared hypotheses: j, hj, hj'
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 1 < 5
a :
  ∀ (hj : 0 < 5),
    (if 0 < 2 then if 0 ≤ 1 then f.coeff (1 - 0) else 0
      else if 0 ≤ 3 then f.coeff (1 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (0 - 2)) : R) 1 else 0) =
      ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨0, hj⟩
a₁ :
  ∀ (hj : 1 < 5),
    (if 1 < 2 then if 1 ≤ 1 then f.coeff (1 - 1) else 0
      else if 1 ≤ 3 then f.coeff (1 - (1 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (1 - 2)) : R) 1 else 0) =
      ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨1, hj⟩
⊢ (if j < 2 then if j ≤ 1 then f.coeff (1 - j) else 0
    else if j ≤ 3 then f.coeff (1 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩
have a₂ : ∀ (hj : 2 < 5),
  (if 2 < 2 then if 2 ≤ 1 then f.coeff (1 - 2) else 0
    else if 2 ≤ 3 then f.coeff (1 - (2 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (2 - 2)) : R) 1 else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨2, hj⟩
Tactic: fin_cases hj'
Cleared hypotheses: j, hj, hj'
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 1 < 5
a :
  ∀ (hj : 0 < 5),
    (if 0 < 2 then if 0 ≤ 1 then f.coeff (1 - 0) else 0
      else if 0 ≤ 3 then f.coeff (1 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (0 - 2)) : R) 1 else 0) =
      ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨0, hj⟩
a₁ :
  ∀ (hj : 1 < 5),
    (if 1 < 2 then if 1 ≤ 1 then f.coeff (1 - 1) else 0
      else if 1 ≤ 3 then f.coeff (1 - (1 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (1 - 2)) : R) 1 else 0) =
      ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨1, hj⟩
a₂ :
  ∀ (hj : 2 < 5),
    (if 2 < 2 then if 2 ≤ 1 then f.coeff (1 - 2) else 0
      else if 2 ≤ 3 then f.coeff (1 - (2 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (2 - 2)) : R) 1 else 0) =
      ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨2, hj⟩
⊢ (if j < 2 then if j ≤ 1 then f.coeff (1 - j) else 0
    else if j ≤ 3 then f.coeff (1 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩
have a₃ : ∀ (hj : 3 < 5),
  (if 3 < 2 then if 3 ≤ 1 then f.coeff (1 - 3) else 0
    else if 3 ≤ 3 then f.coeff (1 - (3 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (3 - 2)) : R) 1 else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨3, hj⟩
Tactic: fin_cases hj'
Cleared hypotheses: j, hj, hj'
-- 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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 1 < 5
a :
  ∀ (hj : 0 < 5),
    (if 0 < 2 then if 0 ≤ 1 then f.coeff (1 - 0) else 0
      else if 0 ≤ 3 then f.coeff (1 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (0 - 2)) : R) 1 else 0) =
      ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨0, hj⟩
a₁ :
  ∀ (hj : 1 < 5),
    (if 1 < 2 then if 1 ≤ 1 then f.coeff (1 - 1) else 0
      else if 1 ≤ 3 then f.coeff (1 - (1 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (1 - 2)) : R) 1 else 0) =
      ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨1, hj⟩
a₂ :
  ∀ (hj : 2 < 5),
    (if 2 < 2 then if 2 ≤ 1 then f.coeff (1 - 2) else 0
      else if 2 ≤ 3 then f.coeff (1 - (2 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (2 - 2)) : R) 1 else 0) =
      ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨2, hj⟩
a₃ :
  ∀ (hj : 3 < 5),
    (if 3 < 2 then if 3 ≤ 1 then f.coeff (1 - 3) else 0
      else if 3 ≤ 3 then f.coeff (1 - (3 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (3 - 2)) : R) 1 else 0) =
      ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨3, hj⟩
⊢ (if j < 2 then if j ≤ 1 then f.coeff (1 - j) else 0
    else if j ≤ 3 then f.coeff (1 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩
have a₄ : ∀ (hj : 4 < 5),
  (if 4 < 2 then if 4 ≤ 1 then f.coeff (1 - 4) else 0
    else if 4 ≤ 3 then f.coeff (1 - (4 - 2) + 1) * HAdd.hAdd (α := R) (↑(1 - (4 - 2)) : R) 1 else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨4, hj⟩
Tactic: fin_cases hj'
Cleared hypotheses: j, hj, hj'