awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
neg :
  ∀ (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

Tactic:
by_cases hf0 : f.natDegree = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 :
  ∀ (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
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hf0

Premises used: Iff.mp, Polynomial.natDegree_eq_zero, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
g : R[X]
r : R
hg : g ≠ 0
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:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
neg :
  ∀ (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

Tactic:
by_cases hg0 : g.natDegree = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg0 : g.natDegree = 0
pos :
  ∀ (a : R) (hg : Ne (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X]))
    (hg0 : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) = 0),
    (f.scaleRoots r).resultant (scaleRoots ((C : (a : R) → R[X]) a) r) f.natDegree
        (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a)) =
      r ^ (f.natDegree * natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a)) * f.resultant ((C : (a : R) → R[X]) a)
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hg0

Premises used: Iff.mp, Polynomial.natDegree_eq_zero, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
hf' : f.Splits
r : R
hf : f ≠ 0
hf0 : ¬f.natDegree = 0
a : R
hg : Ne (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X])
hg0 : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) = 0
⊢ (f.scaleRoots r).resultant (scaleRoots ((C : (a : R) → R[X]) a) r) f.natDegree
      (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a)) =
    r ^ (f.natDegree * natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a)) * f.resultant ((C : (a : R) → R[X]) a)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg0 : ¬g.natDegree = 0
neg :
  (f.scaleRoots 0).resultant (g.scaleRoots 0) f.natDegree g.natDegree =
    HPow.hPow (α := R) 0 (f.natDegree * g.natDegree) * f.resultant g
neg₁ :
  ∀ (hr : r ≠ 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 | hr := eq_or_ne r 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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]
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
neg :
  (HMul.hMul (α := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) f.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X f.natDegree)).resultant
      (HMul.hMul (α := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) g.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X g.natDegree))
      f.natDegree g.natDegree =
    HPow.hPow (α := R) 0 (f.natDegree * g.natDegree) * f.resultant g
⊢ (f.scaleRoots 0).resultant (g.scaleRoots 0) f.natDegree g.natDegree =
    HPow.hPow (α := R) 0 (f.natDegree * g.natDegree) * f.resultant g

Tactic:
rw [scaleRoots_zero, scaleRoots_zero, Algebra.smul_def, Algebra.smul_def]

Premises used: Algebra.smul_def, Polynomial.scaleRoots_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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]
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ (HMul.hMul (α := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) f.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X f.natDegree)).resultant
      (HMul.hMul (α := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) g.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X g.natDegree))
      f.natDegree g.natDegree =
    HPow.hPow (α := R) 0 (f.natDegree * g.natDegree) * f.resultant g

Tactic:
simp [resultant_C_mul_right, resultant_X_pow_right, *, (Ne.symm hf0)]

