awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
inr :
  ∀ (this : f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g),
    ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
rw : a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
rw [← resultant_add_mul_right _ _ a _ _ _ le_rfl, add_comm, mul_comm f, e,
    resultant_one_right] at this

Premises used: Polynomial.resultant_one_right, le_rfl, add_comm, Polynomial.resultant_add_mul_right, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
⟨_, _, this.trans (mul_comm _ _)⟩

Premises used: Exists.intro, mul_comm, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
exact ⟨_, _, this.trans (mul_comm _ _)⟩
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
by_contra! : ∀ (H : b.natDegree + g.natDegree < a.natDegree + f.natDegree), False
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree

Tactic:
by_contra! H
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H_1 : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : b.natDegree + g.natDegree < a.natDegree + f.natDegree
⊢ (b * g).natDegree < (a * f).natDegree

Tactic:
rw [← natDegree_mul ha hf, ← natDegree_mul hb hg] at H

Premises used: Polynomial.natDegree_mul
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H_1 : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : (b * g).natDegree < (a * f).natDegree
⊢ (a * f + b * g).natDegree = (a * f).natDegree

Tactic:
have := natDegree_add_eq_left_of_natDegree_lt H
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H_1 : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this_1 : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : (b * g).natDegree < (a * f).natDegree
this : (a * f + b * g).natDegree = (a * f).natDegree
⊢ 0 = (a * f).natDegree

Tactic:
simp only [e, natDegree_one] at this

Premises used: Polynomial.natDegree_one
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H_1 : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this_1 : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : (b * g).natDegree < (a * f).natDegree
this : 0 = (a * f).natDegree
⊢ False

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
inl : ∀ (H : IsCoprime 0 g), resultant 0 g ≠ 0
inr : ∀ (hf : f ≠ 0), f.resultant g ≠ 0
⊢ f.resultant g ≠ 0

Tactic:
obtain rfl | hf := eq_or_ne f 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
H : ∃ (r : R), IsUnit r ∧ (C : (a : R) → R[X]) r = g
⊢ resultant 0 g ≠ 0

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
e : f.resultant g = 0
⊢ False

Tactic:
simpa [e, hf] using resultant_dvd_leadingCoeff_pow f g H

Premises used: Polynomial.resultant_dvd_leadingCoeff_pow
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
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:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 a s, (f i).leadingCoeff) 0
⊢ Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 a s, (f i).leadingCoeff) 0
⊢ Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0

Tactic:
have hf' : ∏ i ∈ s, (f i).leadingCoeff ≠ 0 := by aesop
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 a s, (f i).leadingCoeff) 0
hf' : Ne.{u_1 + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
⊢ (f a).leadingCoeff * leadingCoeff (∏ x ∈ s, f x) ≠ 0

Tactic:
simpa [*, leadingCoeff_prod'] using hf

Premises used: Polynomial.leadingCoeff_prod'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
insert₄ 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
⊢ 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

Tactic:
rw [Finset.prod_insert has, natDegree_mul' (by simpa [*, leadingCoeff_prod'] using hf),
      resultant_mul_left _ _ _ _ hn, IH hf', Finset.prod_insert has]

Premises used: Finset.prod_insert, Polynomial.natDegree_mul', Polynomial.resultant_mul_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
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.insert a s, (f i).leadingCoeff) 0),
    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
⊢ 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

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]

Premises used: Polynomial.natDegree_mul', Insert.insert, Polynomial.resultant_mul_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
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
⊢ f.resultant (∏ i ∈ s, g i) m = ∏ i ∈ s, f.resultant (g i) m

Tactic:
simp_rw [resultant_comm f]

