refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
⊢ (map f p).Separable ↔ p.Separable
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
⊢ p.Separable