awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ g'.natDegree ≠ 0

Tactic:
simpa [natDegree_eq_natDegree eg]

Premises used: 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
hgl : g.leadingCoeff = (φ : (a : S) → R) g'.leadingCoeff
neg :
  (φ : (a : S) → R) (g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * f'.resultant g') =
    HPow.hPow (α := R) ((φ : (a : S) → R) g'.leadingCoeff : R) (f'.natDegree * (g'.natDegree - 1)) *
      (map φ f').resultant (map φ g') f'.natDegree g'.natDegree
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

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

Premises used: Polynomial.integralNormalization_map, inferInstance, Polynomial.natDegree_eq_natDegree, Polynomial.resultant_map_map, Polynomial.map_scaleRoots
-- 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
⊢ (φ : (a : S) → R) (g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * f'.resultant g') =
    HPow.hPow (α := R) ((φ : (a : S) → R) g'.leadingCoeff : R) (f'.natDegree * (g'.natDegree - 1)) *
      (map φ f').resultant (map φ g') f'.natDegree g'.natDegree

Tactic:
simp [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 : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
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_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
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_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
⊢ g.leadingCoeff ^ f.natDegree ≠ 0

Tactic:
simp [hg0]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
neg :
  Eq.{u_1 + 1} (α := R)
    ((fun (x : R) ↦ g.leadingCoeff ^ f.natDegree * x)
      ((f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree))
    ((fun (x : R) ↦ g.leadingCoeff ^ f.natDegree * x)
      (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:
apply mul_right_injective₀ (a := g.leadingCoeff ^ f.natDegree) (by simp [hg0])

Premises used: mul_right_injective₀
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
⊢ (f.scaleRoots g.leadingCoeff).resultant (g.scaleRoots g.leadingCoeff) =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
have := resultant_scaleRoots f g g.leadingCoeff
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  (f.scaleRoots g.leadingCoeff).resultant (g.scaleRoots g.leadingCoeff) =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
rw [natDegree_scaleRoots, natDegree_scaleRoots,
    ← integralNormalization_mul_C_leadingCoeff, mul_comm, resultant_C_mul_right] at this

Premises used: Polynomial.natDegree_scaleRoots, mul_comm, Polynomial.integralNormalization_mul_C_leadingCoeff, 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 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ 1 ≤ g.natDegree

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
neg :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
neg₁ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
neg₂ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree + f.natDegree * (g.natDegree - 1)) * f.resultant g
neg₃ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1) + f.natDegree) * f.resultant g
neg₄ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1 + 1)) * f.resultant g
neg₅ neg₆ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)

Tactic:
rw [this, ← mul_assoc, ← pow_add, add_comm, ← Nat.mul_add_one, Nat.sub_add_cancel (by lia)]

Premises used: mul_assoc, pow_add, add_comm, Nat.sub_add_cancel, Nat.mul_add_one
-- 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]
g : R[X]
r : R
x : R[X]
h :
  Membership.mem (γ := Set R[X])
    ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
      {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    x
Splits :
  ∀ (s : R),
    resultant ((taylor r : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) s)) ((taylor r : (a : R[X]) → R[X]) g) =
      resultant ((C : (a : R) → R[X]) s) g
Splits₁ :
  ∀ (s : R),
    resultant ((taylor r : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])))
        ((taylor r : (a : R[X]) → R[X]) g) =
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])).resultant g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g

Tactic:
obtain (⟨s, rfl⟩ | ⟨s, rfl⟩) := h

Premises used: 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]
g : R[X]
r s : R
Splits : resultant ((C : (a : R) → R[X]) s) ((taylor r : (a : R[X]) → R[X]) g) = resultant ((C : (a : R) → R[X]) s) g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) s)) ((taylor r : (a : R[X]) → R[X]) g) =
    resultant ((C : (a : R) → R[X]) s) g

Tactic:
rw [taylor_C]

Premises used: Polynomial.taylor_C
-- 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]
g : R[X]
r s : R
⊢ resultant ((C : (a : R) → R[X]) s) ((taylor r : (a : R[X]) → R[X]) g) = resultant ((C : (a : R) → R[X]) s) 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]
g : R[X]
r s : R
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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]
g : R[X]
r s : R
inst_2 : Nontrivial R
Splits :
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r + s) : R[X])).resultant
      ((taylor r : (a : R[X]) → R[X]) g) =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])).resultant g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])))
      ((taylor r : (a : R[X]) → R[X]) g) =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])).resultant g

