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 g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
this : ∀ (i : ℕ) (hi : i ≤ m), (M i).det = r ^ i * M₂.det
⊢ f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n = M m
have e_M : ∀ (i j : Fin (m + n)), f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n i j = M m i j
Tactic: ext i j
-- 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 : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
this : ∀ (i : ℕ) (hi : i ≤ m), (M i).det = r ^ i * M₂.det
i j : Fin (m + n)
⊢ f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n i j = M m i j
have e_M : ∀ (i_1 : Fin m),
  f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n i (Fin.castAdd n i_1) =
    M m i (Fin.castAdd n i_1)
Tactic: induction j using Fin.addCases
Cleared hypotheses: j
-- 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 : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
this : ∀ (i : ℕ) (hi : i ≤ m), (M i).det = r ^ i * M₂.det
i j : Fin (m + n)
e_M :
  ∀ (i_1 : Fin m),
    f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n i (Fin.castAdd n i_1) =
      M m i (Fin.castAdd n i_1)
⊢ f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n i j = M m i j
have e_M₁ : ∀ (i_1 : Fin n),
  f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n i (Fin.natAdd m i_1) =
    M m i (Fin.natAdd m i_1)
Tactic: induction j using Fin.addCases
Cleared hypotheses: j
-- 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 : ℕ
r : R
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f).resultant g m n = r ^ n * f.resultant g m n
have rw : HPow.hPow (α := R) (-1) (m * n) * g.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) n m =
  r ^ n * f.resultant g m n
Tactic: rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]
-- 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 : ℕ
r : R
rw :
  HPow.hPow (α := R) (-1) (m * n) * g.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) n m =
    r ^ n * f.resultant g m n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f).resultant g m n = r ^ n * f.resultant g m n
have rw₁ : HPow.hPow (α := R) (-1) (m * n) * (r ^ n * g.resultant f n m) = r ^ n * f.resultant g m n
Tactic: rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]
-- 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 : ℕ
r : R
rw :
  HPow.hPow (α := R) (-1) (m * n) * g.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) n m =
    r ^ n * f.resultant g m n
rw₁ : HPow.hPow (α := R) (-1) (m * n) * (r ^ n * g.resultant f n m) = r ^ n * f.resultant g m n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f).resultant g m n = r ^ n * f.resultant g m n
have rw₂ : HPow.hPow (α := R) (-1) (m * n) * (r ^ n * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
  r ^ n * f.resultant g m n
Tactic: rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]
-- 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 : ℕ
r : R
rw :
  HPow.hPow (α := R) (-1) (m * n) * g.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) n m =
    r ^ n * f.resultant g m n
rw₁ : HPow.hPow (α := R) (-1) (m * n) * (r ^ n * g.resultant f n m) = r ^ n * f.resultant g m n
rw₂ :
  HPow.hPow (α := R) (-1) (m * n) * (r ^ n * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f).resultant g m n = r ^ n * f.resultant g m n
have rw₃ : r ^ n * (HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
  r ^ n * f.resultant g m n
Tactic: rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]
-- 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 : ℕ
r : R
rw :
  HPow.hPow (α := R) (-1) (m * n) * g.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) n m =
    r ^ n * f.resultant g m n
rw₁ : HPow.hPow (α := R) (-1) (m * n) * (r ^ n * g.resultant f n m) = r ^ n * f.resultant g m n
rw₂ :
  HPow.hPow (α := R) (-1) (m * n) * (r ^ n * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₃ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f).resultant g m n = r ^ n * f.resultant g m n
have rw₄ : r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n) =
  r ^ n * f.resultant g m n
Tactic: rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]
-- 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 : ℕ
r : R
rw :
  HPow.hPow (α := R) (-1) (m * n) * g.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) n m =
    r ^ n * f.resultant g m n
rw₁ : HPow.hPow (α := R) (-1) (m * n) * (r ^ n * g.resultant f n m) = r ^ n * f.resultant g m n
rw₂ :
  HPow.hPow (α := R) (-1) (m * n) * (r ^ n * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₃ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₄ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n) =
    r ^ n * f.resultant g m n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f).resultant g m n = r ^ n * f.resultant g m n
have rw₅ : r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (m * n) * f.resultant g m n) =
  r ^ n * f.resultant g m n
Tactic: rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]
-- 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 : ℕ
r : R
rw :
  HPow.hPow (α := R) (-1) (m * n) * g.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) n m =
    r ^ n * f.resultant g m n
rw₁ : HPow.hPow (α := R) (-1) (m * n) * (r ^ n * g.resultant f n m) = r ^ n * f.resultant g m n
rw₂ :
  HPow.hPow (α := R) (-1) (m * n) * (r ^ n * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₃ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₄ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n) =
    r ^ n * f.resultant g m n
