awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
H : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).Monic
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have this₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).resultant g
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).natDegree n =
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).leadingCoeff ^ n *
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ eval x g)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff⁻¹ : R[X]) f).roots)
Tactic: have := this (C f.leadingCoeff⁻¹ * f) g n hg (.mul (.C _) hf) hR (by simpa) H
-- 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
hfm : f.Monic
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have simp : f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
Tactic: simp only [hfm.leadingCoeff, one_pow, one_mul]
-- 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
hfm : f.Monic
⊢ f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have pos : ∀ (hg0 : g = 0), f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
Tactic: by_cases hg0 : g = 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
hfm : f.Monic
pos : ∀ (hg0 : g = 0), f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
⊢ f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have neg : ∀ (hg0 : ¬g = 0), f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
Tactic: by_cases hg0 : g = 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
hfm : f.Monic
hg0 : g = 0
⊢ f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have pos : ∀ (hg : natDegree.{u_1} (R := R) 0 ≤ n),
  f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)
Tactic: subst hg0
Cleared hypotheses: g, hg, hg0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
n : ℕ
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg : natDegree.{u_1} (R := R) 0 ≤ n
⊢ f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)
have pos : ∀ (hf' : f.natDegree = 0), f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)
Tactic: by_cases hf' : f.natDegree = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
n : ℕ
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg : natDegree.{u_1} (R := R) 0 ≤ n
pos :
  ∀ (hf' : f.natDegree = 0), f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)
⊢ f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)
have neg : ∀ (hf' : ¬f.natDegree = 0), f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)
Tactic: by_cases hf' : f.natDegree = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
n : ℕ
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg : natDegree.{u_1} (R := R) 0 ≤ n
hf' : f.natDegree = 0
⊢ f.resultant 0 f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) f.roots)
have pos : ∀ (hf : Splits.{u_1} (R := R) 1) (hfm : Monic.{u_1} (R := R) 1) (hf' : natDegree.{u_1} (R := R) 1 = 0),
  Eq.{u_1 + 1} (α := R) (resultant 1 0 (natDegree.{u_1} (R := R) 1) n)
    (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x 0) (roots 1)))
Tactic: obtain ⟨r, rfl⟩ := hfm.natDegree_eq_zero.mp hf'
Cleared hypotheses: f, hf, hfm, 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
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
⊢ f.resultant g f.natDegree 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) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
      f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
  (hgm : ¬g.Monic), f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
Tactic: wlog hgm : g.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
hfm : f.Monic
hg0 : ¬g = 0
neg :
  ∀
    (this :
      ∀ {R : Type u_1} [inst : CommRing R] [inst_2 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n)
        (hf : f.Splits) (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
        f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
    (hgm : ¬g.Monic), f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
⊢ f.resultant g f.natDegree 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) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
  f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
Tactic: wlog hgm : g.Monic
Cleared hypotheses: R, inst, inst_1, f, g, n, hg, hf, hR, hfm, hg0
-- 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
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g).Monic
have rw : g.leadingCoeff⁻¹ * g.coeff g.natDegree = 1
Tactic: rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hg0]), 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
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have this₁ : f.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g) f.natDegree n =
  Multiset.prod
    (Multiset.map (fun (x : R) ↦ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g))
      f.roots)
Tactic: have := this f (C g.leadingCoeff⁻¹ * g) n (by simpa [hg0, natDegree_C_mul]) hf hR hfm (by simpa)
      (by rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hg0]), coeff_C_mul]; simp [hg0])
-- 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
hfm : f.Monic
hg0 : ¬g = 0
this_1 :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_3 : IsDomain R] (f g : R[X]) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits)
    (hR : IsField R) (hfm : f.Monic) (hg0 : ¬g = 0) (hgm : g.Monic),
    f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
hgm : ¬g.Monic
inst : Field R := hR.toField
this :
  f.resultant (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g) f.natDegree n =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g))
        f.roots)