Tactic:
rw [map_add, taylor_X, taylor_C, add_assoc, ← map_add]

Premises used: add_assoc, map_add, Polynomial.taylor_X, Polynomial.taylor_C
-- 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]
g : R[X]
r s : R
inst_2 : Nontrivial R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r + s) : R[X])).resultant
      ((taylor r : (a : R[X]) → R[X]) g) =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])).resultant g

Tactic:
simp [-map_add, taylor_eval]

Premises used: Polynomial.taylor_eval, map_add
-- 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]
g : R[X]
r : R
⊢ resultant ((taylor r : (a : R[X]) → R[X]) 1) ((taylor r : (a : R[X]) → R[X]) g) = resultant 1 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]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
pos :
  ∀ (hx0 : x = 0),
    resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
neg :
  ∀ (hx0 : ¬x = 0),
    resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g

Tactic:
by_cases hx0 : x = 0
-- 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]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
hx0 : x = 0
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g

Tactic:
simp [hx0]
-- 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]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
hx0 : ¬x = 0
pos :
  ∀ (hy0 : y = 0),
    resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
neg :
  ∀ (hy0 : ¬y = 0),
    resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g

Tactic:
by_cases hy0 : y = 0
-- 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]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
hx0 : ¬x = 0
hy0 : y = 0
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g

Tactic:
simp [hy0]
-- 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]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ HMul.hMul (α := R) (leadingCoeff ((taylor r : (a : R[X]) → R[X]) x))
      (leadingCoeff ((taylor r : (a : R[X]) → R[X]) y)) ≠
    0

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]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
hx0 : ¬x = 0
hy0 : ¬y = 0
neg :
  HMul.hMul (α := R) (resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g))
      (resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g)) =
    (x * y).resultant g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g

Tactic:
rw [taylor_mul, natDegree_mul' (by simp [*]), resultant_mul_left _ _ _ _ le_rfl]

Premises used: Polynomial.taylor_mul, le_rfl, Polynomial.natDegree_mul', Polynomial.resultant_mul_left
-- 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]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ HMul.hMul (α := R) (resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g))
      (resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g)) =
    (x * y).resultant g

Tactic:
simp [natDegree_mul', hx0, hy0, resultant_mul_left, ← hx', ← hy']

Premises used: Polynomial.natDegree_mul', Polynomial.resultant_mul_left
-- 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
Splits :
  ∀ (x : R[X])
    (h :
      Membership.mem (γ := Set R[X])
        ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
        x),
    resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
Splits₁ : resultant ((taylor r : (a : R[X]) → R[X]) 1) ((taylor r : (a : R[X]) → R[X]) g) = resultant 1 g
Splits₂ :
  ∀ (x y : R[X])
    (hx :
      Membership.mem (γ := Submonoid R[X])
        (Submonoid.closure
          ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
            {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
        x)
    (hy :
      Membership.mem (γ := Submonoid R[X])
        (Submonoid.closure
          ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
            {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
        y)
    (hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g)
    (hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g),
    resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g) = f.resultant g

Tactic:
induction hf' using Submonoid.closure_induction with
    | mem x h =>
      obtain (⟨s, rfl⟩ | ⟨s, rfl⟩) := h
      · rw [taylor_C]; simp
      · nontriviality R
        rw [map_add, taylor_X, taylor_C, add_assoc, ← map_add]
        simp [-map_add, taylor_eval]
    | one => simp
    | mul x y hx hy hx' hy' =>
      by_cases hx0 : x = 0; · simp [hx0]
      by_cases hy0 : y = 0; · simp [hy0]
      rw [taylor_mul, natDegree_mul' (by simp [*]), resultant_mul_left _ _ _ _ le_rfl]
      simp [natDegree_mul', hx0, hy0, resultant_mul_left, ← hx', ← hy']

Premises used: Polynomial.taylor_eval, Polynomial.taylor_mul, le_rfl, add_assoc, Polynomial.natDegree_mul', map_add, Polynomial.resultant_mul_left, Polynomial.taylor_X, Polynomial.taylor_C, 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.Injective (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
IH :
  ∀ (g : S[X]) (r : S),
    resultant ((taylor r : (a : S[X]) → S[X]) (map φ f)) ((taylor r : (a : S[X]) → S[X]) g) = (map φ f).resultant g
g : R[X]
r : R
injective :
  Eq (α := S) ((φ : (a : R) → S) (resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g)) : S)
    ((φ : (a : R) → S) (f.resultant g) : S)
⊢ resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g) = f.resultant g

Tactic:
apply hφ