awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ (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 < f.natDegree - 1 → ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2) → f.coeff f.natDegree = 0
Tactic: split_ifs
-- 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
⊢ (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 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
Tactic: split_ifs
-- 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
⊢ (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 < 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
Tactic: split_ifs
-- 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
⊢ (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 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)
Tactic: split_ifs
-- 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)
⊢ (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 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2) → f.coeff f.natDegree * (↑f.natDegree : R) = 0
Tactic: split_ifs
-- 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
⊢ (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 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
Tactic: split_ifs
-- 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
⊢ (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) →
        f.coeff f.natDegree * (↑f.natDegree : R) = 0
Tactic: split_ifs
-- 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
h : j = f.natDegree - 2
h_1 : j < f.natDegree - 1
h_2 : ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2)
⊢ f.coeff f.natDegree = 0
have neg : f.coeff 1 = 0
Tactic: rw [show f.natDegree = 1 by lia]
-- 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
h : j = f.natDegree - 2
h_1 : j < f.natDegree - 1
h_2 : ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2)
⊢ f.coeff f.natDegree = 0
have neg : f.coeff 1 = 0
Tactic: on_goal 2 => rw [show f.natDegree = 1 by lia]
-- 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
h : j = f.natDegree - 2
h_1 : ¬j < f.natDegree - 1
h_2 : 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
have pos : f.coeff 1 =
  f.coeff (HMul.hMul (α := ℕ) 2 1 - 2 - (j - HSub.hSub (α := ℕ) 1 1) + 1) *
    (↑(HMul.hMul (α := ℕ) 2 1 - 2 - (j - HSub.hSub (α := ℕ) 1 1) + 1) : R)
Tactic: rw [← Nat.cast_one (R := R), ← Nat.cast_add, show f.natDegree = 1 by lia]
-- 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
h : ¬j = f.natDegree - 2
h_1 : j = 2 * f.natDegree - 2
h_2 : ¬j < f.natDegree - 1
h_3 : 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
have pos : f.coeff f.natDegree * (↑f.natDegree : R) =
  f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
    (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) : R)
Tactic: rw [← Nat.cast_one (R := R), ← Nat.cast_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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
h : ¬j = f.natDegree - 2
h_1 : j = 2 * f.natDegree - 2
h_2 : ¬j < f.natDegree - 1
h_3 : 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) *
      (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) : R)
have this : 2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1 = f.natDegree
Tactic: have : 2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1 = f.natDegree := by grind
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
⊢ f.resultant g m n = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
have rw : (↑(↑(∏ i : Fin (n + m),
              ∏ j ∈ Finset.Ioi i,
                if
                    LT.lt (α := Fin (n + m))
                      ((Equiv.trans
                              (Equiv.trans (Equiv.symm finSumFinEquiv)
                                (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                              (Equiv.symm (finCongr sorry)) :
                            (a : Fin (n + m)) → Fin (n + m))
                          i :
                        Fin (n + m))
                      ((Equiv.trans
                              (Equiv.trans (Equiv.symm finSumFinEquiv)
                                (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                              (Equiv.symm (finCongr sorry)) :
                            (a : Fin (n + m)) → Fin (n + m))
                          j :
                        Fin (n + m)) then
                  1
                else -1) :
          ℤ) :
      R) *
    (g.sylvester f n m).det =
  HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
Tactic: rw [resultant, resultant, sylvester_comm, Matrix.det_reindex, Equiv.Perm.sign_eq_prod_prod_Ioi]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
⊢ (↑(↑(∏ i : Fin (n + m),
                ∏ j ∈ Finset.Ioi i,
                  if
                      LT.lt (α := Fin (n + m))
                        ((Equiv.trans
                                (Equiv.trans (Equiv.symm finSumFinEquiv)
                                  (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                                (Equiv.symm (finCongr ⋯)) :
                              (a : Fin (n + m)) → Fin (n + m))
                            i :
                          Fin (n + m))
                        ((Equiv.trans
                                (Equiv.trans (Equiv.symm finSumFinEquiv)
                                  (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                                (Equiv.symm (finCongr ⋯)) :
                              (a : Fin (n + m)) → Fin (n + m))
                            j :
                          Fin (n + m)) then
                    1
                  else -1) :
            ℤ) :
        R) *
      (g.sylvester f n m).det =
    HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
have e_a : (↑(↑(∏ i : Fin (n + m),
            ∏ j ∈ Finset.Ioi i,
              if
                  LT.lt (α := Fin (n + m))
                    ((Equiv.trans
                            (Equiv.trans (Equiv.symm finSumFinEquiv)
                              (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                            (Equiv.symm (finCongr sorry)) :
                          (a : Fin (n + m)) → Fin (n + m))
                        i :
                      Fin (n + m))
                    ((Equiv.trans
                            (Equiv.trans (Equiv.symm finSumFinEquiv)
                              (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                            (Equiv.symm (finCongr sorry)) :
                          (a : Fin (n + m)) → Fin (n + m))
                        j :
                      Fin (n + m)) then
                1
              else -1) :
        ℤ) :
    R) =
  HPow.hPow (α := R) (-1) (m * n)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
⊢ (↑(↑(∏ i : Fin (n + m),
              ∏ j ∈ Finset.Ioi i,
                if
                    LT.lt (α := Fin (n + m))
                      ((Equiv.trans
                              (Equiv.trans (Equiv.symm finSumFinEquiv)
                                (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                              (Equiv.symm (finCongr ⋯)) :
                            (a : Fin (n + m)) → Fin (n + m))
                          i :
                        Fin (n + m))
                      ((Equiv.trans
                              (Equiv.trans (Equiv.symm finSumFinEquiv)
                                (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                              (Equiv.symm (finCongr ⋯)) :
                            (a : Fin (n + m)) → Fin (n + m))
                          j :
                        Fin (n + m)) then
                  1
                else -1) :
          ℤ) :
      R) =
    HPow.hPow (α := R) (-1) (m * n)
have e_a : (↑(↑(∏ i : Fin (n + m),
            ∏ j ∈ Finset.Ioi i,
              if
                  Fin.cast sorry
                      ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                        (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) i))) <
                    Fin.cast sorry
                      ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                        (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) j))) then
                1
              else -1) :
        ℤ) :
    R) =
  HPow.hPow (α := R) (-1) (m * n)
Tactic: dsimp