⊢ f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have this₁ : f.resultant g f.natDegree n =
  g.leadingCoeff ^ f.natDegree *
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff⁻¹ : R[X]) g))
        f.roots)
Tactic: rw [resultant_C_mul_right, inv_pow, inv_mul_eq_iff_eq_mul₀ (by simp [hg0])] at this
Cleared hypotheses: this
-- 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
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
⊢ f.resultant g f.natDegree n = Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)
have a : Eq (α := L) (((algebraMap R L : R →+* L) : (a : R) → L) (f.resultant g f.natDegree n) : L)
  (((algebraMap R L : R →+* L) : (a : R) → L) (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)) : L)
Tactic: apply (algebraMap R L).injective
-- 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
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
⊢ Eq (α := L) (((algebraMap R L : R →+* L) : (a : R) → L) (f.resultant g f.natDegree n) : L)
    (((algebraMap R L : R →+* L) : (a : R) → L) (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)) : L)
have this : (map (algebraMap R L) f).resultant (map (algebraMap R L) g) =
  Multiset.prod
    (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
Tactic: have := resultant_eq_prod_roots_sub (f.map (algebraMap R L))
    (g.map (algebraMap R L)) (hfm.map _) (hgm.map _) (hf.map _) (SplittingField.splits _)
-- 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
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
⊢ Eq (α := L) (((algebraMap R L : R →+* L) : (a : R) → L) (f.resultant g f.natDegree n) : L)
    (((algebraMap R L : R →+* L) : (a : R) → L) (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)) : L)
have this₁ : (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
  Multiset.prod
    (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
Tactic: simp_rw [natDegree_map] at this
Cleared hypotheses: this
-- 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
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
⊢ Eq (α := L) (((algebraMap R L : R →+* L) : (a : R) → L) (f.resultant g f.natDegree n) : L)
    (((algebraMap R L : R →+* L) : (a : R) → L) (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots)) : L)
have a : Eq (α := L)
  (Multiset.prod
    (Multiset.map
      ((fun (x : g.SplittingField (K := R)) ↦ eval x (map (algebraMap R (g.SplittingField (K := R))) g)) ∘
        (⇑(algebraMap R L) : (a : R) → L))
      f.roots))
  (Multiset.prod
    (Multiset.map (α := R) (⇑(algebraMap R L : R →+* L) : (a : R) → L) (Multiset.map (fun (x : R) ↦ eval x g) f.roots)))
Tactic: rw [← resultant_map_map, ← Nat.add_sub_cancel' hg, resultant_add_right_deg _ _ _ _ _ (by simp),
    this, coeff_map, coeff_natDegree, hfm.leadingCoeff, map_one, one_pow, one_mul,
    map_sub_sprod_roots_eq_prod_map_eval _ _ (hgm.map _) (SplittingField.splits _),
    hf.roots_map, map_multiset_prod, Multiset.map_map]
-- 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
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
⊢ Eq (α := L)
    (Multiset.prod
      (Multiset.map
        ((fun (x : g.SplittingField (K := R)) ↦ eval x (map (algebraMap R (g.SplittingField (K := R))) g)) ∘
          (⇑(algebraMap R L) : (a : R) → L))
        f.roots))
    (Multiset.prod
      (Multiset.map (α := R) (⇑(algebraMap R L : R →+* L) : (a : R) → L)
        (Multiset.map (fun (x : R) ↦ eval x g) f.roots)))
have a : Eq (α := g.SplittingField (K := R))
  (Multiset.prod
    (Multiset.map
      (fun (x : R) ↦
        ((aeval ((algebraMap R (g.SplittingField (K := R)) : (a : R) → g.SplittingField) x) :
              R[X] →ₐ[R] g.SplittingField (K := R)) :
            (a : R[X]) → g.SplittingField)
          g)
      f.roots))
  (Multiset.prod
    (Multiset.map
      (fun (x : R) ↦
        ((algebraMap R (g.SplittingField (K := R)) : R →+* g.SplittingField (K := R)) : (a : R) → g.SplittingField)
          (eval x g))
      f.roots))
Tactic: simp only [eval_map_algebraMap, Function.comp_apply, Multiset.map_map, L]
-- 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
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
⊢ Eq (α := g.SplittingField (K := R))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          ((aeval ((algebraMap R (g.SplittingField (K := R)) : (a : R) → g.SplittingField) x) :
                R[X] →ₐ[R] g.SplittingField (K := R)) :
              (a : R[X]) → g.SplittingField)
            g)
        f.roots))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          ((algebraMap R (g.SplittingField (K := R)) : R →+* g.SplittingField (K := R)) : (a : R) → g.SplittingField)
            (eval x g))
        f.roots))
