feat: Add Polynomial.separable_map'. (#8680)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

Mathlib/FieldTheory/Separable.lean

@@ -283,9 +283,13 @@ theorem separable_iff_derivative_ne_zero {f : F[X]} (hf : Irreducible f) :
         natDegree_derivative_lt <| mt derivative_of_natDegree_zero h⟩
 #align polynomial.separable_iff_derivative_ne_zero Polynomial.separable_iff_derivative_ne_zero
 
-theorem separable_map (f : F →+* K) {p : F[X]} :
+attribute [local instance] Ideal.Quotient.field in
+theorem separable_map {S} [CommRing S] [Nontrivial S] (f : F →+* S) {p : F[X]} :
     (p.map f).Separable ↔ p.Separable := by
-  simp_rw [separable_def, derivative_map, isCoprime_map]
+  refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩
+  obtain ⟨m, hm⟩ := Ideal.exists_maximal S
+  have := Separable.map H (f := Ideal.Quotient.mk m)
+  rwa [map_map, separable_def, derivative_map, isCoprime_map] at this
 #align polynomial.separable_map Polynomial.separable_map
 
 theorem separable_prod_X_sub_C_iff' {ι : Sort _} {f : ι → F} {s : Finset ι} :