Premises used: Polynomial.resultant_X_pow_right, Ne.symm, Polynomial.resultant_C_mul_right
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
rw : (f.scaleRoots r).resultant (g.scaleRoots r) (f.scaleRoots r).natDegree
| (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree

Tactic:
rw [← natDegree_scaleRoots f r, ← natDegree_scaleRoots g r]

Premises used: Polynomial.natDegree_scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
neg :
  (f.scaleRoots r).resultant (g.scaleRoots r) (f.scaleRoots r).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:
conv_lhs => rw [← natDegree_scaleRoots f r, ← natDegree_scaleRoots g r]

Premises used: Polynomial.natDegree_scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
neg :
  (f.scaleRoots r).leadingCoeff ^ (g.scaleRoots r).natDegree *
      Multiset.prod
        (Multiset.map (fun (x : R) ↦ eval x (g.scaleRoots r)) (Multiset.map (fun (x : R) ↦ r * x) f.roots)) =
    r ^ (f.natDegree * g.natDegree) *
      (f.leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) (f.scaleRoots r).natDegree =
    r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
rw [resultant_eq_prod_eval _ _ _ le_rfl hf',
      resultant_eq_prod_eval _ _ _ le_rfl (hf'.scaleRoots _),
      roots_scaleRoots _ (isUnit_iff_ne_zero.mpr hr)]

Premises used: Iff.mpr, Polynomial.roots_scaleRoots, le_rfl, Polynomial.resultant_eq_prod_eval, isUnit_iff_ne_zero, Polynomial.Splits.scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
neg :
  (f.scaleRoots r).leadingCoeff ^ (g.scaleRoots r).natDegree *
      Multiset.prod (Multiset.map (fun (x : R) ↦ r ^ g.natDegree * eval x g) f.roots) =
    r ^ (f.natDegree * g.natDegree) *
      (f.leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
⊢ (f.scaleRoots r).leadingCoeff ^ (g.scaleRoots r).natDegree *
      Multiset.prod
        (Multiset.map (fun (x : R) ↦ eval x (g.scaleRoots r)) (Multiset.map (fun (x : R) ↦ r * x) f.roots)) =
    r ^ (f.natDegree * g.natDegree) *
      (f.leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))

Tactic:
simp only [Multiset.map_map, Function.comp_def, scaleRoots_eval_mul]

Premises used: Function.comp_def, Multiset.map_map, Polynomial.scaleRoots_eval_mul
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
neg :
  f.leadingCoeff ^ g.natDegree *
      ((r ^ g.natDegree) ^ f.natDegree * Multiset.prod (Multiset.map (fun (i : R) ↦ eval i g) f.roots)) =
    r ^ (f.natDegree * g.natDegree) *
      (f.leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
⊢ (f.scaleRoots r).leadingCoeff ^ (g.scaleRoots r).natDegree *
      Multiset.prod (Multiset.map (fun (x : R) ↦ r ^ g.natDegree * eval x g) f.roots) =
    r ^ (f.natDegree * g.natDegree) *
      (f.leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))

Tactic:
simp only [leadingCoeff_scaleRoots, natDegree_scaleRoots, Multiset.prod_map_mul,
      Multiset.map_const', Multiset.prod_replicate, ← hf'.natDegree_eq_card_roots]

Premises used: Multiset.prod_replicate, Polynomial.natDegree_scaleRoots, Multiset.prod_map_mul, Polynomial.Splits.natDegree_eq_card_roots, Polynomial.leadingCoeff_scaleRoots, Multiset.map_const'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ f.leadingCoeff ^ g.natDegree *
      ((r ^ g.natDegree) ^ f.natDegree * Multiset.prod (Multiset.map (fun (i : R) ↦ eval i g) f.roots)) =
    r ^ (f.natDegree * g.natDegree) *
      (f.leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
⊢ map φ f ≠ 0

Tactic:
simpa using (map_injective _ hφ).ne hf

Premises used: Function.Injective.ne, Polynomial.map_injective
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
⊢ map φ g ≠ 0

Tactic:
simpa using (map_injective _ hφ).ne hg

Premises used: Function.Injective.ne, Polynomial.map_injective
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
⊢ ((map φ f).scaleRoots ((φ : (a : R) → S) r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r))
      (map φ f).natDegree (map φ g).natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
      (map φ f).resultant (map φ g)

Tactic:
have := IH (g.map φ) (φ r) (by simpa using (map_injective _ hφ).ne hf)
      (by simpa using (map_injective _ hφ).ne hg)
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots ((φ : (a : R) → S) r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r))
      (map φ f).natDegree (map φ g).natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
      (map φ f).resultant (map φ g)
inr :
  Eq (α := S) ((φ : (a : R) → S) ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) : S)
    ((φ : (a : R) → S) (r ^ (f.natDegree * g.natDegree) * f.resultant g) : S)
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
apply hφ
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots ((φ : (a : R) → S) r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r))
      (map φ f).natDegree (map φ g).natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
      (map φ f).resultant (map φ g)
inr :
  ∀
    (this :
      (map φ (f.scaleRoots r)).resultant (map φ (g.scaleRoots r)) (map φ f).natDegree (map φ g).natDegree =
        HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
          (map φ f).resultant (map φ g)),
    Eq (α := S) ((φ : (a : R) → S) ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) : S)
      ((φ : (a : R) → S) (r ^ (f.natDegree * g.natDegree) * f.resultant g) : S)