have a : Eq.{u_1 + 1} (α := R → g.SplittingField (K := R))
  (fun (x : R) ↦
    ((aeval ((algebraMap R (g.SplittingField (K := R)) : (a : R) → g.SplittingField) x) :
          R[X] →ₐ[R] g.SplittingField (K := R)) :
        (a : R[X]) → g.SplittingField)
      g)
  fun (x : R) ↦
  ((algebraMap R (g.SplittingField (K := R)) : R →+* g.SplittingField (K := R)) : (a : R) → g.SplittingField) (eval x g)
Tactic: congr
-- 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
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
⊢ Eq.{u_1 + 1} (α := R → g.SplittingField (K := R))
    (fun (x : R) ↦
      ((aeval ((algebraMap R (g.SplittingField (K := R)) : (a : R) → g.SplittingField) x) :
            R[X] →ₐ[R] g.SplittingField (K := R)) :
          (a : R[X]) → g.SplittingField)
        g)
    fun (x : R) ↦
    ((algebraMap R (g.SplittingField (K := R)) : R →+* g.SplittingField (K := R)) : (a : R) → g.SplittingField)
      (eval x g)
have a : ∀ (x : R),
  Eq (α := g.SplittingField (K := R))
    (((aeval ((algebraMap R (g.SplittingField (K := R)) : (a : R) → g.SplittingField) x) :
          R[X] →ₐ[R] g.SplittingField (K := R)) :
        (a : R[X]) → g.SplittingField)
      g)
    (((algebraMap R (g.SplittingField (K := R)) : R →+* g.SplittingField (K := R)) : (a : R) → g.SplittingField)
      (eval x g))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
⊢ P p
have inr : ∀ (this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R), P p) (hR : ¬IsDomain R), P p
Tactic: wlog hR : IsDomain R generalizing R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
inr : ∀ (this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R), P p) (hR : ¬IsDomain R), P p
⊢ P p
have wlog : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R), P p
Tactic: wlog hR : IsDomain R generalizing R
Cleared hypotheses: R, inst, p
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst : CommRing R
p : R[X]
hR : IsDomain R
⊢ P p
have inr : ∀ (this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R), P p) (hR : ¬IsField R), P p
Tactic: wlog hR : IsField R generalizing R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst : CommRing R
p : R[X]
hR : IsDomain R
inr :
  ∀ (this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R), P p) (hR : ¬IsField R),
    P p
⊢ P p
have wlog : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R), P p
Tactic: wlog hR : IsField R generalizing R
Cleared hypotheses: R, inst, p, hR
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst : CommRing R
p : R[X]
hR_1 : IsDomain R
hR : IsField R
⊢ P p
have inr : ∀ (this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R) (hp : p.Splits), P p)
  (hp : ¬p.Splits), P p
Tactic: wlog hp : p.Splits generalizing R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst : CommRing R
p : R[X]
hR_1 : IsDomain R
hR : IsField R
inr :
  ∀ (this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R) (hp : p.Splits), P p)
    (hp : ¬p.Splits), P p
⊢ P p
have wlog : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R) (hp : p.Splits), P p
Tactic: wlog hp : p.Splits generalizing R
Cleared hypotheses: R, inst, p, hR_1, hR