awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits)
      (hfg : g.natDegree ≤ f.natDegree) (hN : f.natDegree + g.natDegree = m),
      f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr_1 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this :
  (algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
      (Multiset.prod
          (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2)
            ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)) :
        L)
x : K
hx : ¬g = 0
hxg : eval x g = 0
rw : eval x (f %ₘ g)
| eval x f

Tactic:
rw [← f.modByMonic_add_div, eval_add, eval_mul, hxg, zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, Polynomial.eval_mul, Polynomial.eval_add, Polynomial.modByMonic_add_div, add_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits)
      (hfg : g.natDegree ≤ f.natDegree) (hN : f.natDegree + g.natDegree = m),
      f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr_1 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this :
  (algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
      (Multiset.prod
          (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2)
            ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)) :
        L)
x : K
hx : ¬g = 0
hxg : eval x g = 0
conv_lhs : eval x f = eval x (f %ₘ g)
e_a : eval x (f %ₘ g) = eval x (f %ₘ g)
⊢ eval x f = eval x (f %ₘ g)

Tactic:
conv_lhs => rw [← f.modByMonic_add_div, eval_add, eval_mul, hxg, zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, Polynomial.eval_mul, Polynomial.eval_add, Polynomial.modByMonic_add_div, add_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits)
      (hfg : g.natDegree ≤ f.natDegree) (hN : f.natDegree + g.natDegree = m),
      f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr_1 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this :
  (algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
      (Multiset.prod
          (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2)
            ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)) :
        L)
⊢ Multiset.prod (Multiset.map (fun (x : K) ↦ (f %ₘ g).leadingCoeff * eval x r) g.roots) =
    (f %ₘ g).leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : K) ↦ eval x r) g.roots)

Tactic:
simp [hg'.natDegree_eq_card_roots]

Premises used: Polynomial.Splits.natDegree_eq_card_roots
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits)
      (hfg : g.natDegree ≤ f.natDegree) (hN : f.natDegree + g.natDegree = m),
      f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr_1 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this_1 :
  (algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
      (Multiset.prod
          (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2)
            ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)) :
        L)
this :
  Multiset.prod (Multiset.map (fun (x : K) ↦ eval x f) g.roots) =
    (f %ₘ g).leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : K) ↦ eval x r) g.roots)
neg :
  HPow.hPow (α := L) (-1) (f.natDegree * g.natDegree) *
        HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (f %ₘ g).leadingCoeff : L) g.natDegree *
      Multiset.prod
        (Multiset.map
          (fun (x : K) ↦
            ((aeval ((algebraMap K L : (a : K) → L) x) : K[X] →ₐ[K] r.SplittingField) : (a : K[X]) → r.SplittingField)
              r)
          g.roots) =
    HPow.hPow (α := L) (-1) (f.natDegree * g.natDegree) *
        HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (f %ₘ g).leadingCoeff : L) g.natDegree *
      Multiset.prod (Multiset.map (fun (x : K) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (eval x r)) g.roots)
⊢ HPow.hPow (α := L) (-1) (g.natDegree * (f.natDegree - r.natDegree)) *
      (HPow.hPow (α := L) (-1) (r.natDegree * g.natDegree) *
        (HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (f %ₘ g).leadingCoeff : L) g.natDegree *
          Multiset.prod
            (Multiset.map
              (fun (x : K) ↦
                ((aeval ((algebraMap K L : (a : K) → L) x) : K[X] →ₐ[K] r.SplittingField) :
                    (a : K[X]) → r.SplittingField)
                  r)
              g.roots))) =
    HPow.hPow (α := L) (-1) (g.natDegree * f.natDegree) *
      (HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (f %ₘ g).leadingCoeff : L) g.natDegree *
        Multiset.prod (Multiset.map (fun (x : K) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (eval x r)) g.roots))

Tactic:
simp only [← mul_assoc, ← pow_add, ← add_mul, Nat.sub_add_cancel (hrd.le.trans hfg),
      mul_comm g.natDegree]

Premises used: add_mul, mul_assoc, pow_add, LT.lt.le, Nat.sub_add_cancel, mul_comm, LE.le.trans, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits)
      (hfg : g.natDegree ≤ f.natDegree) (hN : f.natDegree + g.natDegree = m),
      f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr_1 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this_1 :
  (algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
      (Multiset.prod
          (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2)
            ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)) :
        L)
