obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid S M) x
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : Sₚ
⊢ (minpoly Rₚ x).Separable
case intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
⊢ (minpoly Rₚ (IsLocalization.mk' Sₚ x s)).Separable