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
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∀ (hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0),
    resultant (∏ i ∈ s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ s, f i)) n =
      ∏ i ∈ s, (f i).resultant g (f i).natDegree n
hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ Insert.insert a s, (f i).leadingCoeff) 0
hf' : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
insert :
  (f a * ∏ x ∈ s, f x).resultant g (f a * ∏ x ∈ s, f x).natDegree n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
insert₁ :
  (f a * ∏ x ∈ s, f x).resultant g ((f a).natDegree + natDegree.{u_1} (R := R) (∏ x ∈ s, f x)) n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
insert₂ :
  (f a).resultant g (f a).natDegree n * resultant (∏ x ∈ s, f x) g (natDegree.{u_1} (R := R) (∏ x ∈ s, f x)) n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
insert₃ :
  (f a).resultant g (f a).natDegree n * ∏ i ∈ s, (f i).resultant g (f i).natDegree n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
⊢ resultant (∏ i ∈ Insert.insert a s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ Insert.insert a s, f i)) n =
    ∏ i ∈ Insert.insert a s, (f i).resultant g (f i).natDegree n
have insert₄ : (f a).resultant g (f a).natDegree n * ∏ i ∈ s, (f i).resultant g (f i).natDegree n =
  (f a).resultant g (f a).natDegree n * ∏ x ∈ s, (f x).resultant g (f x).natDegree n
Tactic: rw [Finset.prod_insert has, natDegree_mul' (by simpa [*, leadingCoeff_prod'] using hf),
      resultant_mul_left _ _ _ _ hn, IH hf', Finset.prod_insert has]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
s : Finset ι
f : ι → R[X]
g : R[X]
n : ℕ
hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
hn : g.natDegree ≤ n
⊢ resultant (∏ i ∈ s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ s, f i)) n = ∏ i ∈ s, (f i).resultant g (f i).natDegree n
have empty : ∀ (hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ ∅, (f i).leadingCoeff) 0),
  resultant (∏ i ∈ ∅, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ ∅, f i)) n = ∏ i ∈ ∅, (f i).resultant g (f i).natDegree n
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s has IH =>
    have hf' : ∏ i ∈ s, (f i).leadingCoeff ≠ 0 := by aesop
    rw [Finset.prod_insert has, natDegree_mul' (by simpa [*, leadingCoeff_prod'] using hf),
      resultant_mul_left _ _ _ _ hn, IH hf', Finset.prod_insert has]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
s : Finset ι
f : ι → R[X]
g : R[X]
n : ℕ
hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
hn : g.natDegree ≤ n
empty :
  ∀ (hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ ∅, (f i).leadingCoeff) 0),
    resultant (∏ i ∈ ∅, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ ∅, f i)) n =
      ∏ i ∈ ∅, (f i).resultant g (f i).natDegree n
⊢ resultant (∏ i ∈ s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ s, f i)) n = ∏ i ∈ s, (f i).resultant g (f i).natDegree n
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (IH :
    ∀ (hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0),
      resultant (∏ i ∈ s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ s, f i)) n =
        ∏ i ∈ s, (f i).resultant g (f i).natDegree n)
  (hf : Ne.{u_1 + 1} (α := R) (∏ i ∈ insert a s, (f i).leadingCoeff) 0),
  resultant (∏ i ∈ insert a s, f i) g (natDegree.{u_1} (R := R) (∏ i ∈ insert a s, f i)) n =
    ∏ i ∈ insert a s, (f i).resultant g (f i).natDegree n
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s has IH =>
    have hf' : ∏ i ∈ s, (f i).leadingCoeff ≠ 0 := by aesop
    rw [Finset.prod_insert has, natDegree_mul' (by simpa [*, leadingCoeff_prod'] using hf),
      resultant_mul_left _ _ _ _ hn, IH hf', Finset.prod_insert has]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
