apply (IsSeparable.separable R x).map.scaleRoots
case intro.intro.intro.intro.refine_1
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)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ P.Separable
case intro.intro.intro.intro.refine_1.hr
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)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ IsUnit (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)