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 : ℕ
⊢ HMul.hMul (α := R)
      (∏ x : Fin n,
        HMul.hMul (α := R) (∏ x : Fin n, if False then -1 else 1)
          (∏ x_1 : Fin m, if (↑x : ℕ) < n + (↑x_1 : ℕ) ∧ ¬m + (↑x : ℕ) < (↑x_1 : ℕ) then -1 else 1))
      (∏ x : Fin m,
        HMul.hMul (α := R) (∏ x_1 : Fin n, if n + (↑x : ℕ) < (↑x_1 : ℕ) ∧ ¬(↑x : ℕ) < m + (↑x_1 : ℕ) then -1 else 1)
          (∏ x : Fin m, if False then -1 else 1)) =
    HPow.hPow (α := R) (-1) (m * n)

Tactic:
simp [(Fin.isLt _).trans_le, (Fin.isLt _).le.trans, pow_mul]

Premises used: Fin.isLt, LT.lt.le, pow_mul, LT.lt.trans_le, LE.le.trans
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
rw : HPow.hPow (α := R) (-1) (m * 0) * g.resultant f 0 m = g.coeff 0 ^ m
⊢ f.resultant g m 0 = g.coeff 0 ^ m

Tactic:
rw [resultant_comm]

Premises used: Polynomial.resultant_comm
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
⊢ HPow.hPow (α := R) (-1) (m * 0) * g.resultant f 0 m = g.coeff 0 ^ m

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m : ℕ
r : R
⊢ f.resultant ((C : (a : R) → R[X]) r) m 0 = r ^ m

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
zero : f.resultant 0 0 n = HPow.hPow (α := R) (β := ℕ) 0 0 * f.coeff 0 ^ n
succ : ∀ (m : ℕ), f.resultant 0 (m + 1) n = HPow.hPow (α := R) 0 (m + 1) * f.coeff 0 ^ n
⊢ f.resultant 0 m n = HPow.hPow (α := R) 0 m * f.coeff 0 ^ n

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

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
n m : ℕ
i : Fin (m + 1 + n)
⊢ 0 < m + 1 + n

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
n m : ℕ
i : Fin (m + 1 + n)
⊢ f.sylvester 0 (m + 1) n i (⟨0, ⋯⟩ : Fin (m + 1 + n)) = 0

Tactic:
simp [sylvester, show (0 : Fin (m + 1 + n)) = Fin.castAdd _ 0 from rfl, Fin.addCases_left]

Premises used: Fin.addCases_left, Polynomial.sylvester, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
n m : ℕ
⊢ ∀ (i : Fin (m + 1 + n)), f.sylvester 0 (m + 1) n i (⟨0, ⋯⟩ : Fin (m + 1 + n)) = 0

Tactic:
have (i : Fin (m + 1 + n)) : sylvester f 0 (m + 1) n i ⟨0, by lia⟩ = 0 := by
    simp [sylvester, show (0 : Fin (m + 1 + n)) = Fin.castAdd _ 0 from rfl, Fin.addCases_left]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
n m : ℕ
this : ∀ (i : Fin (m + 1 + n)), f.sylvester 0 (m + 1) n i (⟨0, ⋯⟩ : Fin (m + 1 + n)) = 0
⊢ 0 < m + 1 + n

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
n m : ℕ
this : ∀ (i : Fin (m + 1 + n)), f.sylvester 0 (m + 1) n i (⟨0, ⋯⟩ : Fin (m + 1 + n)) = 0
⊢ f.resultant 0 (m + 1) n = HPow.hPow (α := R) 0 (m + 1) * f.coeff 0 ^ n

Tactic:
simpa [resultant] using Matrix.det_eq_zero_of_column_eq_zero ⟨0, by lia⟩ this

Premises used: Polynomial.resultant, Matrix.det_eq_zero_of_column_eq_zero, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
rw : HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) 0 n * g.coeff 0 ^ m) = HPow.hPow (α := R) 0 n * g.coeff 0 ^ m
⊢ resultant 0 g m n = HPow.hPow (α := R) 0 n * g.coeff 0 ^ m

Tactic:
rw [resultant_comm, resultant_zero_right]

Premises used: Polynomial.resultant_zero_right, Polynomial.resultant_comm
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
zero :
  HPow.hPow (α := R) (-1) (m * 0) * (HPow.hPow (α := R) (β := ℕ) 0 0 * g.coeff 0 ^ m) =
    HPow.hPow (α := R) (β := ℕ) 0 0 * g.coeff 0 ^ m
succ :
  ∀ (n : ℕ),
    HPow.hPow (α := R) (-1) (m * (n + 1)) * (HPow.hPow (α := R) 0 (n + 1) * g.coeff 0 ^ m) =
      HPow.hPow (α := R) 0 (n + 1) * g.coeff 0 ^ m
⊢ HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) 0 n * g.coeff 0 ^ m) = HPow.hPow (α := R) 0 n * g.coeff 0 ^ m