m : ℕ
hm : f.natDegree ≤ m
hg : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (g i).leadingCoeff) 0
⊢ f.resultant (∏ i ∈ s, g i) m = ∏ i ∈ s, f.resultant (g i) m
have simp_rw : HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) *
    resultant (∏ i ∈ s, g i) f (natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) m =
  ∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
Tactic: simp_rw [resultant_comm f]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
m : ℕ
hm : f.natDegree ≤ m
hg : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (g i).leadingCoeff) 0
⊢ HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) *
      resultant (∏ i ∈ s, g i) f (natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) m =
    ∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
have rw : HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
  ∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
Tactic: rw [resultant_prod_left _ _ _ _ hg hm, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum,
    ← Finset.mul_sum, natDegree_prod' _ _ hg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
m : ℕ
hm : f.natDegree ≤ m
hg : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (g i).leadingCoeff) 0
rw :
  HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
    ∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
⊢ HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) *
      resultant (∏ i ∈ s, g i) f (natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) m =
    ∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
have rw₁ : HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
  HMul.hMul (α := R) (∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree))
    (∏ x ∈ s, (g x).resultant f (g x).natDegree m)
Tactic: rw [resultant_prod_left _ _ _ _ hg hm, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum,
    ← Finset.mul_sum, natDegree_prod' _ _ hg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
m : ℕ
hm : f.natDegree ≤ m
hg : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (g i).leadingCoeff) 0
rw :
  HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
    ∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
rw₁ :
  HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
    HMul.hMul (α := R) (∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree))
      (∏ x ∈ s, (g x).resultant f (g x).natDegree m)
⊢ HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) *
      resultant (∏ i ∈ s, g i) f (natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) m =
    ∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
have rw₂ : HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
  HPow.hPow (α := R) (β := ℕ) (-1) (∑ i ∈ s, m * (g i).natDegree) * ∏ x ∈ s, (g x).resultant f (g x).natDegree m
Tactic: rw [resultant_prod_left _ _ _ _ hg hm, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum,
    ← Finset.mul_sum, natDegree_prod' _ _ hg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
m : ℕ
hm : f.natDegree ≤ m
hg : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (g i).leadingCoeff) 0
rw :
  HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
    ∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
rw₁ :
  HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
    HMul.hMul (α := R) (∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree))
      (∏ x ∈ s, (g x).resultant f (g x).natDegree m)
rw₂ :
  HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
    HPow.hPow (α := R) (β := ℕ) (-1) (∑ i ∈ s, m * (g i).natDegree) * ∏ x ∈ s, (g x).resultant f (g x).natDegree m
⊢ HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) *
      resultant (∏ i ∈ s, g i) f (natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) m =
    ∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
have rw₃ : HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
  HPow.hPow (α := R) (-1) (m * ∑ i ∈ s, (g i).natDegree) * ∏ x ∈ s, (g x).resultant f (g x).natDegree m
Tactic: rw [resultant_prod_left _ _ _ _ hg hm, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum,
    ← Finset.mul_sum, natDegree_prod' _ _ hg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
m : ℕ
hm : f.natDegree ≤ m
hg : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (g i).leadingCoeff) 0
rw :
  HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
    ∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
rw₁ :
  HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
    HMul.hMul (α := R) (∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree))
      (∏ x ∈ s, (g x).resultant f (g x).natDegree m)
rw₂ :
  HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
    HPow.hPow (α := R) (β := ℕ) (-1) (∑ i ∈ s, m * (g i).natDegree) * ∏ x ∈ s, (g x).resultant f (g x).natDegree m
rw₃ :
  HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
    HPow.hPow (α := R) (-1) (m * ∑ i ∈ s, (g i).natDegree) * ∏ x ∈ s, (g x).resultant f (g x).natDegree m
