awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
m : ℕ
hm : f.natDegree ≤ m
⊢ f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
have inr : ∀
  (this :
    ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ) (hm : f.natDegree ≤ m) (hgn : m = f.natDegree),
      f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m)
  (hgn : ¬m = f.natDegree), f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
Tactic: wlog hgn : m = f.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
m : ℕ
hm : f.natDegree ≤ m
inr :
  ∀
    (this :
      ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ) (hm : f.natDegree ≤ m) (hgn : m = f.natDegree),
        f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m)
    (hgn : ¬m = f.natDegree),
    f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
⊢ f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
have wlog : ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ) (hm : f.natDegree ≤ m) (hgn : m = f.natDegree),
  f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
Tactic: wlog hgn : m = f.natDegree
Cleared hypotheses: R, inst, f, g₁, g₂, m, hm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
m : ℕ
hm : f.natDegree ≤ m
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ) (hm : f.natDegree ≤ m) (hgn : m = f.natDegree),
    f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
hgn : ¬m = f.natDegree
⊢ f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
have inr : ∀ (c : ℕ) (hm : f.natDegree ≤ f.natDegree + c) (hgn : ¬f.natDegree + c = f.natDegree),
  f.resultant (g₁ * g₂) (f.natDegree + c) (g₁.natDegree + g₂.natDegree) =
    f.resultant g₁ (f.natDegree + c) * f.resultant g₂ (f.natDegree + c)
Tactic: obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hm
Cleared hypotheses: m, hm, hgn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ) (hm : f.natDegree ≤ m) (hgn : m = f.natDegree),
    f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
c : ℕ
hm : f.natDegree ≤ f.natDegree + c
hgn : ¬f.natDegree + c = f.natDegree
⊢ f.resultant (g₁ * g₂) (f.natDegree + c) (g₁.natDegree + g₂.natDegree) =
    f.resultant g₁ (f.natDegree + c) * f.resultant g₂ (f.natDegree + c)
have inr : HPow.hPow (α := R) (-1) ((g₁.natDegree + g₂.natDegree) * c) * (g₁.leadingCoeff * g₂.leadingCoeff) ^ c *
    (f.resultant g₁ * f.resultant g₂) =
  HPow.hPow (α := R) (-1) (g₁.natDegree * c) * g₁.leadingCoeff ^ c * f.resultant g₁ *
    (HPow.hPow (α := R) (-1) (g₂.natDegree * c) * g₂.leadingCoeff ^ c * f.resultant g₂)
Tactic: simp [resultant_add_left_deg, this f g₁ g₂, coeff_mul_degree_add_degree]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
m : ℕ
hm : f.natDegree ≤ m
hgn : m = f.natDegree
⊢ f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
have subst : ∀ (hm : f.natDegree ≤ f.natDegree),
  f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
Tactic: subst hgn
Cleared hypotheses: m, hm, hgn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
hff : f.Splits
g₁ g₂ : R[X]
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
have Splits : f.leadingCoeff ^ (g₁.natDegree + g₂.natDegree) *
    HMul.hMul (α := R) (Multiset.prod (Multiset.map (fun (i : R) ↦ eval i g₁) f.roots))
      (Multiset.prod (Multiset.map (fun (i : R) ↦ eval i g₂) f.roots)) =
  f.leadingCoeff ^ g₁.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g₁) f.roots) *
    (f.leadingCoeff ^ g₂.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g₂) f.roots))
Tactic: simp [resultant_eq_prod_eval, natDegree_mul_le, hff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R SatisfiesM : Type u_1
inst_1 : CommRing R
inst_2 : CommRing SatisfiesM
φ : R →+* SatisfiesM
hφ : Function.Injective (α := R) (β := SatisfiesM) (⇑φ : (a : R) → SatisfiesM)
f : R[X]
IH :
  ∀ (g₁ g₂ : SatisfiesM[X]),
    (map φ f).resultant (g₁ * g₂) (map φ f).natDegree (g₁.natDegree + g₂.natDegree) =
      (map φ f).resultant g₁ * (map φ f).resultant g₂
g₁ g₂ : R[X]
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
have injective : Eq (α := SatisfiesM)
  ((φ : (a : R) → SatisfiesM) (f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree)) : SatisfiesM)
  ((φ : (a : R) → SatisfiesM) (f.resultant g₁ * f.resultant g₂) : SatisfiesM)
