awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
a :
  ∀ (i : Fin (m + n)) (j : Fin m),
    Eq (α := R)
      ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
            (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
          (f.sylvesterMap g hf hg) i (Sum.inl j) :
        R)
      ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
            (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
          (f.sylvester g m n) i (Sum.inl j) :
        R)
a₁ :
  ∀ (i : Fin (m + n)) (j : Fin n),
    Eq (α := R)
      ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
            (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
          (f.sylvesterMap g hf hg) i (Sum.inr j) :
        R)
      ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
            (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
          (f.sylvester g m n) i (Sum.inr j) :
        R)
⊢ Eq (α := Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
    ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvesterMap g hf hg) :
      Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
    ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
          (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvester g m n) :
      Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)

Tactic:
ext i (j | j)
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
this :
  (if (↑j : ℕ) ≤ (↑i : ℕ) then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j : ℕ) + n then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0
⊢ Eq (α := R)
    ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvesterMap g hf hg) i (Sum.inl j) :
      R)
    ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
          (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvester g m n) i (Sum.inl j) :
      R)

Tactic:
simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']

Premises used: Polynomial.sylvester, Polynomial.coeff_mul_X_pow', LinearMap.toMatrix_apply
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
a :
  (if (↑j : ℕ) ≤ (↑i : ℕ) then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j : ℕ) + n then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0
⊢ Eq (α := R)
    ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvesterMap g hf hg) i (Sum.inl j) :
      R)
    ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
          (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvester g m n) i (Sum.inl j) :
      R)

Tactic:
suffices (if j.1 ≤ i then g.coeff (i - j) else 0) =
      if j ≤ i.1 ∧ ↑i ≤ j + n then g.coeff (i - j) else 0 by
        simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
a :
  (if (↑j : ℕ) ≤ (↑i : ℕ) then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + n then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j : ℕ) + n then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0

Tactic:
rw [ite_and]

Premises used: ite_and
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
pos :
  ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + n),
    g.coeff ((↑i : ℕ) - (↑j : ℕ)) = g.coeff ((↑i : ℕ) - (↑j : ℕ))
neg : ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : ¬(↑i : ℕ) ≤ (↑j : ℕ) + n), g.coeff ((↑i : ℕ) - (↑j : ℕ)) = 0
neg₁ : ∀ (h₁ : ¬(↑j : ℕ) ≤ (↑i : ℕ)), Eq.{u_1 + 1} (α := R) 0 0
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + n then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : (↑j : ℕ) ≤ (↑i : ℕ)
h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + n
⊢ g.coeff ((↑i : ℕ) - (↑j : ℕ)) = g.coeff ((↑i : ℕ) - (↑j : ℕ))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : (↑j : ℕ) ≤ (↑i : ℕ)
h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + n
⊢ g.coeff ((↑i : ℕ) - (↑j : ℕ)) = g.coeff ((↑i : ℕ) - (↑j : ℕ))

Tactic:
try rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : ¬(↑j : ℕ) ≤ (↑i : ℕ)
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : ¬(↑j : ℕ) ≤ (↑i : ℕ)
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
try rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : (↑j : ℕ) ≤ (↑i : ℕ)
h₂ : ¬(↑i : ℕ) ≤ (↑j : ℕ) + n
⊢ g.natDegree < (↑i : ℕ) - (↑j : ℕ)

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : (↑j : ℕ) ≤ (↑i : ℕ)
h₂ : ¬(↑i : ℕ) ≤ (↑j : ℕ) + n
⊢ g.coeff ((↑i : ℕ) - (↑j : ℕ)) = 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt (by lia)

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
this :
  (if (↑j : ℕ) ≤ (↑i : ℕ) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0
⊢ Eq (α := R)
    ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvesterMap g hf hg) i (Sum.inr j) :
      R)
    ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
          (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvester g m n) i (Sum.inr j) :
      R)

Tactic:
simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']

Premises used: Polynomial.sylvester, Polynomial.coeff_mul_X_pow', LinearMap.toMatrix_apply
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
a :
  (if (↑j : ℕ) ≤ (↑i : ℕ) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0
⊢ Eq (α := R)
    ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvesterMap g hf hg) i (Sum.inr j) :
      R)
    ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
          (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvester g m n) i (Sum.inr j) :
      R)

Tactic:
suffices (if j.1 ≤ i then f.coeff (i - j) else 0) =
      if j ≤ i.1 ∧ ↑i ≤ j + m then f.coeff (i - j) else 0 by
        simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
