awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
| eval x f
have rw : eval x (f %ₘ g)
Tactic: rw [← f.modByMonic_add_div, eval_add, eval_mul, hxg, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ eval x f = eval x (f %ₘ g)
have conv_lhs : eval x f = eval x (f %ₘ g)
Tactic: conv_lhs => rw [← f.modByMonic_add_div, eval_add, eval_mul, hxg, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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)
⊢ eval x f = eval x (f %ₘ g)
have e_a : eval x (f %ₘ g) = eval x (f %ₘ g)
Tactic: conv_lhs => rw [← f.modByMonic_add_div, eval_add, eval_mul, hxg, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: simp only [← mul_assoc, ← pow_add, ← add_mul, Nat.sub_add_cancel (hrd.le.trans hfg),
      mul_comm g.natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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)
⊢ 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)
have 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))
Tactic: congr 3 with x
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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 + g.natDegree ≤ (f %ₘ g + g * (f /ₘ g)).natDegree
have neg : (f /ₘ g).natDegree + g.natDegree ≤ f.natDegree
Tactic: rw [f.modByMonic_add_div, natDegree_divByMonic _ hg, Nat.sub_add_cancel hfg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ (f /ₘ g).natDegree + g.natDegree ≤ (f %ₘ g + g * (f /ₘ g)).natDegree
have neg₁ : f.natDegree - g.natDegree + g.natDegree ≤ f.natDegree
Tactic: rw [f.modByMonic_add_div, natDegree_divByMonic _ hg, Nat.sub_add_cancel hfg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ (f /ₘ g).natDegree + g.natDegree ≤ (f %ₘ g + g * (f /ₘ g)).natDegree
have neg₂ : f.natDegree ≤ f.natDegree
Tactic: rw [f.modByMonic_add_div, natDegree_divByMonic _ hg, Nat.sub_add_cancel hfg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have 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)
Tactic: wlog hR : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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)
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have 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)
Tactic: wlog hR : IsField R
Cleared hypotheses: R, inst, inst_1, f, g, n, hg, hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have 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)
Tactic: apply FaithfulSMul.algebraMap_injective R K
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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
⊢ 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)
have 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)
Tactic: have := this (f.map (algebraMap R K)) (g.map (algebraMap R K)) n (natDegree_map_le.trans hg)
      (hf.map _) (Field.toIsField _)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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)
⊢ 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)
have 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))
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have 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)
Tactic: by_cases hf0 : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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)
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have 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)
Tactic: by_cases hf0 : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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)
have 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)
Tactic: wlog hfm : f.Monic
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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)
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have 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)
Tactic: wlog hfm : f.Monic
Cleared hypotheses: R, inst, inst_1, f, g, n, hg, hf, hR, hf0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
have rw : f.leadingCoeff⁻¹ * f.coeff f.natDegree = 1
Tactic: rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hf0]), coeff_C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have H : (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]