awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hf0 : ¬f = 0) (hfm : f.Monic),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hfm : ¬f.Monic
inst : Field R := hR.toField
⊢ f.leadingCoeff⁻¹ ≠ 0

Tactic:
simp [hf0]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hf0 : ¬f = 0) (hfm : f.Monic),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hfm : ¬f.Monic
inst : Field R := hR.toField
rw : f.leadingCoeff⁻¹ * f.coeff f.natDegree = 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).Monic

Tactic:
rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hf0]), coeff_C_mul]

Premises used: Polynomial.coeff_natDegree, Polynomial.coeff_C_mul, Polynomial.natDegree_C_mul, Polynomial.Monic
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hf0 : ¬f = 0) (hfm : f.Monic),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hfm : ¬f.Monic
inst : Field R := hR.toField
⊢ f.leadingCoeff⁻¹ * f.coeff f.natDegree = 1

Tactic:
simp [hf0]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hf0 : ¬f = 0) (hfm : f.Monic),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hfm : ¬f.Monic
inst : Field R := hR.toField
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).Monic

Tactic:
have H : (C f.leadingCoeff⁻¹ * f).Monic := by
      rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hf0]), coeff_C_mul]; simp [hf0]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hf0 : ¬f = 0) (hfm : f.Monic),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hfm : ¬f.Monic
inst : Field R := hR.toField
H : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).Monic
⊢ ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f = 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hf0 : ¬f = 0) (hfm : f.Monic),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hfm : ¬f.Monic
inst : Field R := hR.toField
H : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).Monic
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).resultant g
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).natDegree n =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).leadingCoeff ^ n *
      Multiset.prod
        (Multiset.map (fun (x : R) ↦ eval x g)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).roots)

Tactic:
have := this (C f.leadingCoeff⁻¹ * f) g n hg (.mul (.C _) hf) hR (by simpa) H
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
this_1 :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hf0 : ¬f = 0) (hfm : f.Monic),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hfm : ¬f.Monic
inst : Field R := hR.toField
H : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).Monic
this :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).resultant g
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).natDegree n =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).leadingCoeff ^ n *
      Multiset.prod
        (Multiset.map (fun (x : R) ↦ eval x g)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).roots)
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)

Tactic:
simpa [hf0, natDegree_C_mul, resultant_C_mul_left, inv_mul_eq_iff_eq_mul₀, roots_C_mul,
      H.leadingCoeff] using this

Premises used: Polynomial.roots_C_mul, inv_mul_eq_iff_eq_mul₀, Polynomial.natDegree_C_mul, Polynomial.Monic.leadingCoeff, Polynomial.resultant_C_mul_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
hfm : f.Monic
simp : f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)

Tactic:
simp only [hfm.leadingCoeff, one_pow, one_mul]

Premises used: one_pow, Polynomial.Monic.leadingCoeff, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
pos : ∀ (hg0 : g = 0), f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
neg : ∀ (hg0 : ¬g = 0), f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
⊢ f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)

Tactic:
by_cases hg0 : g = 0
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : g = 0
pos :
  ∀ (hg : natDegree.{u_1} (R := R) 0 ≤ n),
    f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)
⊢ f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)

Tactic:
subst hg0
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
n : ℕ
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg : natDegree.{u_1} (R := R) 0 ≤ n
pos :
  ∀ (hf' : f.natDegree = 0), f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)
neg :
  ∀ (hf' : ¬f.natDegree = 0),
    f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)
⊢ f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)

Tactic:
by_cases hf' : f.natDegree = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
n : ℕ
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg : natDegree.{u_1} (R := R) 0 ≤ n
hf' : f.natDegree = 0
pos :
  ∀ (hf : Splits.{u_1} (R := R) 1) (hfm : Monic.{u_1} (R := R) 1) (hf' : natDegree.{u_1} (R := R) 1 = 0),
    Eq.{u_1 + 1} (α := R) (resultant 1 0 (natDegree.{u_1} (R := R) 1) n)
      (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) (roots 1)))
⊢ f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)

Tactic:
obtain ⟨r, rfl⟩ := hfm.natDegree_eq_zero.mp hf'

Premises used: Polynomial.Monic.natDegree_eq_zero, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hR : IsField R
hg : natDegree.{u_1} (R := R) 0 ≤ n
hf : Splits.{u_1} (R := R) 1
hfm : Monic.{u_1} (R := R) 1
hf' : natDegree.{u_1} (R := R) 1 = 0
⊢ Eq.{u_1 + 1} (α := R) (resultant 1 0 (natDegree.{u_1} (R := R) 1) n)
    (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) (roots 1)))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
n : ℕ
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg : natDegree.{u_1} (R := R) 0 ≤ n
hf' : ¬f.natDegree = 0
⊢ f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)

