F : Type u_1
K : Type u_3
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field E
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsSeparable F E
x : K
hs : Separable (minpoly F (↑(algebraMap K E) x))
⊢ Separable (minpoly F x)
F : Type u_1
K : Type u_3
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field E
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsSeparable F E
x : K
⊢ IsIntegral F x ∧ Separable (minpoly F x)
refine'
  (isSeparable_iff.1 h (algebraMap K E x)).imp isIntegral_tower_bot_of_isIntegral_field
    fun hs => _
case intro
F : Type u_1
K : Type u_3
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field E
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsSeparable F E
x : K
hs : Separable (minpoly F (↑(algebraMap K E) x))
q : F[X]
hq : minpoly F (↑(algebraMap K E) x) = minpoly F x * q
⊢ Separable (minpoly F x)
F : Type u_1
K : Type u_3
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field E
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsSeparable F E
x : K
hs : Separable (minpoly F (↑(algebraMap K E) x))
⊢ Separable (minpoly F x)
obtain ⟨q, hq⟩ :=
  minpoly.dvd F x
    ((aeval_algebraMap_eq_zero_iff _ _ _).mp (minpoly.aeval F ((algebraMap K E) x)))
case intro
F : Type u_1
K : Type u_3
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field E
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsSeparable F E
x : K
q : F[X]
hs : Separable (minpoly F x * q)
hq : minpoly F (↑(algebraMap K E) x) = minpoly F x * q
⊢ Separable (minpoly F x)
case intro
F : Type u_1
K : Type u_3
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field E
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsSeparable F E
x : K
hs : Separable (minpoly F (↑(algebraMap K E) x))
q : F[X]
hq : minpoly F (↑(algebraMap K E) x) = minpoly F x * q
⊢ Separable (minpoly F x)
rw [hq] at hs
no goals
case intro
F : Type u_1
K : Type u_3
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field E
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsSeparable F E
x : K
q : F[X]
hs : Separable (minpoly F x * q)
hq : minpoly F (↑(algebraMap K E) x) = minpoly F x * q
⊢ Separable (minpoly F x)
exact hs.of_mul_left