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 : ¬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
rw : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).leadingCoeff = 1
rw₁ :
  (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).coeff
      (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).natDegree =
    1
rw₂ :
  (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).coeff (f %ₘ g).natDegree = 1
rw₃ : (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g).coeff (f %ₘ g).natDegree = 1
rw₄ : ((f %ₘ g).coeff (f %ₘ g).natDegree)⁻¹ * (f %ₘ g).coeff (f %ₘ g).natDegree = 1
rw₅ rw₆ : Eq.{u_3 + 1} (α := K) 1 1
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).Monic

Tactic:
rw [Monic, leadingCoeff, natDegree_C_mul (by simpa), coeff_C_mul, leadingCoeff,
      inv_mul_cancel₀ (by simpa)]

Premises used: Polynomial.coeff_C_mul, Polynomial.leadingCoeff, Polynomial.natDegree_C_mul, Polynomial.Monic, inv_mul_cancel₀
-- 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 : ¬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
⊢ r.Monic

Tactic:
have hr : r.Monic := by
    dsimp only [r]
    rw [Monic, leadingCoeff, natDegree_C_mul (by simpa), coeff_C_mul, leadingCoeff,
      inv_mul_cancel₀ (by simpa)]
-- 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
simp : g.natDegree + r.natDegree < n
⊢ (map (algebraMap K L) g).natDegree + (map (algebraMap K L) r).natDegree < n

Tactic:
simp
-- 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
⊢ g.natDegree + r.natDegree < n

Tactic:
lia
-- 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
⊢ (map (algebraMap K L) r).natDegree ≤ (map (algebraMap K L) g).natDegree

Tactic:
simpa [r, natDegree_C_mul, hr₀] using hrd.le

Premises used: LT.lt.le, 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
⊢ (map (algebraMap K L) g).resultant (map (algebraMap K L) r) =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots))

Tactic:
have := IH _ (by simp; lia)
    (g.map (algebraMap K L)) (r.map (algebraMap K L)) (hg.map _) (hr.map _)
    (hg'.map _) (SplittingField.splits _) (by simpa [r, natDegree_C_mul, hr₀] using hrd.le) rfl
-- 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 :
  HMul.hMul (α := L) (β := L) (((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree))⁻¹ : L)
      ((algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.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))
⊢ Ne (α := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L) (0 : L)

Tactic:
simp [hr₀]
-- 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 :
  (map (algebraMap K L) g).resultant (map (algebraMap K L) r) =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots))
⊢ (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)

Tactic:
rw [resultant_map_map, natDegree_map, natDegree_map, resultant_C_mul_right,
    map_mul, inv_pow, map_inv₀, inv_mul_eq_iff_eq_mul₀ (by simp [hr₀])] at this

Premises used: inv_mul_eq_iff_eq_mul₀, Polynomial.natDegree_map, map_inv₀, inv_pow, map_mul, Polynomial.resultant_map_map, Polynomial.resultant_C_mul_right
-- 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 :
  HPow.hPow (α := K) (-1) (g.natDegree * (f.natDegree - r.natDegree)) *
        g.coeff g.natDegree ^ (f.natDegree - r.natDegree) *
      (HPow.hPow (α := K) (-1) (r.natDegree * g.natDegree) * g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
neg₁ : (f %ₘ g).natDegree ≤ r.natDegree
neg₂ : (f /ₘ g).natDegree + g.natDegree ≤ (f %ₘ g + g * (f /ₘ g)).natDegree
neg₃ : g.natDegree ≤ g.natDegree
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))

Tactic:
rw [← f.modByMonic_add_div, resultant_add_mul_left, f.modByMonic_add_div,
    ← Nat.sub_add_cancel (hrd.le.trans hfg), add_comm, resultant_add_left_deg, resultant_comm]

Premises used: Polynomial.resultant_add_left_deg, Polynomial.resultant_comm, LT.lt.le, add_comm, Nat.sub_add_cancel, Polynomial.modByMonic_add_div, Polynomial.resultant_add_mul_left, LE.le.trans
-- 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 :
  Eq (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        (HPow.hPow (α := K) (-1) (g.natDegree * (f.natDegree - r.natDegree)) *
            g.coeff g.natDegree ^ (f.natDegree - r.natDegree) *
          (HPow.hPow (α := K) (-1) (r.natDegree * g.natDegree) * g.resultant (f %ₘ g) g.natDegree r.natDegree)) :
      L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        (Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))) :
      L)
⊢ HPow.hPow (α := K) (-1) (g.natDegree * (f.natDegree - r.natDegree)) *
        g.coeff g.natDegree ^ (f.natDegree - r.natDegree) *
      (HPow.hPow (α := K) (-1) (r.natDegree * g.natDegree) * g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))