rw₅ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (m * n) * f.resultant g m n) =
    r ^ n * f.resultant g m n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f).resultant g m n = r ^ n * f.resultant g m n
have rw₆ : r ^ n * (HMul.hMul (α := R) (-1) (-1) ^ (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
Tactic: rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]
-- 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 : ℕ
r : R
rw :
  HPow.hPow (α := R) (-1) (m * n) * g.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) n m =
    r ^ n * f.resultant g m n
rw₁ : HPow.hPow (α := R) (-1) (m * n) * (r ^ n * g.resultant f n m) = r ^ n * f.resultant g m n
rw₂ :
  HPow.hPow (α := R) (-1) (m * n) * (r ^ n * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₃ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₄ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n) =
    r ^ n * f.resultant g m n
rw₅ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (m * n) * f.resultant g m n) =
    r ^ n * f.resultant g m n
rw₆ : r ^ n * (HMul.hMul (α := R) (-1) (-1) ^ (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f).resultant g m n = r ^ n * f.resultant g m n
have rw₇ : r ^ n * (HPow.hPow (α := R) (- -1) (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
Tactic: rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]
-- 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 : ℕ
r : R
rw :
  HPow.hPow (α := R) (-1) (m * n) * g.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) n m =
    r ^ n * f.resultant g m n
rw₁ : HPow.hPow (α := R) (-1) (m * n) * (r ^ n * g.resultant f n m) = r ^ n * f.resultant g m n
rw₂ :
  HPow.hPow (α := R) (-1) (m * n) * (r ^ n * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₃ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₄ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n) =
    r ^ n * f.resultant g m n
rw₅ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (m * n) * f.resultant g m n) =
    r ^ n * f.resultant g m n