Tactic:
simp [← hf.natDegree_eq_card_roots, hf']

Premises used: Polynomial.Splits.natDegree_eq_card_roots
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
neg :
  ∀
    (this :
      ∀ {R : Type u_1} [inst : CommRing R] [inst_2 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n)
        (hf : f.Splits) (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
        f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
    (hgm : ¬g.Monic), f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
wlog :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_2 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
⊢ f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)

Tactic:
wlog hgm : g.Monic

Premises used: Polynomial.Monic
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g).natDegree ≤ n

Tactic:
simpa [hg0, natDegree_C_mul]

Premises used: Polynomial.natDegree_C_mul
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ ¬HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g = 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ g.leadingCoeff⁻¹ ≠ 0

Tactic:
simp [hg0]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
rw : g.leadingCoeff⁻¹ * g.coeff g.natDegree = 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g).Monic

Tactic:
rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hg0]), coeff_C_mul]

Premises used: Polynomial.coeff_natDegree, Polynomial.coeff_C_mul, Polynomial.natDegree_C_mul, Polynomial.Monic
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ g.leadingCoeff⁻¹ * g.coeff g.natDegree = 1

Tactic:
simp [hg0]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ f.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g) f.natDegree n =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g))
        f.roots)

Tactic:
have := this f (C g.leadingCoeff⁻¹ * g) n (by simpa [hg0, natDegree_C_mul]) hf hR hfm (by simpa)
      (by rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hg0]), coeff_C_mul]; simp [hg0])
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this_1 :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
this :
  (g.leadingCoeff ^ f.natDegree)⁻¹ * f.resultant g f.natDegree n =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g))
        f.roots)
⊢ g.leadingCoeff ^ f.natDegree ≠ 0

Tactic:
simp [hg0]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this_1 :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
this :
  f.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g) f.natDegree n =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g))
        f.roots)
⊢ f.resultant g f.natDegree n =
    g.leadingCoeff ^ f.natDegree *
      Multiset.prod
        (Multiset.map (fun (x : R) ↦ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g))
          f.roots)

Tactic:
rw [resultant_C_mul_right, inv_pow, inv_mul_eq_iff_eq_mul₀ (by simp [hg0])] at this

Premises used: inv_mul_eq_iff_eq_mul₀, inv_pow, Polynomial.resultant_C_mul_right
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this_1 :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
this :
  f.resultant g f.natDegree n =
    g.leadingCoeff ^ f.natDegree *
      Multiset.prod
        (Multiset.map (fun (x : R) ↦ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g))
          f.roots)
⊢ f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)

Tactic:
simpa [← hf.natDegree_eq_card_roots, inv_pow, mul_left_comm (_ ^ g.natDegree), hg0] using this

Premises used: mul_left_comm, inv_pow, Polynomial.Splits.natDegree_eq_card_roots, HPow.hPow, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
a :
  Eq (α := L) (((algebraMap R L : R →+* L) : (a : R) → L) (f.resultant g f.natDegree n) : L)
    (((algebraMap R L : R →+* L) : (a : R) → L) (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)) : L)
⊢ f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)

Tactic:
apply (algebraMap R L).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
⊢ (map (algebraMap R L) f).resultant (map (algebraMap R L) g) =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))

Tactic:
have := resultant_eq_prod_roots_sub (f.map (algebraMap R L))
    (g.map (algebraMap R L)) (hfm.map _) (hgm.map _) (hf.map _) (SplittingField.splits _)
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
⊢ (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))

Tactic:
simp_rw [natDegree_map] at this

Premises used: Polynomial.natDegree_map
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
⊢ (map (algebraMap R L) g).natDegree ≤ g.natDegree

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
a :
  Eq (α := L)
    (Multiset.prod
      (Multiset.map
        ((fun (x : g.SplittingField (K := R)) ↦ eval x (map (algebraMap R (g.SplittingField (K := R))) g)) ∘
          (⇑(algebraMap R L) : (a : R) → L))
        f.roots))
    (Multiset.prod
      (Multiset.map (α := R) (⇑(algebraMap R L : R →+* L) : (a : R) → L)
        (Multiset.map (fun (x : R) ↦ eval x g) f.roots)))
⊢ Eq (α := L) (((algebraMap R L : R →+* L) : (a : R) → L) (f.resultant g f.natDegree n) : L)
    (((algebraMap R L : R →+* L) : (a : R) → L) (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)) : L)

Tactic:
rw [← resultant_map_map, ← Nat.add_sub_cancel' hg, resultant_add_right_deg _ _ _ _ _ (by simp),
    this, coeff_map, coeff_natDegree, hfm.leadingCoeff, map_one, one_pow, one_mul,
    map_sub_sprod_roots_eq_prod_map_eval _ _ (hgm.map _) (SplittingField.splits _),
    hf.roots_map, map_multiset_prod, Multiset.map_map]

Premises used: one_pow, Polynomial.coeff_map, Polynomial.coeff_natDegree, Polynomial.map_sub_sprod_roots_eq_prod_map_eval, Polynomial.Splits.roots_map, Polynomial.SplittingField.splits, map_multiset_prod, map_one, Polynomial.resultant_map_map, Polynomial.resultant_add_right_deg, Multiset.map_map, Polynomial.Monic.leadingCoeff, Nat.add_sub_cancel', Polynomial.Monic.map, one_mul