⊢ HPow.hPow (α := R) (-1) (m * natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) *
      resultant (∏ i ∈ s, g i) f (natDegree.{u_1} (R := R) (∏ i ∈ s, g i)) m =
    ∏ x ∈ s, HPow.hPow (α := R) (-1) (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
have rw₄ : HPow.hPow (α := R) (-1) (m * ∑ i ∈ s, (g i).natDegree) * ∏ i ∈ s, (g i).resultant f (g i).natDegree m =
  HPow.hPow (α := R) (-1) (m * ∑ i ∈ s, (g i).natDegree) * ∏ x ∈ s, (g x).resultant f (g x).natDegree m
Tactic: rw [resultant_prod_left _ _ _ _ hg hm, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum,
    ← Finset.mul_sum, natDegree_prod' _ _ hg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
hf : f.leadingCoeff ^ m ≠ 0
hn : g.natDegree ≤ n
⊢ (f ^ m).resultant g (f ^ m).natDegree n = f.resultant g f.natDegree n ^ m
have h : f ^ m = ∏ i ∈ Finset.range m, f
Tactic: convert! resultant_prod_left (Finset.range m) (fun _ ↦ f) g n (by simpa) hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
hf : f.leadingCoeff ^ m ≠ 0
hn : g.natDegree ≤ n
h : f ^ m = ∏ i ∈ Finset.range m, f
⊢ (f ^ m).resultant g (f ^ m).natDegree n = f.resultant g f.natDegree n ^ m
have h₁ : f.resultant g f.natDegree n ^ m = ∏ i ∈ Finset.range m, f.resultant g f.natDegree n
Tactic: convert! resultant_prod_left (Finset.range m) (fun _ ↦ f) g n (by simpa) hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
hm : f.natDegree ≤ m
hg : g.leadingCoeff ^ n ≠ 0
⊢ f.resultant (g ^ n) m = f.resultant g m ^ n
have h : g ^ n = ∏ i ∈ Finset.range n, g
Tactic: convert! resultant_prod_right (Finset.range n) f (fun _ ↦ g) m hm (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
hm : f.natDegree ≤ m
hg : g.leadingCoeff ^ n ≠ 0
h : g ^ n = ∏ i ∈ Finset.range n, g
⊢ f.resultant (g ^ n) m = f.resultant g m ^ n
have h₁ : f.resultant g m ^ n = ∏ i ∈ Finset.range n, f.resultant g m
Tactic: convert! resultant_prod_right (Finset.range n) f (fun _ ↦ g) m hm (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ m).resultant g m n = eval r g ^ m
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
h : Nontrivial R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ m).resultant g m n = eval r g ^ m
have h : m = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ m).natDegree
Tactic: convert! resultant_pow_left _ _ _ _ _ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
h_1 : Nontrivial R
h : m = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ m).natDegree
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ m).resultant g m n = eval r g ^ m
have h₁ : eval r g =
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree n
Tactic: convert! resultant_pow_left _ _ _ _ _ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
h_1 : Nontrivial R
h : m = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ m).natDegree
h₁ :
  eval r g =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree n
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ m).resultant g m n = eval r g ^ m
have convert_7 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).leadingCoeff ^ m ≠ 0
Tactic: convert! resultant_pow_left _ _ _ _ _ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
r : R
m n : ℕ
hm : f.natDegree ≤ m
⊢ f.resultant (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ n) m n =
    HPow.hPow (α := R) (-1) (m * n) * eval r f ^ n
have rw : HPow.hPow (α := R) (-1) (m * n) *
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ n).resultant f n m =
  HPow.hPow (α := R) (-1) (m * n) * eval r f ^ n
Tactic: rw [resultant_comm, resultant_X_sub_C_pow_left _ _ _ _ hm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
r : R
m n : ℕ
hm : f.natDegree ≤ m
rw :
  HPow.hPow (α := R) (-1) (m * n) *
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ n).resultant f n m =
    HPow.hPow (α := R) (-1) (m * n) * eval r f ^ n
⊢ f.resultant (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ n) m n =
    HPow.hPow (α := R) (-1) (m * n) * eval r f ^ n
