case intro
F : Type u_1
K : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
hx : IsIntegral F x
hhx : Splits (algebraMap F E) (minpoly F x)
⊢ IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)
F : Type u_1
K : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
⊢ IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)
cases' h.out x with hx hhx
case intro
F : Type u_1
K : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
hx : IsIntegral F x
hhx : Splits (RingHom.comp (algebraMap K E) (algebraMap F K)) (minpoly F x)
⊢ IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)
case intro
F : Type u_1
K : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
hx : IsIntegral F x
hhx : Splits (algebraMap F E) (minpoly F x)
⊢ IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)
rw [algebraMap_eq F K E] at hhx
no goals
case intro
F : Type u_1
K : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
hx : IsIntegral F x
hhx : Splits (RingHom.comp (algebraMap K E) (algebraMap F K)) (minpoly F x)
⊢ IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)
exact
  ⟨isIntegral_of_isScalarTower hx,
    Polynomial.splits_of_splits_of_dvd (algebraMap K E)
      (Polynomial.map_ne_zero (minpoly.ne_zero hx))
      ((Polynomial.splits_map_iff (algebraMap F K) (algebraMap K E)).mpr hhx)
      (minpoly.dvd_map_of_isScalarTower F K x)⟩