awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff

Tactic:
have hfl : f.leadingCoeff = φ f'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
-- 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
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
simp_rw : g.coeff g.natDegree = (φ : (a : R) → S) (g'.coeff g'.natDegree)
simp_rw₁ : g.coeff g'.natDegree = (φ : (a : R) → S) (g'.coeff g'.natDegree)
simp_rw₂ : (map φ g').coeff g'.natDegree = (φ : (a : R) → S) (g'.coeff g'.natDegree)
⊢ g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff

Tactic:
simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]

Premises used: Polynomial.coeff_map, Polynomial.coeff_natDegree, Polynomial.natDegree_eq_natDegree
-- 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
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
⊢ g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff

Tactic:
have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
-- 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
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
⊢ Ne (α := S) ((φ : (a : R) → S) f'.leadingCoeff : S) (0 : S)

Tactic:
simpa [← hfl]
-- 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
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
⊢ Ne (α := S) ((φ : (a : R) → S) g'.leadingCoeff : S) (0 : S)

Tactic:
simpa [← hgl]
-- 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
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
⊢ f' ≠ 0

Tactic:
aesop
-- 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
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
⊢ g' ≠ 0

Tactic:
aesop
-- 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
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
inr :
  (φ : (a : R) → S) (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) (f'.natDegree * g'.natDegree) * f.resultant g f'.natDegree g'.natDegree
⊢ (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

Tactic:
rw [← hf', ← map_scaleRoots _ _ _ (by simpa [← hfl]), ← hg',
      ← map_scaleRoots _ _ _ (by simpa [← hgl]), hf', hg',
      ← natDegree_eq_natDegree ef, ← natDegree_eq_natDegree eg,
      resultant_map_map, IH f' g' r (by aesop) (by aesop)]

Premises used: Polynomial.natDegree_eq_natDegree, Polynomial.resultant_map_map, 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.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
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
inr :
  (φ : (a : R) → S) (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') =
    HMul.hMul (β := S) (HPow.hPow (α := S) ((φ : (a : R) → S) r : S) (f'.natDegree * g'.natDegree))
      ((φ : (a : R) → S) (f'.resultant g') : S)
⊢ (φ : (a : R) → S) (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) (f'.natDegree * g'.natDegree) * f.resultant g f'.natDegree g'.natDegree

Tactic:
rw [← hf', ← hg', resultant_map_map]

Premises used: Polynomial.resultant_map_map
-- 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
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
⊢ (φ : (a : R) → S) (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') =
    HMul.hMul (β := S) (HPow.hPow (α := S) ((φ : (a : R) → S) r : S) (f'.natDegree * g'.natDegree))
      ((φ : (a : R) → S) (f'.resultant g') : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
rw :
  (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
rw [natDegree_scaleRoots, natDegree_integralNormalization]

Premises used: Polynomial.natDegree_scaleRoots, Polynomial.natDegree_integralNormalization
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
inr :
  ∀
    (this :
      ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
    (hR : ¬IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
wlog :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
wlog hR : IsDomain R

Premises used: IsDomain
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
pos :
  ∀ (hf0 : f = 0),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
neg :
  ∀ (hf0 : ¬f = 0),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
by_cases hf0 : f = 0
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : f = 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
simp [hf0]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
pos :
  ∀ (hg0 : g = 0),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
neg :
  ∀ (hg0 : ¬g = 0),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
by_cases hg0 : g = 0
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : g = 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
simp [hg0]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type u_1 := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
x : R
⊢ (φ : (a : S) → R) (MvPolynomial.X x) = x

Tactic:
simp [φ, MvPolynomial.eval₂Hom]

Premises used: MvPolynomial.eval₂Hom
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type u_1 := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
⊢ Function.Surjective (α := S) (β := R) (⇑φ : (a : S) → R)

Tactic:
have hφ : Function.Surjective φ := fun x ↦ ⟨.X x, by simp [φ, MvPolynomial.eval₂Hom]⟩
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type u_1 := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective (α := S) (β := R) (⇑φ : (a : S) → R)
neg :
  ∀ (f' : S[X]) (hf' : map φ f' = f) (ef : f'.degree = f.degree),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * 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 : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type u_1 := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective (α := S) (β := R) (⇑φ : (a : S) → R)
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
neg :
  ∀ (g' : S[X]) (hg' : map φ g' = g) (eg : g'.degree = g.degree),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * 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 : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type u_1 := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective (α := S) (β := R) (⇑φ : (a : S) → R)
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
simp_rw : f.coeff f.natDegree = (φ : (a : S) → R) (f'.coeff f'.natDegree)
simp_rw₁ : f.coeff f'.natDegree = (φ : (a : S) → R) (f'.coeff f'.natDegree)
simp_rw₂ : (map φ f').coeff f'.natDegree = (φ : (a : S) → R) (f'.coeff f'.natDegree)
⊢ f.leadingCoeff = (φ : (a : S) → R) 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
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type u_1 := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective (α := S) (β := R) (⇑φ : (a : S) → R)
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
⊢ f.leadingCoeff = (φ : (a : S) → R) f'.leadingCoeff

Tactic:
have hfl : f.leadingCoeff = φ f'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type u_1 := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective (α := S) (β := R) (⇑φ : (a : S) → R)
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = (φ : (a : S) → R) f'.leadingCoeff
simp_rw : g.coeff g.natDegree = (φ : (a : S) → R) (g'.coeff g'.natDegree)
simp_rw₁ : g.coeff g'.natDegree = (φ : (a : S) → R) (g'.coeff g'.natDegree)
simp_rw₂ : (map φ g').coeff g'.natDegree = (φ : (a : S) → R) (g'.coeff g'.natDegree)
⊢ g.leadingCoeff = (φ : (a : S) → R) g'.leadingCoeff

Tactic:
simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]

Premises used: Polynomial.coeff_map, Polynomial.coeff_natDegree, Polynomial.natDegree_eq_natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type u_1 := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective (α := S) (β := R) (⇑φ : (a : S) → R)
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = (φ : (a : S) → R) f'.leadingCoeff
⊢ g.leadingCoeff = (φ : (a : S) → R) g'.leadingCoeff

Tactic:
have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type u_1 := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective (α := S) (β := R) (⇑φ : (a : S) → R)
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = (φ : (a : S) → R) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : S) → R) g'.leadingCoeff
⊢ Ne (α := R) ((φ : (a : S) → R) f'.leadingCoeff : R) (0 : R)

Tactic:
simpa [← hfl]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type u_1 := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective (α := S) (β := R) (⇑φ : (a : S) → R)
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = (φ : (a : S) → R) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : S) → R) g'.leadingCoeff
⊢ Ne (α := R) ((φ : (a : S) → R) g'.leadingCoeff : R) (0 : R)

Tactic:
simpa [← hgl]