Tactic: apply hφ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R SatisfiesM : Type u_1
inst_1 : CommRing R
inst_2 : CommRing SatisfiesM
φ : R →+* SatisfiesM
hφ : Function.Injective (α := R) (β := SatisfiesM) (⇑φ : (a : R) → SatisfiesM)
f : R[X]
IH :
  ∀ (g₁ g₂ : SatisfiesM[X]),
    (map φ f).resultant (g₁ * g₂) (map φ f).natDegree (g₁.natDegree + g₂.natDegree) =
      (map φ f).resultant g₁ * (map φ f).resultant g₂
g₁ g₂ : R[X]
⊢ Eq (α := SatisfiesM)
    ((φ : (a : R) → SatisfiesM) (f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree)) : SatisfiesM)
    ((φ : (a : R) → SatisfiesM) (f.resultant g₁ * f.resultant g₂) : SatisfiesM)
have this : (map φ f).resultant (map φ g₁ * map φ g₂) (map φ f).natDegree ((map φ g₁).natDegree + (map φ g₂).natDegree) =
  (map φ f).resultant (map φ g₁) * (map φ f).resultant (map φ g₂)
Tactic: have := IH (g₁.map φ) (g₂.map φ)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R SatisfiesM : Type u_1
inst_1 : CommRing R
inst_2 : CommRing SatisfiesM
φ : R →+* SatisfiesM
hφ : Function.Injective (α := R) (β := SatisfiesM) (⇑φ : (a : R) → SatisfiesM)
f : R[X]
IH :
  ∀ (g₁ g₂ : SatisfiesM[X]),
    (map φ f).resultant (g₁ * g₂) (map φ f).natDegree (g₁.natDegree + g₂.natDegree) =
      (map φ f).resultant g₁ * (map φ f).resultant g₂
g₁ g₂ : R[X]
this :
  (map φ f).resultant (map φ g₁ * map φ g₂) (map φ f).natDegree ((map φ g₁).natDegree + (map φ g₂).natDegree) =
    (map φ f).resultant (map φ g₁) * (map φ f).resultant (map φ g₂)
⊢ Eq (α := SatisfiesM)
    ((φ : (a : R) → SatisfiesM) (f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree)) : SatisfiesM)
    ((φ : (a : R) → SatisfiesM) (f.resultant g₁ * f.resultant g₂) : SatisfiesM)
have this₁ : (map φ f).resultant (map φ (g₁ * g₂)) (map φ f).natDegree ((map φ g₁).natDegree + (map φ g₂).natDegree) =
  (map φ f).resultant (map φ g₁) * (map φ f).resultant (map φ g₂)