a :
  (if (↑j : ℕ) ≤ (↑i : ℕ) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0

Tactic:
rw [ite_and]

Premises used: ite_and
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
pos :
  ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + m),
    f.coeff ((↑i : ℕ) - (↑j : ℕ)) = f.coeff ((↑i : ℕ) - (↑j : ℕ))
neg : ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : ¬(↑i : ℕ) ≤ (↑j : ℕ) + m), f.coeff ((↑i : ℕ) - (↑j : ℕ)) = 0
neg₁ : ∀ (h₁ : ¬(↑j : ℕ) ≤ (↑i : ℕ)), Eq.{u_1 + 1} (α := R) 0 0
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : (↑j : ℕ) ≤ (↑i : ℕ)
h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + m
⊢ f.coeff ((↑i : ℕ) - (↑j : ℕ)) = f.coeff ((↑i : ℕ) - (↑j : ℕ))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : (↑j : ℕ) ≤ (↑i : ℕ)
h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + m
⊢ f.coeff ((↑i : ℕ) - (↑j : ℕ)) = f.coeff ((↑i : ℕ) - (↑j : ℕ))

Tactic:
try rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : ¬(↑j : ℕ) ≤ (↑i : ℕ)
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : ¬(↑j : ℕ) ≤ (↑i : ℕ)
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
try rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : (↑j : ℕ) ≤ (↑i : ℕ)
h₂ : ¬(↑i : ℕ) ≤ (↑j : ℕ) + m
⊢ f.natDegree < (↑i : ℕ) - (↑j : ℕ)

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : (↑j : ℕ) ≤ (↑i : ℕ)
h₂ : ¬(↑i : ℕ) ≤ (↑j : ℕ) + m
⊢ f.coeff ((↑i : ℕ) - (↑j : ℕ)) = 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt (by lia)

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
a :
  ∀ (i j : Fin (m + n)),
    (LinearMap.toMatrix
            (Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv)
            (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
        (f.sylvesterMap g hf hg) i j =
      f.sylvester g m n i j
⊢ (LinearMap.toMatrix
          (Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv)
          (degreeLT.basis R (m + n)) :
        (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
      (f.sylvesterMap g hf hg) =
    f.sylvester g m n

Tactic:
ext i j
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i j : Fin (m + n)
a :
  ∀ (j : Fin m ⊕ Fin n),
    (LinearMap.toMatrix
            (Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv)
            (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
        (f.sylvesterMap g hf hg) i ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n)) j) =
      f.sylvester g m n i ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n)) j)
⊢ (LinearMap.toMatrix
          (Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv)
          (degreeLT.basis R (m + n)) :
        (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
      (f.sylvesterMap g hf hg) i j =
    f.sylvester g m n i j

Tactic:
obtain ⟨j, rfl⟩ := finSumFinEquiv.surjective j

Premises used: finSumFinEquiv, Equiv.surjective, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m ⊕ Fin n
⊢ (LinearMap.toMatrix
          (Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv)
          (degreeLT.basis R (m + n)) :
        (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
      (f.sylvesterMap g hf hg) i ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n)) j) =
    f.sylvester g m n i ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n)) j)

Tactic:
simpa [LinearMap.toMatrix_apply] using congr($(toMatrix_sylvesterMap f g hf hg) i j)

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
⊢ Eq (α := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
    ((Matrix.toLin b₂ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
        (HMul.hMul (α := Matrix (Fin (m + n)) (Fin (m + n)) R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
          ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg) :
            Matrix (Fin (m + n)) (Fin (m + n)) R)
          (Matrix.adjugate
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg)))) :
      ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
    ((Matrix.toLin b₂ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
        (HSMul.hSMul (α := R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
          (Matrix.det (n := Fin (m + n))
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg)))
          1) :
      ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))

Tactic:
have := congr(Matrix.toLin b₂ b₂ $(((sylvesterMap f g hf hg).toMatrix b₁ b₂).mul_adjugate))
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
⊢ Eq (α := ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
    ((Matrix.toLin b₁ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
        (HMul.hMul (α := Matrix (Fin (m + n)) (Fin (m + n)) R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
          (Matrix.adjugate
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg)))
          ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg) :
            Matrix (Fin (m + n)) (Fin (m + n)) R)) :
      ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
    ((Matrix.toLin b₁ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
        (HSMul.hSMul (α := R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
          (Matrix.det (n := Fin (m + n))
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg)))
          1) :
      ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)

Tactic:
have := congr(Matrix.toLin b₁ b₁ $(((sylvesterMap f g hf hg).toMatrix b₁ b₂).adjugate_mul))
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
h : Nontrivial R
⊢ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) 1