this :
  Multiset.prod (Multiset.map (fun (x : K) ↦ eval x f) g.roots) =
    (f %ₘ g).leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : K) ↦ eval x r) g.roots)
neg :
  ∀ (x : K),
    Eq (α := r.SplittingField)
      (((aeval ((algebraMap K L : (a : K) → L) x) : K[X] →ₐ[K] r.SplittingField) : (a : K[X]) → r.SplittingField) r)
      (((algebraMap K L : K →+* L) : (a : K) → L) (eval x r))
⊢ HPow.hPow (α := L) (-1) (f.natDegree * g.natDegree) *
        HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (f %ₘ g).leadingCoeff : L) g.natDegree *
      Multiset.prod
        (Multiset.map
          (fun (x : K) ↦
            ((aeval ((algebraMap K L : (a : K) → L) x) : K[X] →ₐ[K] r.SplittingField) : (a : K[X]) → r.SplittingField)
              r)
          g.roots) =
    HPow.hPow (α := L) (-1) (f.natDegree * g.natDegree) *
        HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (f %ₘ g).leadingCoeff : L) g.natDegree *
      Multiset.prod (Multiset.map (fun (x : K) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (eval x r)) g.roots)

Tactic:
congr 3 with x
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits)
      (hfg : g.natDegree ≤ f.natDegree) (hN : f.natDegree + g.natDegree = m),
      f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr_1 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this_1 :
  (algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
      (Multiset.prod
          (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2)
            ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)) :
        L)
this :
  Multiset.prod (Multiset.map (fun (x : K) ↦ eval x f) g.roots) =
    (f %ₘ g).leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : K) ↦ eval x r) g.roots)
x : K
⊢ Eq (α := r.SplittingField)
    (((aeval ((algebraMap K L : (a : K) → L) x) : K[X] →ₐ[K] r.SplittingField) : (a : K[X]) → r.SplittingField) r)
    (((algebraMap K L : K →+* L) : (a : K) → L) (eval x r))

Tactic:
aeval_algebraMap_apply _ _ _

Premises used: Polynomial.eval, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits)
      (hfg : g.natDegree ≤ f.natDegree) (hN : f.natDegree + g.natDegree = m),
      f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr_1 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this_1 :
  (algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
      (Multiset.prod
          (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2)
            ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)) :
        L)
this :
  Multiset.prod (Multiset.map (fun (x : K) ↦ eval x f) g.roots) =
    (f %ₘ g).leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : K) ↦ eval x r) g.roots)
x : K
⊢ Eq (α := r.SplittingField)
    (((aeval ((algebraMap K L : (a : K) → L) x) : K[X] →ₐ[K] r.SplittingField) : (a : K[X]) → r.SplittingField) r)
    (((algebraMap K L : K →+* L) : (a : K) → L) (eval x r))

Tactic:
exact aeval_algebraMap_apply _ _ _

Premises used: Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits)
      (hfg : g.natDegree ≤ f.natDegree) (hN : f.natDegree + g.natDegree = m),
      f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr_1 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this :
  (algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
      (Multiset.prod
          (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2)
            ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)) :
        L)
⊢ (f %ₘ g).natDegree ≤ r.natDegree

Tactic:
simp [r, hr₀, natDegree_C_mul]

Premises used: Polynomial.natDegree_C_mul
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits)
      (hfg : g.natDegree ≤ f.natDegree) (hN : f.natDegree + g.natDegree = m),
      f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr_1 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this :
  (algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
      (Multiset.prod
          (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2)
            ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)) :
        L)
neg : (f /ₘ g).natDegree + g.natDegree ≤ f.natDegree
neg₁ : f.natDegree - g.natDegree + g.natDegree ≤ f.natDegree
neg₂ neg₃ : f.natDegree ≤ f.natDegree
⊢ (f /ₘ g).natDegree + g.natDegree ≤ (f %ₘ g + g * (f /ₘ g)).natDegree

Tactic:
rw [f.modByMonic_add_div, natDegree_divByMonic _ hg, Nat.sub_add_cancel hfg]

Premises used: Polynomial.natDegree_divByMonic, Nat.sub_add_cancel, Polynomial.modByMonic_add_div
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits)
      (hfg : g.natDegree ≤ f.natDegree) (hN : f.natDegree + g.natDegree = m),
      f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr_1 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this :
  (algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
      (Multiset.prod
          (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2)
            ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)) :
        L)
