have := Separable.map H (f := Ideal.Quotient.mk m)
case intro
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
m : Ideal S
hm : m.IsMaximal
⊢ p.Separable
case intro
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
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
⊢ p.Separable