Tactic: rw [← Polynomial.map_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
have surjective : ∀ (f' : R[X]) (hf' : map φ f' = f) (e : f'.degree = f.degree),
  f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
Tactic: obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
have surjective : ∀ (g₁' : R[X]) (hg₁ : map φ g₁' = g₁) (e₁ : g₁'.degree = g₁.degree),
  f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
Tactic: obtain ⟨g₁', hg₁, e₁⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₁)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
have surjective : ∀ (g₂' : R[X]) (hg₂ : map φ g₂' = g₂) (e₂ : g₂'.degree = g₂.degree),
  f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
Tactic: obtain ⟨g₂', hg₂, e₂⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₂)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
g₂' : R[X]
hg₂ : map φ g₂' = g₂
e₂ : g₂'.degree = g₂.degree
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
have surjective : (map φ f').resultant (map φ (g₁' * g₂')) (map φ f').natDegree ((map φ g₁').natDegree + (map φ g₂').natDegree) =
  (map φ f').resultant (map φ g₁') * (map φ f').resultant (map φ g₂')
Tactic: rw [← hg₁, ← hg₂, ← hf', ← Polynomial.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
have Splits : ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hff : f.Splits) (g₁ g₂ : R[X]),
  f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
Tactic: induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hff =>
    simp [resultant_eq_prod_eval, natDegree_mul_le, hff]
    ring_nf
  | injective R SatisfiesM φ hφ f IH =>
    apply hφ
    have := IH (g₁.map φ) (g₂.map φ)
    rw [← Polynomial.map_mul] at this
    simpa only [resultant_map_map, ← map_mul, natDegree_map_eq_of_injective hφ] using this
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g₁', hg₁, e₁⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₁)
    obtain ⟨g₂', hg₂, e₂⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₂)
    rw [← hg₁, ← hg₂, ← hf', ← Polynomial.map_mul]
    simp_rw [resultant_map_map, hg₁, hg₂, hf', ← natDegree_eq_natDegree e₁,
      ← natDegree_eq_natDegree e₂, ← natDegree_eq_natDegree e, IH, map_mul]
Cleared hypotheses: f, g₁, g₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
Splits :
  ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hff : f.Splits) (g₁ g₂ : R[X]),
    f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
have injective : ∀ (R SatisfiesM : Type u_1) [inst : CommRing R] [inst_1 : CommRing SatisfiesM] (φ : R →+* SatisfiesM)
  (hφ : Function.Injective (α := R) (β := SatisfiesM) (⇑φ : (a : R) → SatisfiesM)) (f : R[X])
  (IH :
    ∀ (g₁ g₂ : SatisfiesM[X]),
      (map φ f).resultant (g₁ * g₂) (map φ f).natDegree (g₁.natDegree + g₂.natDegree) =
        (map φ f).resultant g₁ * (map φ f).resultant g₂)
  (g₁ g₂ : R[X]), f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
Tactic: induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hff =>
    simp [resultant_eq_prod_eval, natDegree_mul_le, hff]
    ring_nf
  | injective R SatisfiesM φ hφ f IH =>
    apply hφ
    have := IH (g₁.map φ) (g₂.map φ)
    rw [← Polynomial.map_mul] at this
    simpa only [resultant_map_map, ← map_mul, natDegree_map_eq_of_injective hφ] using this
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g₁', hg₁, e₁⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₁)
    obtain ⟨g₂', hg₂, e₂⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₂)
    rw [← hg₁, ← hg₂, ← hf', ← Polynomial.map_mul]
    simp_rw [resultant_map_map, hg₁, hg₂, hf', ← natDegree_eq_natDegree e₁,
      ← natDegree_eq_natDegree e₂, ← natDegree_eq_natDegree e, IH, map_mul]
Cleared hypotheses: f, g₁, g₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
Splits :
  ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hff : f.Splits) (g₁ g₂ : R[X]),
    f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
injective :
  ∀ (R SatisfiesM : Type u_1) [inst : CommRing R] [inst_1 : CommRing SatisfiesM] (φ : R →+* SatisfiesM)
    (hφ : Function.Injective (α := R) (β := SatisfiesM) (⇑φ : (a : R) → SatisfiesM)) (f : R[X])
    (IH :
      ∀ (g₁ g₂ : SatisfiesM[X]),
        (map φ f).resultant (g₁ * g₂) (map φ f).natDegree (g₁.natDegree + g₂.natDegree) =
          (map φ f).resultant g₁ * (map φ f).resultant g₂)
    (g₁ g₂ : R[X]), f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
have surjective : ∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
  (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (f : S[X])
  (IH :
    ∀ (q g₁ g₂ : R[X]),
      q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂)
  (g₁ g₂ : S[X]), f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
Tactic: induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hff =>
    simp [resultant_eq_prod_eval, natDegree_mul_le, hff]
    ring_nf
  | injective R SatisfiesM φ hφ f IH =>
    apply hφ
    have := IH (g₁.map φ) (g₂.map φ)
    rw [← Polynomial.map_mul] at this
    simpa only [resultant_map_map, ← map_mul, natDegree_map_eq_of_injective hφ] using this
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g₁', hg₁, e₁⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₁)
    obtain ⟨g₂', hg₂, e₂⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₂)
    rw [← hg₁, ← hg₂, ← hf', ← Polynomial.map_mul]
    simp_rw [resultant_map_map, hg₁, hg₂, hf', ← natDegree_eq_natDegree e₁,
      ← natDegree_eq_natDegree e₂, ← natDegree_eq_natDegree e, IH, map_mul]
Cleared hypotheses: f, g₁, g₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f₁ f₂ g : R[X]
n : ℕ
hn : g.natDegree ≤ n
⊢ (f₁ * f₂).resultant g (f₁.natDegree + f₂.natDegree) n = f₁.resultant g f₁.natDegree n * f₂.resultant g f₂.natDegree n
have rw : HPow.hPow (α := R) (-1) ((f₁.natDegree + f₂.natDegree) * n) *
    (HPow.hPow (α := R) (-1) (n * f₁.natDegree) * f₁.resultant g f₁.natDegree n * g.resultant f₂ n) =
  f₁.resultant g f₁.natDegree n * (HPow.hPow (α := R) (-1) (f₂.natDegree * n) * g.resultant f₂ n)
Tactic: rw [resultant_comm, resultant_mul_right _ _ _ n hn, resultant_comm, resultant_comm f₂]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f₁ f₂ g : R[X]
n : ℕ
hn : g.natDegree ≤ n
⊢ HPow.hPow (α := R) (-1) ((f₁.natDegree + f₂.natDegree) * n) *
      (HPow.hPow (α := R) (-1) (n * f₁.natDegree) * f₁.resultant g f₁.natDegree n * g.resultant f₂ n) =
    f₁.resultant g f₁.natDegree n * (HPow.hPow (α := R) (-1) (f₂.natDegree * n) * g.resultant f₂ n)
have ring_nf : f₁.resultant g f₁.natDegree n * g.resultant f₂ n * HPow.hPow (α := R) (-1) (f₁.natDegree * n * 2) *
    HPow.hPow (α := R) (-1) (f₂.natDegree * n) =
  f₁.resultant g f₁.natDegree n * g.resultant f₂ n * HPow.hPow (α := R) (-1) (f₂.natDegree * n)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
hf : f.Splits
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree
have pos : ∀ (h : f.natDegree = 0), f.resultant f = HPow.hPow (α := R) 0 f.natDegree
Tactic: by_cases h : f.natDegree = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
hf : f.Splits
pos : ∀ (h : f.natDegree = 0), f.resultant f = HPow.hPow (α := R) 0 f.natDegree
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree
have neg : ∀ (h : ¬f.natDegree = 0), f.resultant f = HPow.hPow (α := R) 0 f.natDegree
Tactic: by_cases h : f.natDegree = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
hf : f.Splits
h : f.natDegree = 0
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree
have pos : ∀ (r : R) (hf : Splits.{u_1} (R := R) ((C : (a : R) → R[X]) r))
  (h : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r) = 0),
  resultant ((C : (a : R) → R[X]) r) ((C : (a : R) → R[X]) r) =
    HPow.hPow (α := R) 0 (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r))
Tactic: obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp h
Cleared hypotheses: f, hf, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
hf : f.Splits
h : ¬f.natDegree = 0
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree
have neg : f.leadingCoeff ^ f.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x f) f.roots) =
  HPow.hPow (α := R) 0 f.natDegree
Tactic: rw [resultant_eq_prod_eval _ _ _ le_rfl hf]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
IH : (map φ f).resultant (map φ f) = HPow.hPow (α := S) 0 (map φ f).natDegree
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree
have injective : Eq (α := S) ((φ : (a : R) → S) (f.resultant f) : S) ((φ : (a : R) → S) (HPow.hPow (α := R) 0 f.natDegree) : S)
Tactic: apply hφ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree
⊢ f.resultant f = HPow.hPow (α := S) 0 f.natDegree
have surjective : ∀ (f' : R[X]) (hf' : map φ f' = f) (e : f'.degree = f.degree), f.resultant f = HPow.hPow (α := S) 0 f.natDegree
Tactic: obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
⊢ f.resultant f = HPow.hPow (α := S) 0 f.natDegree
have surjective : (map φ f').resultant (map φ f') = HPow.hPow (α := S) 0 (map φ f').natDegree
Tactic: rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
surjective : (map φ f').resultant (map φ f') = HPow.hPow (α := S) 0 (map φ f').natDegree
⊢ f.resultant f = HPow.hPow (α := S) 0 f.natDegree
have surjective₁ : (φ : (a : R) → S) (f'.resultant f' (map φ f').natDegree (map φ f').natDegree) =
  HPow.hPow (α := S) 0 (map φ f').natDegree
Tactic: rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
surjective : (map φ f').resultant (map φ f') = HPow.hPow (α := S) 0 (map φ f').natDegree
surjective₁ :
  (φ : (a : R) → S) (f'.resultant f' (map φ f').natDegree (map φ f').natDegree) =
    HPow.hPow (α := S) 0 (map φ f').natDegree
⊢ f.resultant f = HPow.hPow (α := S) 0 f.natDegree
have surjective₂ : (φ : (a : R) → S) (f'.resultant f' f.natDegree f.natDegree) = HPow.hPow (α := S) 0 f.natDegree
Tactic: rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
surjective : (map φ f').resultant (map φ f') = HPow.hPow (α := S) 0 (map φ f').natDegree
surjective₁ :
  (φ : (a : R) → S) (f'.resultant f' (map φ f').natDegree (map φ f').natDegree) =
    HPow.hPow (α := S) 0 (map φ f').natDegree
surjective₂ : (φ : (a : R) → S) (f'.resultant f' f.natDegree f.natDegree) = HPow.hPow (α := S) 0 f.natDegree
⊢ f.resultant f = HPow.hPow (α := S) 0 f.natDegree
have surjective₃ : (φ : (a : R) → S) (f'.resultant f') = HPow.hPow (α := S) 0 f'.natDegree
Tactic: rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]