Tactic:
apply (algebraMap K L).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- 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 :
  HMul.hMul (α := L) (β := L)
        (((algebraMap K L : K →+* L) : (a : K) → L)
            (HPow.hPow (α := K) (-1) (g.natDegree * (f.natDegree - r.natDegree))) :
          L)
        (((algebraMap K L : K →+* L) : (a : K) → L) (g.coeff g.natDegree ^ (f.natDegree - r.natDegree)) : L) *
      HMul.hMul (α := L)
        (((algebraMap K L : K →+* L) : (a : K) → L) (HPow.hPow (α := K) (-1) (r.natDegree * g.natDegree)) : L)
        (HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
          (Multiset.prod
              (Multiset.map (fun (x : r.SplittingField) ↦ eval x (map (algebraMap K r.SplittingField) r))
                (Multiset.map (⇑(algebraMap K L) : (a : K) → L) g.roots)) :
            r.SplittingField)) =
    HMul.hMul (α := L) (β := L)
      (((algebraMap K L : K →+* L) : (a : K) → L) (HPow.hPow (α := K) (-1) (g.roots.card * f.roots.card)) : L)
      (((algebraMap K L : K →+* L) : (a : K) → L) (Multiset.prod (Multiset.map (fun (x : K) ↦ eval x f) g.roots)) : L)
⊢ Eq (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        (HPow.hPow (α := K) (-1) (g.natDegree * (f.natDegree - r.natDegree)) *
            g.coeff g.natDegree ^ (f.natDegree - r.natDegree) *
          (HPow.hPow (α := K) (-1) (r.natDegree * g.natDegree) * g.resultant (f %ₘ g) g.natDegree r.natDegree)) :
      L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        (Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))) :
      L)

Tactic:
rw [map_mul, map_mul, map_mul, this, map_sub_roots_sprod_eq_prod_map_eval _ _ hf hf',
      map_sub_sprod_roots_eq_prod_map_eval _ _ (hr.map _) (SplittingField.splits _), map_mul,
      hg'.roots_map]

Premises used: Polynomial.map_sub_roots_sprod_eq_prod_map_eval, Polynomial.map_sub_sprod_roots_eq_prod_map_eval, Polynomial.Splits.roots_map, Polynomial.SplittingField.splits, map_mul, Polynomial.Monic.map
-- 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)
trans :
  Eq (α := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ eval x f) g.roots))
    (Multiset.prod (Multiset.map (fun (x : K) ↦ (f %ₘ g).leadingCoeff * eval x r) g.roots))
trans₁ :
  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)
⊢ 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)

Tactic:
trans (g.roots.map ((f %ₘ g).leadingCoeff * eval · r)).prod

Premises used: Polynomial.eval, Polynomial.roots, HMul.hMul, Multiset.map, Multiset.prod, Polynomial.leadingCoeff, Polynomial.modByMonic
-- 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)
e_a :
  Eq (α := Multiset K) (Multiset.map (fun (x : K) ↦ eval x f) g.roots)
    (Multiset.map (fun (x : K) ↦ (f %ₘ g).leadingCoeff * eval x r) g.roots)
⊢ Eq (α := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ eval x f) g.roots))
    (Multiset.prod (Multiset.map (fun (x : K) ↦ (f %ₘ g).leadingCoeff * eval x r) g.roots))

Tactic:
congr 1
-- 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)
⊢ Eq (α := Multiset K) (Multiset.map (fun (x : K) ↦ eval x f) g.roots)
    (Multiset.map (fun (x : K) ↦ (f %ₘ g).leadingCoeff * eval x r) g.roots)

Tactic:
Multiset.map_congr rfl ?_

Premises used: Multiset.map_congr, rfl
-- 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)
e_a : ∀ x ∈ g.roots, eval x f = (f %ₘ g).leadingCoeff * eval x r
⊢ Eq (α := Multiset K) (Multiset.map (fun (x : K) ↦ eval x f) g.roots)
    (Multiset.map (fun (x : K) ↦ (f %ₘ g).leadingCoeff * eval x r) g.roots)

Tactic:
refine Multiset.map_congr rfl ?_

Premises used: Multiset.map_congr, rfl
-- 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)
e_a : ∀ (x : K), ¬g = 0 → eval x g = 0 → eval x f = eval x (f %ₘ g)
⊢ ∀ x ∈ g.roots, eval x f = (f %ₘ g).leadingCoeff * eval x r

Tactic:
simp only [mem_roots', ne_eq, IsRoot.def, eval_mul, eval_C, leadingCoeff_eq_zero, hr₀,
          not_false_eq_true, mul_inv_cancel_left₀, and_imp, r]

Premises used: mul_inv_cancel_left₀, Polynomial.eval_C, and_imp, Polynomial.IsRoot.def, Polynomial.eval_mul, ne_eq, Polynomial.mem_roots', not_false_eq_true, Polynomial.leadingCoeff_eq_zero