Tactic:
simpa [Polynomial.mem_degreeLT,
    ← Nat.cast_add, Nat.pos_iff_ne_zero, not_and_or, -not_and] using H

Premises used: Nat.pos_iff_ne_zero, Nat.cast_add, not_and_or, not_and, Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
h : Nontrivial R
X : ↥R[X]_m × ↥R[X]_n :=
  (f.adjSylvester g : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
    (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 ⋯)
⊢ Eq.{u_1 + 1} (α := R[X]) (↑((f.sylvesterMap g hf hg : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) X) : R[X])
    (↑((HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id :
            (a : ↥R[X]_(m + n)) → ↥R[X]_(m + n))
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 ⋯)) :
      R[X])

Tactic:
have : ((sylvesterMap f g hf hg X)).1 = _ :=
    congr(($(sylveserMap_comp_adjSylvester f g hf hg) _).1)
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
h : Nontrivial R
X : ↥R[X]_m × ↥R[X]_n :=
  (f.adjSylvester g : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
    (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 ⋯)
this :
  Eq.{u_1 + 1} (α := R[X]) (↑((f.sylvesterMap g hf hg : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) X) : R[X])
    (↑((HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id :
            (a : ↥R[X]_(m + n)) → ↥R[X]_(m + n))
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 ⋯)) :
      R[X])
⊢ (↑X.2 : R[X]).degree < (↑n : WithBot ℕ)

Tactic:
simpa [-SetLike.coe_mem] using X.2.2

Premises used: SetLike.coe_mem, Prod.snd, Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
h : Nontrivial R
X : ↥R[X]_m × ↥R[X]_n :=
  (f.adjSylvester g : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
    (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 ⋯)
this :
  Eq.{u_1 + 1} (α := R[X]) (↑((f.sylvesterMap g hf hg : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) X) : R[X])
    (↑((HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id :
            (a : ↥R[X]_(m + n)) → ↥R[X]_(m + n))
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 ⋯)) :
      R[X])
⊢ (↑X.1 : R[X]).degree < (↑m : WithBot ℕ)

Tactic:
simpa [-SetLike.coe_mem] using X.1.2

Premises used: SetLike.coe_mem, Prod.fst, Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
h : Nontrivial R
X : ↥R[X]_m × ↥R[X]_n :=
  (f.adjSylvester g : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
    (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 ⋯)
this :
  Eq.{u_1 + 1} (α := R[X]) (↑((f.sylvesterMap g hf hg : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) X) : R[X])
    (↑((HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id :
            (a : ↥R[X]_(m + n)) → ↥R[X]_(m + n))
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 ⋯)) :
      R[X])
⊢ f * (↑X.2 : R[X]) + g * (↑X.1 : R[X]) = (C : (a : R) → R[X]) (f.resultant g m n)

Tactic:
simpa [Algebra.smul_def] using this

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
h : Nontrivial R
X : ↥R[X]_m × ↥R[X]_n :=
  (f.adjSylvester g : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
    (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 ⋯)
this :
  Eq.{u_1 + 1} (α := R[X]) (↑((f.sylvesterMap g hf hg : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) X) : R[X])
    (↑((HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id :
            (a : ↥R[X]_(m + n)) → ↥R[X]_(m + n))
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 ⋯)) :
      R[X])
⊢ ∃ (p : R[X]) (q : R[X]),
    p.degree < (↑n : WithBot ℕ) ∧ q.degree < (↑m : WithBot ℕ) ∧ f * p + g * q = (C : (a : R) → R[X]) (f.resultant g m n)

Tactic:
refine ⟨X.2, X.1, by simpa [-SetLike.coe_mem] using X.2.2,
    by simpa [-SetLike.coe_mem] using X.1.2, by simpa [Algebra.smul_def] using this⟩
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
pos : ∀ (hf0 : f.natDegree = 0), IsUnit (f.resultant g) ↔ IsCoprime f g
neg : ∀ (hf0 : ¬f.natDegree = 0), IsUnit (f.resultant g) ↔ IsCoprime f g
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g

Tactic:
by_cases hf0 : f.natDegree = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : f.natDegree = 0
pos : ∀ (hf : Monic.{u_1} (R := R) 1) (hf0 : natDegree.{u_1} (R := R) 1 = 0), IsUnit (resultant 1 g) ↔ IsCoprime 1 g
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g

Tactic:
obtain rfl := eq_one_of_monic_natDegree_zero hf hf0

Premises used: Polynomial.eq_one_of_monic_natDegree_zero, rfl