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
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
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)
have 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⟩
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 : 2 < 5
⊢ (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⟩
have 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⟩
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 : 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⟩
⊢ (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⟩
have 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⟩
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 : 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⟩
⊢ (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⟩
have 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⟩
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 : 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⟩
⊢ (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⟩
have 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⟩
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 : 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⟩
⊢ (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⟩
have 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⟩
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 : 3 < 5
⊢ (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)
have 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⟩
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 : 3 < 5
⊢ (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⟩
have 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⟩
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 : 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⟩
⊢ (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⟩
have 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⟩
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 : 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⟩
⊢ (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⟩
have 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⟩
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 : 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⟩
⊢ (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⟩
have 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⟩
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 : 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⟩
⊢ (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⟩
have 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⟩
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 : 4 < 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)
have 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))
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 : 4 < 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))
have 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))
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 : 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))
⊢ 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))
have 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))
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 : 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))
⊢ 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))
have 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))
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 : 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))
⊢ 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))
have 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))
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 : 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))
⊢ 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))
have 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))
Tactic: fin_cases hj'
Cleared hypotheses: j, hj, hj'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.degree = 3
⊢ f.discr =
    HPow.hPow (β := ℕ) (f.coeff 2) 2 * HPow.hPow (β := ℕ) (f.coeff 1) 2 -
            4 * f.coeff 3 * HPow.hPow (β := ℕ) (f.coeff 1) 3 -
          4 * HPow.hPow (β := ℕ) (f.coeff 2) 3 * f.coeff 0 -
        27 * HPow.hPow (β := ℕ) (f.coeff 3) 2 * HPow.hPow (β := ℕ) (f.coeff 0) 2 +
      18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0
have hf₁ : f.natDegree = 3
Tactic: apply natDegree_eq_of_degree_eq_some at hf
Cleared hypotheses: hf
-- 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
⊢ f.natDegree - 1 + f.natDegree = 5
have rw : 3 - 1 + 3 = 5
Tactic: rw [hf]
-- 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
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 5 := finCongr ⋯
⊢ f.discr =
    HPow.hPow (β := ℕ) (f.coeff 2) 2 * HPow.hPow (β := ℕ) (f.coeff 1) 2 -
            4 * f.coeff 3 * HPow.hPow (β := ℕ) (f.coeff 1) 3 -
          4 * HPow.hPow (β := ℕ) (f.coeff 2) 3 * f.coeff 0 -
        27 * HPow.hPow (β := ℕ) (f.coeff 3) 2 * HPow.hPow (β := ℕ) (f.coeff 0) 2 +
      18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0
have rw : Matrix.det (n := Fin 5)
      !![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] *
    HPow.hPow (α := R) (-1) (f.natDegree * (f.natDegree - 1) / 2) =
  HPow.hPow (β := ℕ) (f.coeff 2) 2 * HPow.hPow (β := ℕ) (f.coeff 1) 2 -
          4 * f.coeff 3 * HPow.hPow (β := ℕ) (f.coeff 1) 3 -
        4 * HPow.hPow (β := ℕ) (f.coeff 2) 3 * f.coeff 0 -
      27 * HPow.hPow (β := ℕ) (f.coeff 3) 2 * HPow.hPow (β := ℕ) (f.coeff 0) 2 +
    18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0
Tactic: rw [discr, ← Matrix.det_reindex_self e, sylvesterDeriv_of_natDegree_eq_three hf]