inr₁ :
  ∀
    (this :
      (map φ (f.scaleRoots r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r)) (map φ f).natDegree
          (map φ g).natDegree =
        HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
          (map φ f).resultant (map φ g)),
    Ne (α := S) ((φ : (a : R) → S) g.leadingCoeff : S) (0 : S)
inr₂ : Ne (α := S) ((φ : (a : R) → S) f.leadingCoeff : S) (0 : S)
⊢ Eq (α := S) ((φ : (a : R) → S) ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) : S)
    ((φ : (a : R) → S) (r ^ (f.natDegree * g.natDegree) * f.resultant g) : S)

Tactic:
rw [← map_scaleRoots, ← map_scaleRoots] at this

Premises used: Polynomial.map_scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  (map φ (f.scaleRoots r)).resultant (map φ (g.scaleRoots r)) (map φ f).natDegree (map φ g).natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
      (map φ f).resultant (map φ g)
⊢ Eq (α := S) ((φ : (a : R) → S) ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) : S)
    ((φ : (a : R) → S) (r ^ (f.natDegree * g.natDegree) * f.resultant g) : S)

Tactic:
simpa [natDegree_map_eq_of_injective hφ] using this

Premises used: Polynomial.natDegree_map_eq_of_injective
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  (map φ (f.scaleRoots r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r)) (map φ f).natDegree
      (map φ g).natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
      (map φ f).resultant (map φ g)
⊢ Ne (α := S) ((φ : (a : R) → S) g.leadingCoeff : S) (0 : S)

Tactic:
simpa [map_eq_zero_iff _ hφ]

Premises used: map_eq_zero_iff
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots ((φ : (a : R) → S) r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r))
      (map φ f).natDegree (map φ g).natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
      (map φ f).resultant (map φ g)
⊢ Ne (α := S) ((φ : (a : R) → S) f.leadingCoeff : S) (0 : S)

Tactic:
simpa [map_eq_zero_iff _ hφ]

Premises used: map_eq_zero_iff
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : R[X]) (r : R) (hf : q ≠ 0) (hg : g ≠ 0),
    (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
      r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
r : S
hf : f ≠ 0
hg : g ≠ 0
inr :
  ∀ (f' : R[X]) (hf' : map φ f' = f) (ef : f'.degree = f.degree),
    (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 ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)

Premises used: Polynomial.map_surjective, Polynomial.exists_degree_eq_of_mem_lifts
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : R[X]) (r : R) (hf : q ≠ 0) (hg : g ≠ 0),
    (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
      r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
r : S
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
inr :
  ∀ (g' : R[X]) (hg' : map φ g' = g) (eg : g'.degree = g.degree),
    (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 ⟨g', hg', eg⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g)

Premises used: Polynomial.map_surjective, Polynomial.exists_degree_eq_of_mem_lifts
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : R[X]) (r : R) (hf : q ≠ 0) (hg : g ≠ 0),
    (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
      r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
r : S
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
inr :
  ∀ (r : R),
    (f.scaleRoots ((φ : (a : R) → S) r)).resultant (g.scaleRoots ((φ : (a : R) → S) r)) f.natDegree g.natDegree =
      HPow.hPow (α := S) ((φ : (a : R) → S) r : S) (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 ⟨r, rfl⟩ := hφ r

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : R[X]) (r : R) (hf : q ≠ 0) (hg : g ≠ 0),
    (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
      r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
simp_rw : f.coeff f.natDegree = (φ : (a : R) → S) (f'.coeff f'.natDegree)
simp_rw₁ : f.coeff f'.natDegree = (φ : (a : R) → S) (f'.coeff f'.natDegree)
simp_rw₂ : (map φ f').coeff f'.natDegree = (φ : (a : R) → S) (f'.coeff f'.natDegree)
⊢ f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff

Tactic:
simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]

Premises used: Polynomial.coeff_map, Polynomial.coeff_natDegree, Polynomial.natDegree_eq_natDegree