Tactic:
cases n
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m : ℕ
⊢ HPow.hPow (α := R) (-1) (m * 0) * (HPow.hPow (α := R) (β := ℕ) 0 0 * g.coeff 0 ^ m) =
    HPow.hPow (α := R) (β := ℕ) 0 0 * g.coeff 0 ^ m

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
⊢ HPow.hPow (α := R) (-1) (m * (n + 1)) * (HPow.hPow (α := R) 0 (n + 1) * g.coeff 0 ^ m) =
    HPow.hPow (α := R) 0 (n + 1) * g.coeff 0 ^ m

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
m n : ℕ
⊢ resultant 0 0 m n = HPow.hPow (α := R) 0 (m + n)

Tactic:
simp [pow_add]

Premises used: pow_add
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
inl :
  ∀ (hk : k + 0 ≤ n) (hf : f.natDegree ≤ 0),
    f.resultant (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 0 n = f.resultant g 0 n
inr :
  ∀ (hm : m ≠ 0),
    f.resultant (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n = f.resultant g m n
⊢ f.resultant (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n = f.resultant g m n

Tactic:
obtain rfl | hm := eq_or_ne m 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
n k : ℕ
hk : k + 0 ≤ n
hf : f.natDegree ≤ 0
inl :
  ∀ (q : R) (hf : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) q) ≤ 0),
    resultant ((C : (a : R) → R[X]) q)
        (g + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) q : R[X]) ((monomial k : (a : R) → R[X]) r : R[X]))
        0 n =
      resultant ((C : (a : R) → R[X]) q) g 0 n
⊢ f.resultant (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 0 n = f.resultant g 0 n

Tactic:
obtain ⟨q, rfl⟩ := natDegree_eq_zero.mp (le_zero_iff.mp hf)

Premises used: le_zero_iff, Iff.mp, Polynomial.natDegree_eq_zero, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
r : R
n k : ℕ
hk : k + 0 ≤ n
q : R
hf : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) q) ≤ 0
⊢ resultant ((C : (a : R) → R[X]) q)
      (g + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) q : R[X]) ((monomial k : (a : R) → R[X]) r : R[X])) 0
      n =
    resultant ((C : (a : R) → R[X]) q) g 0 n

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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₂
hi : 0 ≤ m
zero :
  Matrix.det (n := Fin (m + n))
      ((Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R)
        fun (j₁ j₂ : Fin (m + n)) ↦ M₂ j₁ j₂) =
    M₂.det
⊢ (M 0).det = M₂.det

Tactic:
simp [M]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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₂
hi : 0 ≤ m
⊢ Matrix.det (n := Fin (m + n))
      ((Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R)
        fun (j₁ j₂ : Fin (m + n)) ↦ M₂ j₁ j₂) =
    M₂.det

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : i + 1 ≤ m
⊢ i ≤ m

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : i + 1 ≤ m
⊢ i < m + n

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : i + 1 ≤ m
⊢ i + k + m < m + n

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : i + 1 ≤ m
simp : ¬i = i + k + m
⊢ (⟨i, ⋯⟩ : Fin (m + n)) ≠ ⟨i + k + m, ⋯⟩

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : i + 1 ≤ m
⊢ ¬i = i + k + m

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : i + 1 ≤ m
succ :
  ((M (i + 1)).updateCol (⟨i, ⋯⟩ : Fin (m + n)) fun (k_1 : Fin (m + n)) ↦
        M (i + 1) k_1 (⟨i, ⋯⟩ : Fin (m + n)) + -r • M (i + 1) k_1 (⟨i + k + m, ⋯⟩ : Fin (m + n))).det =
    (M i).det
⊢ (M (i + 1)).det = M₂.det

Tactic:
rw [← IH (by lia), ← Matrix.det_updateCol_add_smul_self (i := ⟨i, by lia⟩)
        (j := ⟨i + k + m, by lia⟩) (c := -r) (M (i + 1)) (by simp; lia)]

Premises used: HAdd.hAdd, Matrix.det_updateCol_add_smul_self, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : i + 1 ≤ m
succ :
  ((M (i + 1)).updateCol (⟨i, ⋯⟩ : Fin (m + n)) fun (k_1 : Fin (m + n)) ↦
      M (i + 1) k_1 (⟨i, ⋯⟩ : Fin (m + n)) + -r • M (i + 1) k_1 (⟨i + k + m, ⋯⟩ : Fin (m + n))) =
    M i
⊢ ((M (i + 1)).updateCol (⟨i, ⋯⟩ : Fin (m + n)) fun (k_1 : Fin (m + n)) ↦
        M (i + 1) k_1 (⟨i, ⋯⟩ : Fin (m + n)) + -r • M (i + 1) k_1 (⟨i + k + m, ⋯⟩ : Fin (m + n))).det =
    (M i).det

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : i + 1 ≤ m
succ :
  ∀ (j₁ j₂ : Fin (m + n)),
    (M (i + 1)).updateCol (⟨i, ⋯⟩ : Fin (m + n))
        (fun (k_1 : Fin (m + n)) ↦
          M (i + 1) k_1 (⟨i, ⋯⟩ : Fin (m + n)) + -r • M (i + 1) k_1 (⟨i + k + m, ⋯⟩ : Fin (m + n)))
        j₁ j₂ =
      M i j₁ j₂