have rw₁ : HPow.hPow (α := R) (-1) (m * n) * eval r f ^ n = HPow.hPow (α := R) (-1) (m * n) * eval r f ^ n
Tactic: rw [resultant_comm, resultant_X_sub_C_pow_left _ _ _ _ hm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ (HPow.hPow (α := R[X]) X m).resultant g m n = g.coeff 0 ^ m
have h : X = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)
Tactic: convert! resultant_X_sub_C_pow_left 0 g m n hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
h : X = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)
⊢ (HPow.hPow (α := R[X]) X m).resultant g m n = g.coeff 0 ^ m
have h₁ : g.coeff 0 = eval 0 g
Tactic: convert! resultant_X_sub_C_pow_left 0 g m n hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ f.resultant (HPow.hPow (α := R[X]) X n) m n = HPow.hPow (α := R) (-1) (m * n) * f.coeff 0 ^ n
have h : X = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)
Tactic: convert! resultant_X_sub_C_pow_right f 0 m n hm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
h : X = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)
⊢ f.resultant (HPow.hPow (α := R[X]) X n) m n = HPow.hPow (α := R) (-1) (m * n) * f.coeff 0 ^ n
have h₁ : f.coeff 0 = eval 0 f
Tactic: convert! resultant_X_sub_C_pow_right f 0 m n hm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) = r ^ (f.natDegree * g.natDegree) * f.resultant g
have rw : (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: rw [natDegree_scaleRoots, natDegree_scaleRoots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have inl : resultant (scaleRoots 0 r) (g.scaleRoots r) (natDegree.{u_1} (R := R) 0) g.natDegree =
  r ^ (natDegree.{u_1} (R := R) 0 * g.natDegree) * resultant 0 g
Tactic: obtain rfl | hf := eq_or_ne f 0
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
inl :
  resultant (scaleRoots 0 r) (g.scaleRoots r) (natDegree.{u_1} (R := R) 0) g.natDegree =
    r ^ (natDegree.{u_1} (R := R) 0 * g.natDegree) * resultant 0 g
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have inr : ∀ (hf : f ≠ 0),
  (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: obtain rfl | hf := eq_or_ne f 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
hf : f ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have inr : (f.scaleRoots r).resultant (scaleRoots 0 r) f.natDegree (natDegree.{u_1} (R := R) 0) =
  r ^ (f.natDegree * natDegree.{u_1} (R := R) 0) * f.resultant 0
Tactic: obtain rfl | hg := eq_or_ne g 0
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
hf : f ≠ 0
inr :
  (f.scaleRoots r).resultant (scaleRoots 0 r) f.natDegree (natDegree.{u_1} (R := R) 0) =
    r ^ (f.natDegree * natDegree.{u_1} (R := R) 0) * f.resultant 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have inr₁ : ∀ (hg : g ≠ 0),
  (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: obtain rfl | hg := eq_or_ne g 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
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have pos : ∀ (hf0 : f.natDegree = 0),
  (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: by_cases hf0 : 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
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
pos :
  ∀ (hf0 : f.natDegree = 0),
    (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree =
      r ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have neg : ∀ (hf0 : ¬f.natDegree = 0),
  (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: by_cases hf0 : 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
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : f.natDegree = 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have pos : ∀ (a : R) (hf' : Splits.{u_1} (R := R) ((C : (a : R) → R[X]) a))
  (hf : Ne (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X]))
  (hf0 : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) = 0),
  resultant (scaleRoots ((C : (a : R) → R[X]) a) r) (g.scaleRoots r) (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a))
      g.natDegree =
    r ^ (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) * g.natDegree) * resultant ((C : (a : R) → R[X]) a) g
Tactic: obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hf0
Cleared hypotheses: f, hf', hf, hf0
-- 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
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have pos : ∀ (hg0 : g.natDegree = 0),
  (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: by_cases hg0 : g.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
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
pos :
  ∀ (hg0 : g.natDegree = 0),
    (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree =
      r ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have neg : ∀ (hg0 : ¬g.natDegree = 0),
  (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: by_cases hg0 : g.natDegree = 0