awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₂
i : ℕ
IH : ∀ (hi : i ≤ m), (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
j₁ j₂ : Fin (m + n)
succ :
  (if (↑j₂ : ℕ) = i then r * f.sylvester g m n j₁ (⟨i, ⋯⟩ : Fin (m + n))
    else if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if (↑j₂ : ℕ) < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂
⊢ (M i).updateCol (⟨i, ⋯⟩ : Fin (m + n))
      (HSMul.hSMul (β := (j : Fin (m + n)) → R) r fun (j : Fin (m + n)) ↦ M i j (⟨i, ⋯⟩ : Fin (m + n))) j₁ j₂ =
    M (i + 1) j₁ j₂

Tactic:
simp only [Matrix.of_apply, lt_self_iff_false, ↓reduceIte, Matrix.updateCol_apply,
        Fin.ext_iff, Pi.smul_apply, smul_eq_mul, M, M₂]

Premises used: Fin.ext_iff, Matrix.updateCol_apply, Matrix.of_apply, lt_self_iff_false, reduceIte, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₂
i : ℕ
IH : ∀ (hi : i ≤ m), (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
j₁ j₂ : Fin (m + n)
succ :
  ∀ (IH : ∀ (hi : (↑j₂ : ℕ) ≤ m), (M (↑j₂ : ℕ)).det = r ^ (↑j₂ : ℕ) * M₂.det) (hi : (↑j₂ : ℕ) + 1 ≤ m),
    (if (↑j₂ : ℕ) = (↑j₂ : ℕ) then r * f.sylvester g m n j₁ (⟨(↑j₂ : ℕ), ⋯⟩ : Fin (m + n))
      else if (↑j₂ : ℕ) < (↑j₂ : ℕ) then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
      if (↑j₂ : ℕ) < (↑j₂ : ℕ) + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂
succ₁ :
  ∀ (h : (↑j₂ : ℕ) ≠ i),
    (if (↑j₂ : ℕ) = i then r * f.sylvester g m n j₁ (⟨i, ⋯⟩ : Fin (m + n))
      else if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
      if (↑j₂ : ℕ) < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂
⊢ (if (↑j₂ : ℕ) = i then r * f.sylvester g m n j₁ (⟨i, ⋯⟩ : Fin (m + n))
    else if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if (↑j₂ : ℕ) < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂

Tactic:
obtain rfl | h := eq_or_ne ↑j₂ i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₂
j₁ j₂ : Fin (m + n)
IH : ∀ (hi : (↑j₂ : ℕ) ≤ m), (M (↑j₂ : ℕ)).det = r ^ (↑j₂ : ℕ) * M₂.det
hi : (↑j₂ : ℕ) + 1 ≤ m
succ :
  HMul.hMul (β := R) r
      (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
          (fun (j₁_1 : Fin m) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
          (fun (j₁_1 : Fin n) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
          j₂ :
        R) =
    Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
      (fun (j₁_1 : Fin m) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then r * g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      (fun (j₁_1 : Fin n) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      j₂
⊢ (if (↑j₂ : ℕ) = (↑j₂ : ℕ) then r * f.sylvester g m n j₁ (⟨(↑j₂ : ℕ), ⋯⟩ : Fin (m + n))
    else if (↑j₂ : ℕ) < (↑j₂ : ℕ) then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if (↑j₂ : ℕ) < (↑j₂ : ℕ) + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂

Tactic:
simp only [↓reduceIte, sylvester, Set.mem_Icc, Fin.eta, Matrix.of_apply,
          lt_add_iff_pos_right, zero_lt_one, coeff_C_mul, M₁]

Premises used: lt_add_iff_pos_right, Polynomial.coeff_C_mul, Fin.eta, Matrix.of_apply, zero_lt_one, Polynomial.sylvester, Set.mem_Icc, reduceIte
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₂
j₁ : Fin (m + n)
j₂ : Fin m
IH : ∀ (hi : (↑(Fin.castAdd n j₂) : ℕ) ≤ m), (M (↑(Fin.castAdd n j₂) : ℕ)).det = r ^ (↑(Fin.castAdd n j₂) : ℕ) * M₂.det
hi : (↑(Fin.castAdd n j₂) : ℕ) + 1 ≤ m
⊢ HMul.hMul (β := R) r
      (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
          (fun (j₁_1 : Fin m) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
          (fun (j₁_1 : Fin n) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
          (Fin.castAdd n j₂) :
        R) =
    Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
      (fun (j₁_1 : Fin m) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then r * g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      (fun (j₁_1 : Fin n) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      (Fin.castAdd n j₂)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₂
j₁ : Fin (m + n)
i : Fin n
IH : ∀ (hi : (↑(Fin.natAdd m i) : ℕ) ≤ m), (M (↑(Fin.natAdd m i) : ℕ)).det = r ^ (↑(Fin.natAdd m i) : ℕ) * M₂.det
hi : (↑(Fin.natAdd m i) : ℕ) + 1 ≤ m
⊢ HMul.hMul (β := R) r
      (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
          (fun (j₁_1 : Fin m) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
          (fun (j₁_1 : Fin n) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
          (Fin.natAdd m i) :
        R) =
    Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
      (fun (j₁_1 : Fin m) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then r * g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      (fun (j₁_1 : Fin n) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      (Fin.natAdd m i)

Tactic:
simp at hi
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₂
i : ℕ
IH : ∀ (hi : i ≤ m), (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
j₁ j₂ : Fin (m + n)
h : (↑j₂ : ℕ) ≠ i
⊢ (if (↑j₂ : ℕ) = i then r * f.sylvester g m n j₁ (⟨i, ⋯⟩ : Fin (m + n))
    else if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if (↑j₂ : ℕ) < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₂
i : ℕ
hi : i ≤ m
zero : ∀ (hi : 0 ≤ m), (M 0).det = HPow.hPow (β := ℕ) r 0 * M₂.det
succ :
  ∀ (i : ℕ) (IH : ∀ (hi : i ≤ m), (M i).det = r ^ i * M₂.det) (hi : i + 1 ≤ m), (M (i + 1)).det = r ^ (i + 1) * M₂.det
⊢ (M i).det = r ^ i * M₂.det

Tactic:
induction i with
    | zero => simp [M]; rfl
    | succ i IH =>
      suffices (M i).updateCol ⟨i, by lia⟩ (r • fun j ↦ M i j ⟨i, by lia⟩) = (M (i + 1)) by
        rw [pow_succ', mul_assoc, ← IH (by lia), ← this, Matrix.det_updateCol_smul,
          Matrix.updateCol_eq_self]
      ext j₁ j₂
      simp only [Matrix.of_apply, lt_self_iff_false, ↓reduceIte, Matrix.updateCol_apply,
        Fin.ext_iff, Pi.smul_apply, smul_eq_mul, M, M₂]
      obtain rfl | h := eq_or_ne ↑j₂ i
      · simp only [↓reduceIte, sylvester, Set.mem_Icc, Fin.eta, Matrix.of_apply,
          lt_add_iff_pos_right, zero_lt_one, coeff_C_mul, M₁]
        induction j₂ using Fin.addCases with
        | left j₂ => simp
        | right i => simp at hi
      lia

Premises used: lt_add_iff_pos_right, Fin.ext_iff, Matrix.updateCol_apply, Polynomial.coeff_C_mul, Fin.eta, Matrix.of_apply, zero_lt_one, Polynomial.sylvester, lt_self_iff_false, Set.mem_Icc, eq_or_ne, reduceIte, smul_eq_mul, rfl, Pi.smul_apply
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₂
⊢ ∀ (i : ℕ) (hi : i ≤ m), (M i).det = r ^ i * M₂.det

Tactic:
have (i : ℕ) (hi : i ≤ m) : (M i).det = r ^ i * M₂.det := by
    induction i with
    | zero => simp [M]; rfl
    | succ i IH =>
      suffices (M i).updateCol ⟨i, by lia⟩ (r • fun j ↦ M i j ⟨i, by lia⟩) = (M (i + 1)) by
        rw [pow_succ', mul_assoc, ← IH (by lia), ← this, Matrix.det_updateCol_smul,
          Matrix.updateCol_eq_self]
      ext j₁ j₂
      simp only [Matrix.of_apply, lt_self_iff_false, ↓reduceIte, Matrix.updateCol_apply,
        Fin.ext_iff, Pi.smul_apply, smul_eq_mul, M, M₂]
      obtain rfl | h := eq_or_ne ↑j₂ i
      · simp only [↓reduceIte, sylvester, Set.mem_Icc, Fin.eta, Matrix.of_apply,
          lt_add_iff_pos_right, zero_lt_one, coeff_C_mul, M₁]
        induction j₂ using Fin.addCases with
        | left j₂ => simp
        | right i => simp at hi
      lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
rw : (f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n).det = (M m).det
⊢ f.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n = r ^ m * f.resultant g m n

Tactic:
rw [resultant, resultant, ← this m le_rfl]

Premises used: le_rfl, Polynomial.resultant, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
e_M : f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n = M m
⊢ (f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n).det = (M m).det

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
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
⊢ f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n = M m

Tactic:
ext i j
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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)
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)
⊢ f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n i j = M m i j

Tactic:
induction j using Fin.addCases
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : Fin (m + n)
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:
simp [M, sylvester, M₁, M₂]

Premises used: Polynomial.sylvester
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : Fin (m + n)
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:
simp [M, sylvester, M₁, M₂]

Premises used: Polynomial.sylvester
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
rw₁₀ rw₁₁ : r ^ 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

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]

Premises used: one_pow, Polynomial.resultant_comm, mul_assoc, neg_one_mul, neg_neg, mul_left_comm, HPow.hPow, mul_comm, OfNat.ofNat, mul_pow, Neg.neg, Polynomial.resultant_C_mul_right, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
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)
⊢ f.resultant g (m + 1) n = HPow.hPow (α := R) (-1) n * g.coeff n * f.resultant g m n

Tactic:
obtain _ | n := n
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
⊢ f.resultant g (m + 1) 0 = HPow.hPow (α := R) (β := ℕ) (-1) 0 * g.coeff 0 * f.resultant g m 0

Tactic:
simp [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ Fin ((m + 1).add n).succ

Tactic:
exact ((Fin.last m).castAdd (n + 1))

Premises used: Fin.castAdd, HAdd.hAdd, Fin.last, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (Fin.castAdd (n + 1) (Fin.last m) : Fin (m + 1 + (n + 1))) ∉ Finset.univ →
    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 =
      0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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)
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
⊢ f.resultant g (m + 1) (n + 1) = 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)]

Premises used: Polynomial.resultant, Matrix.det_succ_row, Finset.sum_eq_single, Fin.last, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (m + 1).add n = m + (n + 1)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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.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))
⊢ 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_reindex_self (finCongr (show (m + 1).add n = m + (n + 1) by grind))]

Premises used: Polynomial.resultant, finCongr, Matrix.det_reindex_self, Polynomial.natDegree