⊢ ((M (i + 1)).updateCol (⟨i, ⋯⟩ : Fin (m + n)) fun (k_1 : Fin (m + n)) ↦
      M (i + 1) k_1 (⟨i, ⋯⟩ : Fin (m + n)) + -r • M (i + 1) k_1 (⟨i + k + m, ⋯⟩ : Fin (m + n))) =
    M i

Tactic:
ext j₁ j₂
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : i + 1 ≤ m
j₁ j₂ : Fin (m + n)
succ :
  (if (↑j₂ : ℕ) = i then M₁ j₁ (⟨i, ⋯⟩ : Fin (m + n)) - r * f.sylvester g m n j₁ (⟨i + (k + m), ⋯⟩ : Fin (m + n))
    else if (↑j₂ : ℕ) < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂
⊢ (M (i + 1)).updateCol (⟨i, ⋯⟩ : Fin (m + n))
      (fun (k_1 : Fin (m + n)) ↦
        M (i + 1) k_1 (⟨i, ⋯⟩ : Fin (m + n)) + -r • M (i + 1) k_1 (⟨i + k + m, ⋯⟩ : Fin (m + n)))
      j₁ j₂ =
    M i j₁ j₂

Tactic:
simp only [Matrix.of_apply, lt_add_iff_pos_right, zero_lt_one, ↓reduceIte, add_assoc,
        add_lt_add_iff_left, Nat.lt_one_iff, Nat.add_eq_zero_iff, hm, and_false, smul_eq_mul,
        Matrix.updateCol_apply, Fin.ext_iff, M, M₂, neg_mul, ← sub_eq_add_neg]

Premises used: lt_add_iff_pos_right, Fin.ext_iff, add_assoc, Matrix.updateCol_apply, sub_eq_add_neg, Matrix.of_apply, zero_lt_one, Nat.lt_one_iff, reduceIte, neg_mul, and_false, smul_eq_mul, Nat.add_eq_zero_iff, add_lt_add_iff_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : i + 1 ≤ m
j₁ j₂ : Fin (m + n)
succ :
  ∀ (IH : ∀ (hi : (↑j₂ : ℕ) ≤ m), (M (↑j₂ : ℕ)).det = M₂.det) (hi : (↑j₂ : ℕ) + 1 ≤ m),
    (if (↑j₂ : ℕ) = (↑j₂ : ℕ) then
        M₁ j₁ (⟨(↑j₂ : ℕ), ⋯⟩ : Fin (m + n)) - r * f.sylvester g m n j₁ (⟨(↑j₂ : ℕ) + (k + m), ⋯⟩ : Fin (m + n))
      else if (↑j₂ : ℕ) < (↑j₂ : ℕ) + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
      if (↑j₂ : ℕ) < (↑j₂ : ℕ) then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂
succ₁ :
  ∀ (h : (↑j₂ : ℕ) ≠ i),
    (if (↑j₂ : ℕ) = i then M₁ j₁ (⟨i, ⋯⟩ : Fin (m + n)) - r * f.sylvester g m n j₁ (⟨i + (k + m), ⋯⟩ : Fin (m + n))
      else if (↑j₂ : ℕ) < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂
⊢ (if (↑j₂ : ℕ) = i then M₁ j₁ (⟨i, ⋯⟩ : Fin (m + n)) - r * f.sylvester g m n j₁ (⟨i + (k + m), ⋯⟩ : Fin (m + n))
    else if (↑j₂ : ℕ) < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if (↑j₂ : ℕ) < i 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]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : (↑j₂ : ℕ) + 1 ≤ m
succ :
  HSub.hSub (α := 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 : ℕ)) +
                (HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])).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)
      (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₂ : ℕ) + (k + m), ⋯⟩ : Fin (m + n)) :
          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₂
⊢ (if (↑j₂ : ℕ) = (↑j₂ : ℕ) then
      M₁ j₁ (⟨(↑j₂ : ℕ), ⋯⟩ : Fin (m + n)) - r * f.sylvester g m n j₁ (⟨(↑j₂ : ℕ) + (k + m), ⋯⟩ : Fin (m + n))
    else if (↑j₂ : ℕ) < (↑j₂ : ℕ) + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if (↑j₂ : ℕ) < (↑j₂ : ℕ) then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂

Tactic:
simp only [↓reduceIte, sylvester, Set.mem_Icc, coeff_add, Fin.eta, Matrix.of_apply,
          lt_self_iff_false, M₁]

Premises used: Fin.eta, Polynomial.coeff_add, Matrix.of_apply, Polynomial.sylvester, lt_self_iff_false, Set.mem_Icc, reduceIte
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : (↑j₂ : ℕ) + 1 ≤ m
⊢ (↑j₂ : ℕ) + (k + m) < m + n

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : (↑j₂ : ℕ) + 1 ≤ m
⊢ (↑j₂ : ℕ) + k < n

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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 = M₂.det
hi : (↑j₂ : ℕ) + 1 ≤ m
⊢ (↑j₂ : ℕ) + (k + m) = m + ((↑j₂ : ℕ) + k)

Tactic:
lia