awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
i : ℕ
hi : i < 5
j : ℕ
hj : j < 5
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)
⊢ 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)

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]

Premises used: Polynomial.coeff_derivative, Nat.cast_ofNat, Fin.mk_le_mk, Nat.add_one_sub_one, Fin.mk.injEq, finCongr_apply, OfNat.ofNat_ne_zero, Matrix.reindex_apply, reduceDIte, Matrix.cons_val_fin_one, Matrix.of_apply, tsub_le_iff_right, Polynomial.sylvester, Fin.val_subNat, Set.mem_Icc, finCongr_symm, Fin.val_cast, Fin.cast_mk, Fin.val_castLT, eq_rec_constant, Matrix.submatrix_apply, dite_eq_ite, Nat.reduceSub, Polynomial.sylvesterDeriv, one_mul, Matrix.updateRow_apply, Nat.reduceMul, Fin.val_fin_le, Matrix.cons_val'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
i : ℕ
hi : i < 5
j : ℕ
hj : j < 5
⊢ i ∈ Finset.range 5

Tactic:
have hi' : i ∈ Finset.range 5 := Finset.mem_range.mpr hi
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
⊢ j ∈ Finset.range 5

Tactic:
have hj' : j ∈ Finset.range 5 := Finset.mem_range.mpr hj
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 :
  (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⟩
⊢ (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:
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]

Premises used: zero_le, Fin.mk_one, and_true, OfNat.one_ne_ofNat, Nat.reduceLeDiff, Matrix.cons_val_one, Matrix.cons_val_zero, Nat.reduceAdd, Fin.reduceFinMk, zero_add, Fin.zero_eta, Fin.isValue, Nat.reduceEqDiff, reduceIte, Matrix.cons_val, le_add_iff_nonneg_left, nonpos_iff_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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⟩
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⟩
⊢ (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:
fin_cases hj'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 0 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 1 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 2 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 3 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 4 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 :
  (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⟩
⊢ (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:
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]

Premises used: zero_le, Fin.mk_one, and_true, OfNat.one_ne_ofNat, Nat.reduceLeDiff, Matrix.cons_val_one, Matrix.cons_val_zero, Nat.reduceAdd, Fin.reduceFinMk, zero_add, Fin.zero_eta, Fin.isValue, Nat.reduceEqDiff, reduceIte, Matrix.cons_val, le_add_iff_nonneg_left, nonpos_iff_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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⟩
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⟩
⊢ (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:
fin_cases hj'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 0 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 1 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 2 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 3 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 4 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : 2 < 5
a :
  (if j < 2 then if j ≤ 2 then f.coeff (2 - j) else 0
    else if j ≤ 4 then f.coeff (2 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(2 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩
⊢ (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:
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]

Premises used: zero_le, Fin.mk_one, and_true, OfNat.one_ne_ofNat, Nat.reduceLeDiff, Matrix.cons_val_one, Matrix.cons_val_zero, Nat.reduceAdd, Fin.reduceFinMk, zero_add, Fin.zero_eta, Fin.isValue, Nat.reduceEqDiff, reduceIte, Matrix.cons_val, le_add_iff_nonneg_left, nonpos_iff_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : 2 < 5
a :
  ∀ (hj : 0 < 5),
    (if 0 < 2 then if 0 ≤ 2 then f.coeff (2 - 0) else 0
      else if 0 ≤ 4 then f.coeff (2 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(2 - (0 - 2)) : R) 1 else 0) =
      ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨0, hj⟩
a₁ :
  ∀ (hj : 1 < 5),
    (if 1 < 2 then if 1 ≤ 2 then f.coeff (2 - 1) else 0
      else if 1 ≤ 4 then f.coeff (2 - (1 - 2) + 1) * HAdd.hAdd (α := R) (↑(2 - (1 - 2)) : R) 1 else 0) =
      ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨1, hj⟩
a₂ :
  ∀ (hj : 2 < 5),
    (if 2 < 2 then if 2 ≤ 2 then f.coeff (2 - 2) else 0
      else if 2 ≤ 4 then f.coeff (2 - (2 - 2) + 1) * HAdd.hAdd (α := R) (↑(2 - (2 - 2)) : R) 1 else 0) =
      ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨2, hj⟩
a₃ :
  ∀ (hj : 3 < 5),
    (if 3 < 2 then if 3 ≤ 2 then f.coeff (2 - 3) else 0
      else if 3 ≤ 4 then f.coeff (2 - (3 - 2) + 1) * HAdd.hAdd (α := R) (↑(2 - (3 - 2)) : R) 1 else 0) =
      ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨3, hj⟩
a₄ :
  ∀ (hj : 4 < 5),
    (if 4 < 2 then if 4 ≤ 2 then f.coeff (2 - 4) else 0
      else if 4 ≤ 4 then f.coeff (2 - (4 - 2) + 1) * HAdd.hAdd (α := R) (↑(2 - (4 - 2)) : R) 1 else 0) =
      ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨4, hj⟩
⊢ (if j < 2 then if j ≤ 2 then f.coeff (2 - j) else 0
    else if j ≤ 4 then f.coeff (2 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(2 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩

Tactic:
fin_cases hj'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 0 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 1 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 2 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 3 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 4 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : 3 < 5
a :
  (if j < 2 then if j ≤ 3 then f.coeff (3 - j) else 0
    else if j ≤ 5 ∧ 1 ≤ j - 2 then f.coeff (3 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(3 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩
⊢ (if 3 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 3 ∧ 3 ≤ j + 3 then f.coeff (3 - j) else 0
      else
        if j ≤ 3 + 2 ∧ 3 ≤ j - 2 + 2 then f.coeff (3 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(3 - (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)
      (⟨3, hi⟩ : Fin 5)

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]

Premises used: zero_le, Fin.mk_one, and_true, OfNat.one_ne_ofNat, Nat.reduceLeDiff, Matrix.cons_val_one, Matrix.cons_val_zero, Nat.reduceAdd, Fin.reduceFinMk, zero_add, Fin.zero_eta, Fin.isValue, Nat.reduceEqDiff, reduceIte, Matrix.cons_val, le_add_iff_nonneg_left, nonpos_iff_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : 3 < 5
a :
  ∀ (hj : 0 < 5),
    (if 0 < 2 then if 0 ≤ 3 then f.coeff (3 - 0) else 0
      else if 0 ≤ 5 ∧ 1 ≤ 0 - 2 then f.coeff (3 - (0 - 2) + 1) * HAdd.hAdd (α := R) (↑(3 - (0 - 2)) : R) 1 else 0) =
      ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨0, hj⟩
a₁ :
  ∀ (hj : 1 < 5),
    (if 1 < 2 then if 1 ≤ 3 then f.coeff (3 - 1) else 0
      else if 1 ≤ 5 ∧ 1 ≤ 1 - 2 then f.coeff (3 - (1 - 2) + 1) * HAdd.hAdd (α := R) (↑(3 - (1 - 2)) : R) 1 else 0) =
      ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨1, hj⟩
a₂ :
  ∀ (hj : 2 < 5),
    (if 2 < 2 then if 2 ≤ 3 then f.coeff (3 - 2) else 0
      else if 2 ≤ 5 ∧ 1 ≤ 2 - 2 then f.coeff (3 - (2 - 2) + 1) * HAdd.hAdd (α := R) (↑(3 - (2 - 2)) : R) 1 else 0) =
      ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨2, hj⟩
a₃ :
  ∀ (hj : 3 < 5),
    (if 3 < 2 then if 3 ≤ 3 then f.coeff (3 - 3) else 0
      else if 3 ≤ 5 ∧ 1 ≤ 3 - 2 then f.coeff (3 - (3 - 2) + 1) * HAdd.hAdd (α := R) (↑(3 - (3 - 2)) : R) 1 else 0) =
      ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨3, hj⟩
a₄ :
  ∀ (hj : 4 < 5),
    (if 4 < 2 then if 4 ≤ 3 then f.coeff (3 - 4) else 0
      else if 4 ≤ 5 ∧ 1 ≤ 4 - 2 then f.coeff (3 - (4 - 2) + 1) * HAdd.hAdd (α := R) (↑(3 - (4 - 2)) : R) 1 else 0) =
      ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨4, hj⟩
⊢ (if j < 2 then if j ≤ 3 then f.coeff (3 - j) else 0
    else if j ≤ 5 ∧ 1 ≤ j - 2 then f.coeff (3 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(3 - (j - 2)) : R) 1 else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩

Tactic:
fin_cases hj'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 0 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 1 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 2 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 3 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 4 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : 4 < 5
a : Eq.{u_1 + 1} (α := R) (if j = 1 then 1 else if j = 4 then 3 else 0) (![0, 1, 0, 0, 3] (⟨j, hj⟩ : Fin 5))
⊢ (if 4 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 4 ∧ 4 ≤ j + 3 then f.coeff (4 - j) else 0
      else
        if j ≤ 4 + 2 ∧ 4 ≤ j - 2 + 2 then f.coeff (4 - (j - 2) + 1) * HAdd.hAdd (α := R) (↑(4 - (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)
      (⟨4, hi⟩ : Fin 5)

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]

Premises used: zero_le, Fin.mk_one, and_true, OfNat.one_ne_ofNat, Nat.reduceLeDiff, Matrix.cons_val_one, Matrix.cons_val_zero, Nat.reduceAdd, Fin.reduceFinMk, zero_add, Fin.zero_eta, Fin.isValue, Nat.reduceEqDiff, reduceIte, Matrix.cons_val, le_add_iff_nonneg_left, nonpos_iff_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : 4 < 5
a :
  ∀ (hj : 0 < 5),
    Eq.{u_1 + 1} (α := R) (if 0 = 1 then 1 else if 0 = 4 then 3 else 0) (![0, 1, 0, 0, 3] (⟨0, hj⟩ : Fin 5))
a₁ :
  ∀ (hj : 1 < 5),
    Eq.{u_1 + 1} (α := R) (if 1 = 1 then 1 else if 1 = 4 then 3 else 0) (![0, 1, 0, 0, 3] (⟨1, hj⟩ : Fin 5))
a₂ :
  ∀ (hj : 2 < 5),
    Eq.{u_1 + 1} (α := R) (if 2 = 1 then 1 else if 2 = 4 then 3 else 0) (![0, 1, 0, 0, 3] (⟨2, hj⟩ : Fin 5))
a₃ :
  ∀ (hj : 3 < 5),
    Eq.{u_1 + 1} (α := R) (if 3 = 1 then 1 else if 3 = 4 then 3 else 0) (![0, 1, 0, 0, 3] (⟨3, hj⟩ : Fin 5))
a₄ :
  ∀ (hj : 4 < 5),
    Eq.{u_1 + 1} (α := R) (if 4 = 1 then 1 else if 4 = 4 then 3 else 0) (![0, 1, 0, 0, 3] (⟨4, hj⟩ : Fin 5))
⊢ Eq.{u_1 + 1} (α := R) (if j = 1 then 1 else if j = 4 then 3 else 0) (![0, 1, 0, 0, 3] (⟨j, hj⟩ : Fin 5))

Tactic:
fin_cases hj'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 0 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 1 < 5
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
norm_num