-- 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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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
surjective :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) f.natDegree =
    f.resultant g
surjective₁ :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) f.natDegree g.natDegree =
    f.resultant g
surjective₂ :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) (map φ f'))
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) (map φ f').natDegree g.natDegree =
    (map φ f').resultant g
surjective₃ :
  (map φ ((taylor r : (a : R[X]) → R[X]) f')).resultant
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) (map φ f').natDegree g.natDegree =
    (map φ f').resultant g
surjective₄ :
  (map φ ((taylor r : (a : R[X]) → R[X]) f')).resultant
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) (map φ g')) (map φ f').natDegree
      (map φ g').natDegree =
    (map φ f').resultant (map φ g')
surjective₅ :
  (map φ ((taylor r : (a : R[X]) → R[X]) f')).resultant (map φ ((taylor r : (a : R[X]) → R[X]) g')) (map φ f').natDegree
      (map φ g').natDegree =
    (map φ f').resultant (map φ g')
surjective₆ :
  (φ : (a : R) → S)
      (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') (map φ f').natDegree
        (map φ g').natDegree) =
    (map φ f').resultant (map φ g')
surjective₇ :
  Eq (α := S)
    ((φ : (a : R) → S)
        (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') (map φ f').natDegree
          (map φ g').natDegree) :
      S)
    ((φ : (a : R) → S) (f'.resultant g' (map φ f').natDegree (map φ g').natDegree) : S)
surjective₈ :
  Eq (α := S)
    ((φ : (a : R) → S)
        (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') f.natDegree
          (map φ g').natDegree) :
      S)
    ((φ : (a : R) → S) (f'.resultant g' f.natDegree (map φ g').natDegree) : S)
surjective₉ :
  Eq (α := S)
    ((φ : (a : R) → S)
        (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') f.natDegree g.natDegree) :
      S)
    ((φ : (a : R) → S) (f'.resultant g' f.natDegree g.natDegree) : S)
surjective₁₀ :
  Eq (α := S)
    ((φ : (a : R) → S)
        (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') f'.natDegree g.natDegree) :
      S)
    ((φ : (a : R) → S) (f'.resultant g' f'.natDegree g.natDegree) : S)
surjective₁₁ :
  Eq (α := S)
    ((φ : (a : R) → S)
        (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') f'.natDegree g'.natDegree) :
      S)
    ((φ : (a : R) → S) (f'.resultant g') : S)
surjective₁₂ :
  Eq (α := S)
    ((φ : (a : R) → S)
        (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') f'.natDegree g'.natDegree) :
      S)
    ((φ : (a : R) → S) (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g')) : S)
surjective₁₃ :
  Eq (α := S)
    ((φ : (a : R) → S)
        (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') f'.natDegree g'.natDegree) :
      S)
    ((φ : (a : R) → S)
        (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') f'.natDegree) :
      S)
surjective₁₄ surjective₁₅ :
  Eq (α := S)
    ((φ : (a : R) → S)
        (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') f'.natDegree g'.natDegree) :
      S)
    ((φ : (a : R) → S)
        (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') f'.natDegree g'.natDegree) :
      S)
⊢ resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) =
    f.resultant g

Tactic:
rw [natDegree_taylor, natDegree_taylor, ← hf', ← map_taylor, ← hg', ← map_taylor,
      resultant_map_map, resultant_map_map, hf', hg', ← natDegree_eq_natDegree ef,
      ← natDegree_eq_natDegree eg, ← IH f' g' r, natDegree_taylor, natDegree_taylor]

Premises used: Polynomial.map_taylor, Polynomial.natDegree_taylor, Polynomial.natDegree_eq_natDegree, Polynomial.resultant_map_map