rw₆ : r ^ n * (HMul.hMul (α := R) (-1) (-1) ^ (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
rw₇ : r ^ n * (HPow.hPow (α := R) (- -1) (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f).resultant g m n = r ^ n * f.resultant g m n
have rw₈ : r ^ n * (HPow.hPow (α := R) 1 (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
Tactic: rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]
-- 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 : ℕ
r : R
rw :
  HPow.hPow (α := R) (-1) (m * n) * g.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) n m =
    r ^ n * f.resultant g m n
rw₁ : HPow.hPow (α := R) (-1) (m * n) * (r ^ n * g.resultant f n m) = r ^ n * f.resultant g m n
rw₂ :
  HPow.hPow (α := R) (-1) (m * n) * (r ^ n * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₃ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₄ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n) =
    r ^ n * f.resultant g m n
rw₅ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (m * n) * f.resultant g m n) =
    r ^ n * f.resultant g m n
rw₆ : r ^ n * (HMul.hMul (α := R) (-1) (-1) ^ (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
rw₇ : r ^ n * (HPow.hPow (α := R) (- -1) (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
rw₈ : r ^ n * (HPow.hPow (α := R) 1 (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f).resultant g m n = r ^ n * f.resultant g m n
have rw₉ : r ^ n * (1 * f.resultant g m n) = r ^ n * f.resultant g m n
Tactic: rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]
-- 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 : ℕ
r : R
rw :
  HPow.hPow (α := R) (-1) (m * n) * g.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) n m =
    r ^ n * f.resultant g m n
rw₁ : HPow.hPow (α := R) (-1) (m * n) * (r ^ n * g.resultant f n m) = r ^ n * f.resultant g m n
rw₂ :
  HPow.hPow (α := R) (-1) (m * n) * (r ^ n * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₃ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n)) =
    r ^ n * f.resultant g m n
rw₄ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (n * m) * f.resultant g m n) =
    r ^ n * f.resultant g m n
rw₅ :
  r ^ n * (HPow.hPow (α := R) (-1) (m * n) * HPow.hPow (α := R) (-1) (m * n) * f.resultant g m n) =
    r ^ n * f.resultant g m n
rw₆ : r ^ n * (HMul.hMul (α := R) (-1) (-1) ^ (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
rw₇ : r ^ n * (HPow.hPow (α := R) (- -1) (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
rw₈ : r ^ n * (HPow.hPow (α := R) 1 (m * n) * f.resultant g m n) = r ^ n * f.resultant g m n
rw₉ : r ^ n * (1 * f.resultant g m n) = r ^ n * f.resultant g m n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f).resultant g m n = r ^ n * f.resultant g m n
have rw₁₀ : r ^ n * f.resultant g m n = r ^ n * f.resultant g m n
Tactic: rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]
-- 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 : ℕ
hf : f.natDegree ≤ m
⊢ f.resultant g (m + 1) n = HPow.hPow (α := R) (-1) n * g.coeff n * f.resultant g m n
have zero : f.resultant g (m + 1) 0 = HPow.hPow (α := R) (β := ℕ) (-1) 0 * g.coeff 0 * f.resultant g m 0
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- 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 : ℕ
hf : f.natDegree ≤ m
zero : f.resultant g (m + 1) 0 = HPow.hPow (α := R) (β := ℕ) (-1) 0 * g.coeff 0 * f.resultant g m 0
⊢ f.resultant g (m + 1) n = HPow.hPow (α := R) (-1) n * g.coeff n * f.resultant g m n
have succ : ∀ (n : ℕ), f.resultant g (m + 1) (n + 1) = HPow.hPow (α := R) (-1) (n + 1) * g.coeff (n + 1) * f.resultant g m (n + 1)
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ f.resultant g (m + 1) (n + 1) = HPow.hPow (α := R) (-1) (n + 1) * g.coeff (n + 1) * f.resultant g m (n + 1)
have succ : HPow.hPow (α := R) (-1)
        ((↑(Fin.last ((m + 1).add n)) : ℕ) + (↑(Fin.castAdd (n + 1) (Fin.last m) : Fin (m + 1 + (n + 1))) : ℕ)) *
      f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) (Fin.castAdd (n + 1) (Fin.last m)) *
    (Matrix.submatrix (f.sylvester g (m + 1) (n + 1)) (Fin.succAbove (Fin.last ((m + 1).add n)))
        (Fin.succAbove (Fin.castAdd (n + 1) (Fin.last m)))).det =
  HPow.hPow (α := R) (-1) (n + 1) * g.coeff (n + 1) * f.resultant g m (n + 1)
Tactic: rw [resultant, Matrix.det_succ_row (i := .last _),
      Finset.sum_eq_single (by exact ((Fin.last m).castAdd (n + 1))) _ (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
succ :
  HPow.hPow (α := R) (-1)
          ((↑(Fin.last ((m + 1).add n)) : ℕ) + (↑(Fin.castAdd (n + 1) (Fin.last m) : Fin (m + 1 + (n + 1))) : ℕ)) *
        f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) (Fin.castAdd (n + 1) (Fin.last m)) *
      (Matrix.submatrix (f.sylvester g (m + 1) (n + 1)) (Fin.succAbove (Fin.last ((m + 1).add n)))
          (Fin.succAbove (Fin.castAdd (n + 1) (Fin.last m)))).det =
    HPow.hPow (α := R) (-1) (n + 1) * g.coeff (n + 1) * f.resultant g m (n + 1)
⊢ f.resultant g (m + 1) (n + 1) = HPow.hPow (α := R) (-1) (n + 1) * g.coeff (n + 1) * f.resultant g m (n + 1)
have rw : ∀ (b : Fin ((m + 1).add n).succ),
  Membership.mem (γ := Finset (Fin ((m + 1).add n).succ)) Finset.univ b →
    b ≠ Fin.castAdd (n + 1) (Fin.last m) →
      HPow.hPow (α := R) (-1) ((↑(Fin.last ((m + 1).add n)) : ℕ) + (↑b : ℕ)) *
            f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) b *
          (Matrix.submatrix (f.sylvester g (m + 1) (n + 1)) (Fin.succAbove (Fin.last ((m + 1).add n)))
              b.succAbove).det =
        0
Tactic: rw [resultant, Matrix.det_succ_row (i := .last _),
      Finset.sum_eq_single (by exact ((Fin.last m).castAdd (n + 1))) _ (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ HPow.hPow (α := R) (-1)
          ((↑(Fin.last ((m + 1).add n)) : ℕ) + (↑(Fin.castAdd (n + 1) (Fin.last m) : Fin (m + 1 + (n + 1))) : ℕ)) *
        f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) (Fin.castAdd (n + 1) (Fin.last m)) *
      (Matrix.submatrix (f.sylvester g (m + 1) (n + 1)) (Fin.succAbove (Fin.last ((m + 1).add n)))
          (Fin.succAbove (Fin.castAdd (n + 1) (Fin.last m)))).det =
    HPow.hPow (α := R) (-1) (n + 1) * g.coeff (n + 1) * f.resultant g m (n + 1)
have succ : HPow.hPow (α := R) (-1)
        ((↑(Fin.last ((m + 1).add n)) : ℕ) + (↑(Fin.castAdd (n + 1) (Fin.last m) : Fin (m + 1 + (n + 1))) : ℕ)) *
      f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) (Fin.castAdd (n + 1) (Fin.last m)) *
    Matrix.det (n := Fin (m + (n + 1)))
      ((Matrix.reindex (finCongr sorry) (finCongr sorry) :
          (a : Matrix (Fin ((m + 1).add n)) (Fin ((m + 1).add n)) R) → Matrix (Fin (m + (n + 1))) (Fin (m + (n + 1))) R)
        (Matrix.submatrix (f.sylvester g (m + 1) (n + 1)) (Fin.succAbove (Fin.last ((m + 1).add n)))
          (Fin.succAbove (Fin.castAdd (n + 1) (Fin.last m))))) =
  HPow.hPow (α := R) (-1) (n + 1) * g.coeff (n + 1) * Matrix.det (n := Fin (m + (n + 1))) (f.sylvester g m (n + 1))
Tactic: rw [resultant, ← Matrix.det_reindex_self (finCongr (show (m + 1).add n = m + (n + 1) 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 : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ HPow.hPow (α := R) (-1)
          ((↑(Fin.last ((m + 1).add n)) : ℕ) + (↑(Fin.castAdd (n + 1) (Fin.last m) : Fin (m + 1 + (n + 1))) : ℕ)) *
        f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) (Fin.castAdd (n + 1) (Fin.last m)) *
      Matrix.det (n := Fin (m + (n + 1)))
        ((Matrix.reindex (finCongr ⋯) (finCongr ⋯) :
            (a : Matrix (Fin ((m + 1).add n)) (Fin ((m + 1).add n)) R) →
              Matrix (Fin (m + (n + 1))) (Fin (m + (n + 1))) R)
          (Matrix.submatrix (f.sylvester g (m + 1) (n + 1)) (Fin.succAbove (Fin.last ((m + 1).add n)))
            (Fin.succAbove (Fin.castAdd (n + 1) (Fin.last m))))) =
    HPow.hPow (α := R) (-1) (n + 1) * g.coeff (n + 1) * Matrix.det (n := Fin (m + (n + 1))) (f.sylvester g m (n + 1))
have succ : HPow.hPow (α := R) (-1) (m + 1 + n + m) *
      f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) (Fin.castAdd (n + 1) (Fin.last m)) *
    Matrix.det (n := Fin (m + (n + 1)))
      (Matrix.submatrix (f.sylvester g (m + 1) (n + 1))
        (Fin.castSucc ∘ (⇑(finCongr sorry) : (a : Fin (m + (n + 1))) → Fin (m + 1 + n)))
        (Fin.succAbove (Fin.castAdd (n + 1) (Fin.last m)) ∘
          (⇑(finCongr sorry) : (a : Fin (m + (n + 1))) → Fin (m + 1 + n)))) =
  HPow.hPow (α := R) (-1) (n + 1) * g.coeff (n + 1) * Matrix.det (n := Fin (m + (n + 1))) (f.sylvester g m (n + 1))
Tactic: simp only [Nat.add_eq, Nat.succ_eq_add_one, Fin.val_last, Fin.val_castAdd, Fin.succAbove_last,
      Matrix.reindex_apply, finCongr_symm, Matrix.submatrix_submatrix]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ HPow.hPow (α := R) (-1) (m + 1 + n + m) *
        f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) (Fin.castAdd (n + 1) (Fin.last m)) *
      Matrix.det (n := Fin (m + (n + 1)))
        (Matrix.submatrix (f.sylvester g (m + 1) (n + 1))
          (Fin.castSucc ∘ (⇑(finCongr ⋯) : (a : Fin (m + (n + 1))) → Fin (m + 1 + n)))
          (Fin.succAbove (Fin.castAdd (n + 1) (Fin.last m)) ∘
            (⇑(finCongr ⋯) : (a : Fin (m + (n + 1))) → Fin (m + 1 + n)))) =
    HPow.hPow (α := R) (-1) (n + 1) * g.coeff (n + 1) * Matrix.det (n := Fin (m + (n + 1))) (f.sylvester g m (n + 1))
have succ : HPow.hPow (α := R) (-1) (m + 1 + n + m) = HPow.hPow (α := R) (-1) (n + 1)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
succ : HPow.hPow (α := R) (-1) (m + 1 + n + m) = HPow.hPow (α := R) (-1) (n + 1)
⊢ HPow.hPow (α := R) (-1) (m + 1 + n + m) *
        f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) (Fin.castAdd (n + 1) (Fin.last m)) *
      Matrix.det (n := Fin (m + (n + 1)))
        (Matrix.submatrix (f.sylvester g (m + 1) (n + 1))
          (Fin.castSucc ∘ (⇑(finCongr ⋯) : (a : Fin (m + (n + 1))) → Fin (m + 1 + n)))
          (Fin.succAbove (Fin.castAdd (n + 1) (Fin.last m)) ∘
            (⇑(finCongr ⋯) : (a : Fin (m + (n + 1))) → Fin (m + 1 + n)))) =
    HPow.hPow (α := R) (-1) (n + 1) * g.coeff (n + 1) * Matrix.det (n := Fin (m + (n + 1))) (f.sylvester g m (n + 1))
have succ₁ : f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) (Fin.castAdd (n + 1) (Fin.last m)) = g.coeff (n + 1)
Tactic: congr 2