⊢ g.natDegree ≤ g.natDegree

Tactic:
simp
-- 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
inr :
  ∀
    (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),
        f.resultant g f.natDegree n =
          f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
    (hR : ¬IsField R),
    f.resultant g f.natDegree n = f.leadingCoeff ^ 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),
    f.resultant g f.natDegree n = f.leadingCoeff ^ 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:
wlog hR : IsField R

Premises used: IsField
-- 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
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),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hR : ¬IsField R
K : Type u_1 := FractionRing R
inr :
  Eq (α := K) ((algebraMap R K : (a : R) → K) (f.resultant g f.natDegree n) : K)
    ((algebraMap R K : (a : R) → K)
        (f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)) :
      K)
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)

Tactic:
apply FaithfulSMul.algebraMap_injective R K

Premises used: FaithfulSMul.algebraMap_injective
-- 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
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),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hR : ¬IsField R
K : Type u_1 := FractionRing R
⊢ (map (algebraMap R K) f).resultant (map (algebraMap R K) g) (map (algebraMap R K) f).natDegree n =
    (map (algebraMap R K) f).leadingCoeff ^ n *
      Multiset.prod (Multiset.map (fun (x : K) ↦ eval x (map (algebraMap R K) g)) (map (algebraMap R K) f).roots)

Tactic:
have := this (f.map (algebraMap R K)) (g.map (algebraMap R K)) n (natDegree_map_le.trans hg)
      (hf.map _) (Field.toIsField _)
-- 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
this_1 :
  ∀ {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),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hR : ¬IsField R
K : Type u_1 := FractionRing R
this :
  (map (algebraMap R K) f).resultant (map (algebraMap R K) g) (map (algebraMap R K) f).natDegree n =
    (map (algebraMap R K) f).leadingCoeff ^ n *
      Multiset.prod (Multiset.map (fun (x : K) ↦ eval x (map (algebraMap R K) g)) (map (algebraMap R K) f).roots)
⊢ (algebraMap R K : (a : R) → K) (f.resultant g f.natDegree n) =
    HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) n *
      Multiset.prod
        (Multiset.map (fun (x : K) ↦ eval x (map (algebraMap R K) g))
          (Multiset.map (⇑(algebraMap R K) : (a : R) → K) f.roots))

Tactic:
simp only [resultant_map_map, natDegree_map_eq_of_injective, leadingCoeff_map_of_injective,
      FaithfulSMul.algebraMap_injective R K, ← hf.natDegree_eq_card_roots,
      ← roots_map_of_injective_of_card_eq_natDegree] at this

Premises used: Polynomial.roots_map_of_injective_of_card_eq_natDegree, Polynomial.Splits.natDegree_eq_card_roots, Polynomial.leadingCoeff_map_of_injective, Polynomial.resultant_map_map, FaithfulSMul.algebraMap_injective, Polynomial.natDegree_map_eq_of_injective
-- 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
this_1 :
  ∀ {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),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hR : ¬IsField R
K : Type u_1 := FractionRing R
this :
  (algebraMap R K : (a : R) → K) (f.resultant g f.natDegree n) =
    HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) n *
      Multiset.prod
        (Multiset.map (fun (x : K) ↦ eval x (map (algebraMap R K) g))
          (Multiset.map (⇑(algebraMap R K) : (a : R) → K) f.roots))
⊢ Eq (α := K) ((algebraMap R K : (a : R) → K) (f.resultant g f.natDegree n) : K)
    ((algebraMap R K : (a : R) → K)
        (f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)) :
      K)

Tactic:
simpa [map_multiset_prod, aeval_algebraMap_apply, Multiset.map_map] using this

Premises used: map_multiset_prod, Multiset.map_map, Polynomial.aeval_algebraMap_apply
-- 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
pos :
  ∀ (hf0 : f = 0),
    f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
neg :
  ∀ (hf0 : ¬f = 0),
    f.resultant g f.natDegree n = f.leadingCoeff ^ 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:
by_cases hf0 : f = 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
hf0 : f = 0
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)

Tactic:
simp [hf0]
-- 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
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) (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),
    f.resultant g f.natDegree n = f.leadingCoeff ^ 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) (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)
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)

Tactic:
wlog hfm : f.Monic

Premises used: Polynomial.Monic