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
⊢ (map (algebraMap K L) g).natDegree + (map (algebraMap K L) r).natDegree < n
have simp : g.natDegree + r.natDegree < n
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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))
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have 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)
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
Cleared hypotheses: this
-- 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.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have 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))
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]
-- 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 :
  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))
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have neg₁ : (f %ₘ g).natDegree ≤ r.natDegree
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]
-- 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 :
  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
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have neg₂ : (f /ₘ g).natDegree + g.natDegree ≤ (f %ₘ g + g * (f /ₘ g)).natDegree
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]
-- 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 :
  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
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have neg₃ : g.natDegree ≤ g.natDegree
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]
-- 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)
⊢ 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))
have 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)
Tactic: apply (algebraMap K L).injective
-- 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)
⊢ 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)
have 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)
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]
-- 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)
⊢ 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)
have 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))
Tactic: trans (g.roots.map ((f %ₘ g).leadingCoeff * eval · r)).prod
-- 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)
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))
⊢ 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)
have 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)
Tactic: trans (g.roots.map ((f %ₘ g).leadingCoeff * eval · r)).prod
-- 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)
⊢ 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))
have 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)
Tactic: congr 1
-- 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)
⊢ 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)
have e_a : ∀ x ∈ g.roots, eval x f = (f %ₘ g).leadingCoeff * eval x r
Tactic: refine Multiset.map_congr rfl ?_
-- 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 ∈ g.roots, eval x f = (f %ₘ g).leadingCoeff * eval x r
have e_a : ∀ (x : K), ¬g = 0 → eval x g = 0 → eval x f = eval x (f %ₘ g)
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]