Premises used: Polynomial.resultant_comm
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
rw₄ 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
⊢ 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:
rw [resultant_prod_left _ _ _ _ hg hm, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum,
    ← Finset.mul_sum, natDegree_prod' _ _ hg]

Premises used: Finset.mul_sum, Finset.prod_mul_distrib, Polynomial.natDegree_prod', Finset.prod_pow_eq_pow_sum, Polynomial.resultant_prod_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
hf : f.leadingCoeff ^ m ≠ 0
hn : g.natDegree ≤ n
⊢ Ne.{u_1 + 1} (α := R) (∏ i ∈ Finset.range m, leadingCoeff ((fun (x : ℕ) ↦ f) i)) 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
h₁ : f.resultant g f.natDegree n ^ m = ∏ i ∈ Finset.range m, f.resultant g f.natDegree n
⊢ (f ^ m).resultant g (f ^ m).natDegree n = f.resultant g f.natDegree n ^ m

Tactic:
convert! resultant_prod_left (Finset.range m) (fun _ ↦ f) g n (by simpa) hn

Premises used: Finset.range, Polynomial.resultant_prod_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 = ∏ i ∈ Finset.range m, f

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
hf : f.leadingCoeff ^ m ≠ 0
hn : g.natDegree ≤ n
⊢ f.resultant g f.natDegree n ^ m = ∏ i ∈ Finset.range m, f.resultant g f.natDegree n

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
hm : f.natDegree ≤ m
hg : g.leadingCoeff ^ n ≠ 0
⊢ Ne.{u_1 + 1} (α := R) (∏ i ∈ Finset.range n, leadingCoeff ((fun (x : ℕ) ↦ g) i)) 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
h₁ : f.resultant g m ^ n = ∏ i ∈ Finset.range n, f.resultant g m
⊢ f.resultant (g ^ n) m = f.resultant g m ^ n

Tactic:
convert! resultant_prod_right (Finset.range n) f (fun _ ↦ g) m hm (by simpa)

Premises used: Finset.range, Polynomial.resultant_prod_right
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
hm : f.natDegree ≤ m
hg : g.leadingCoeff ^ n ≠ 0
⊢ g ^ n = ∏ i ∈ Finset.range n, g

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 m ^ n = ∏ i ∈ Finset.range n, f.resultant g m

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ m).natDegree n =
    (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 ^
      m

Tactic:
resultant_pow_left _ _ _ _ _ _

Premises used: Polynomial.resultant_pow_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
convert_7 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).leadingCoeff ^ m ≠ 0
convert_8 : 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

Tactic:
convert! resultant_pow_left _ _ _ _ _ _

Premises used: Polynomial.resultant_pow_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
h : Nontrivial R
⊢ m = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ m).natDegree

Tactic:
simp [natDegree_pow', hn]

Premises used: Polynomial.natDegree_pow'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
h : Nontrivial R
⊢ 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:
simp [natDegree_pow', hn]

Premises used: Polynomial.natDegree_pow'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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])).leadingCoeff ^ m ≠ 0

Tactic:
simp [natDegree_pow', hn]

Premises used: Polynomial.natDegree_pow'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
h : Nontrivial R
⊢ g.natDegree ≤ n

Tactic:
simp [natDegree_pow', hn]

Premises used: Polynomial.natDegree_pow'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
rw₁ rw₂ : HPow.hPow (α := R) (-1) (m * n) * eval r f ^ n = 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

Tactic:
rw [resultant_comm, resultant_X_sub_C_pow_left _ _ _ _ hm]

Premises used: Polynomial.resultant_comm, Polynomial.resultant_X_sub_C_pow_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ^ m).resultant g m n = eval 0 g ^ m

Tactic:
resultant_X_sub_C_pow_left 0 g m n hn

Premises used: Polynomial.resultant_X_sub_C_pow_left, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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)
h₁ : g.coeff 0 = eval 0 g
⊢ (HPow.hPow (α := R[X]) X m).resultant g m n = g.coeff 0 ^ m

Tactic:
convert! resultant_X_sub_C_pow_left 0 g m n hn

Premises used: Polynomial.resultant_X_sub_C_pow_left, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ X = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)

Tactic:
simp [coeff_zero_eq_eval_zero]

Premises used: Polynomial.coeff_zero_eq_eval_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ g.coeff 0 = eval 0 g

Tactic:
simp [coeff_zero_eq_eval_zero]

Premises used: Polynomial.coeff_zero_eq_eval_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ f.resultant (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ^ n) m n =
    HPow.hPow (α := R) (-1) (m * n) * eval 0 f ^ n

Tactic:
resultant_X_sub_C_pow_right f 0 m n hm

Premises used: Polynomial.resultant_X_sub_C_pow_right, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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)
h₁ : f.coeff 0 = eval 0 f
⊢ f.resultant (HPow.hPow (α := R[X]) X n) m n = HPow.hPow (α := R) (-1) (m * n) * f.coeff 0 ^ n

Tactic:
convert! resultant_X_sub_C_pow_right f 0 m n hm

Premises used: Polynomial.resultant_X_sub_C_pow_right, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ X = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)

Tactic:
simp [coeff_zero_eq_eval_zero]

Premises used: Polynomial.coeff_zero_eq_eval_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ f.coeff 0 = eval 0 f

Tactic:
simp [coeff_zero_eq_eval_zero]

Premises used: Polynomial.coeff_zero_eq_eval_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
rw :
  (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) = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
rw [natDegree_scaleRoots, natDegree_scaleRoots]

Premises used: Polynomial.natDegree_scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
inr :
  ∀ (hf : f ≠ 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

Tactic:
obtain rfl | hf := eq_or_ne f 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
r : R
⊢ 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:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
inr₁ :
  ∀ (hg : g ≠ 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

Tactic:
obtain rfl | hg := eq_or_ne g 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
r : R
hf : f ≠ 0
⊢ (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:
simp