case intro
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
⊢ IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
⊢ IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)
cases' h.out (f.symm x) with hx hhx
case intro
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F (↑↑f (↑(AlgEquiv.symm f) x))
⊢ IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)
case intro
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
⊢ IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)
have H := map_isIntegral f.toAlgHom hx
case intro
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)
case intro
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F (↑↑f (↑(AlgEquiv.symm f) x))
⊢ IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)
simp [AlgEquiv.toAlgHom_eq_coe] at H
case intro
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ Splits (algebraMap F E') (minpoly F x)
case intro
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)
use H
case intro.hf
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ Splits (algebraMap F E') (minpoly F (↑(AlgEquiv.symm f) x))

case intro.hgf
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ minpoly F x ∣ minpoly F (↑(AlgEquiv.symm f) x)
case intro
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ Splits (algebraMap F E') (minpoly F x)
apply Polynomial.splits_of_splits_of_dvd (algebraMap F E') (minpoly.ne_zero hx)
case intro.hf
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ Splits (RingHom.comp (↑↑f) (algebraMap F E)) (minpoly F (↑(AlgEquiv.symm f) x))
case intro.hf
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ Splits (algebraMap F E') (minpoly F (↑(AlgEquiv.symm f) x))
rw [← AlgHom.comp_algebraMap f.toAlgHom]
no goals
case intro.hf
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ Splits (RingHom.comp (↑↑f) (algebraMap F E)) (minpoly F (↑(AlgEquiv.symm f) x))
exact Polynomial.splits_comp_of_splits (algebraMap F E) f.toAlgHom.toRingHom hhx
case intro.hgf
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ ↑(aeval x) (minpoly F (↑(AlgEquiv.symm f) x)) = 0
case intro.hgf
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ minpoly F x ∣ minpoly F (↑(AlgEquiv.symm f) x)
apply minpoly.dvd _ _
case intro.hgf
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ ↑(AlgEquiv.toAddEquiv (AlgEquiv.symm f)) (↑(aeval x) (minpoly F (↑(AlgEquiv.symm f) x))) = 0
case intro.hgf
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ ↑(aeval x) (minpoly F (↑(AlgEquiv.symm f) x)) = 0
rw [← AddEquiv.map_eq_zero_iff f.symm.toAddEquiv]
no goals
case intro.hgf
F : Type u_1
K : Type ?u.73378
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
E' : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
x : E'
hx : IsIntegral F (↑(AlgEquiv.symm f) x)
hhx : Splits (algebraMap F E) (minpoly F (↑(AlgEquiv.symm f) x))
H : IsIntegral F x
⊢ ↑(AlgEquiv.toAddEquiv (AlgEquiv.symm f)) (↑(aeval x) (minpoly F (↑(AlgEquiv.symm f) x))) = 0
exact
  Eq.trans (Polynomial.aeval_algHom_apply f.symm.toAlgHom x (minpoly F (f.symm x))).symm
    (minpoly.aeval _ _)