-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
Splits :
  ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hf' : f.Splits) (g : R[X]) (r : R),
    resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g) = f.resultant g
injective :
  ∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : 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), resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g) = f.resultant g
surjective :
  ∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : 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]) (r : S), resultant ((taylor r : (a : S[X]) → S[X]) f) ((taylor r : (a : S[X]) → S[X]) g) = f.resultant g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g) = f.resultant g

Tactic:
induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf' =>
    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']
  | injective R S φ hφ f IH =>
    apply hφ
    have := IH (g.map φ) (φ r)
    rw [← map_taylor, ← map_taylor] at this
    simpa [natDegree_map_eq_of_injective hφ] using this
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g', hg', eg⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g)
    obtain ⟨r, rfl⟩ := hφ r
    have hfl : f.leadingCoeff = φ f'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
    have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
    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.taylor_eval, Polynomial.taylor_mul, le_rfl, add_assoc, Polynomial.map_taylor, Polynomial.natDegree_mul', map_add, Polynomial.natDegree_taylor, Polynomial.resultant_mul_left, Polynomial.resultant_map_map, Polynomial.induction_of_Splits_of_injective_of_surjective, Polynomial.Splits, Polynomial.taylor_X, Polynomial.taylor_C, rfl