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
ϕ : E →ₐ[F] K
x : K
this : Algebra E K := RingHom.toAlgebra ↑ϕ
⊢ ∃ a, ↑ϕ a = 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
ϕ : E →ₐ[F] K
x : K
⊢ ∃ a, ↑ϕ a = x
letI : Algebra E K := ϕ.toRingHom.toAlgebra
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
ϕ : E →ₐ[F] K
x : K
this : Algebra E K := RingHom.toAlgebra ↑ϕ
h1 : IsIntegral F (↑(algebraMap K E) x)
h2 : Splits (algebraMap F E) (minpoly F (↑(algebraMap K E) x))
⊢ ∃ a, ↑ϕ a = 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
ϕ : E →ₐ[F] K
x : K
this : Algebra E K := RingHom.toAlgebra ↑ϕ
⊢ ∃ a, ↑ϕ a = x
obtain ⟨h1, h2⟩ := h.out (algebraMap K E x)
case intro.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
ϕ : E →ₐ[F] K
x : K
this : Algebra E K := RingHom.toAlgebra ↑ϕ
h1 : IsIntegral F (↑(algebraMap K E) x)
h2 : Splits (algebraMap F E) (minpoly F (↑(algebraMap K E) x))
y : E
hy : ↑(algebraMap E K) y = x
⊢ ∃ a, ↑ϕ a = 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
ϕ : E →ₐ[F] K
x : K
this : Algebra E K := RingHom.toAlgebra ↑ϕ
h1 : IsIntegral F (↑(algebraMap K E) x)
h2 : Splits (algebraMap F E) (minpoly F (↑(algebraMap K E) x))
⊢ ∃ a, ↑ϕ a = x
cases'
  minpoly.mem_range_of_degree_eq_one E x
    (h2.def.resolve_left (minpoly.ne_zero h1)
      (minpoly.irreducible
        (isIntegral_of_isScalarTower
          ((isIntegral_algebraMap_iff (algebraMap K E).injective).mp h1)))
      (minpoly.dvd E x
        ((algebraMap K E).injective
          (by
            rw [RingHom.map_zero, aeval_map_algebraMap, ← aeval_algebraMap_apply]
            exact minpoly.aeval F (algebraMap K E x))))) with
  y hy
no goals
case intro.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
ϕ : E →ₐ[F] K
x : K
this : Algebra E K := RingHom.toAlgebra ↑ϕ
h1 : IsIntegral F (↑(algebraMap K E) x)
h2 : Splits (algebraMap F E) (minpoly F (↑(algebraMap K E) x))
y : E
hy : ↑(algebraMap E K) y = x
⊢ ∃ a, ↑ϕ a = x
exact ⟨y, hy⟩
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
ϕ : E →ₐ[F] K
x : K
this : Algebra E K := RingHom.toAlgebra ↑ϕ
h1 : IsIntegral F (↑(algebraMap K E) x)
h2 : Splits (algebraMap F E) (minpoly F (↑(algebraMap K E) x))
⊢ ↑(aeval (↑(algebraMap K E) x)) (minpoly F (↑(algebraMap K E) x)) = 0
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
ϕ : E →ₐ[F] K
x : K
this : Algebra E K := RingHom.toAlgebra ↑ϕ
h1 : IsIntegral F (↑(algebraMap K E) x)
h2 : Splits (algebraMap F E) (minpoly F (↑(algebraMap K E) x))
⊢ ↑(algebraMap K E) (↑(aeval x) (map (algebraMap F E) (minpoly F (↑(algebraMap K E) x)))) = ↑(algebraMap K E) 0
rw [RingHom.map_zero, aeval_map_algebraMap, ← aeval_algebraMap_apply]
no goals
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
ϕ : E →ₐ[F] K
x : K
this : Algebra E K := RingHom.toAlgebra ↑ϕ
h1 : IsIntegral F (↑(algebraMap K E) x)
h2 : Splits (algebraMap F E) (minpoly F (↑(algebraMap K E) x))
⊢ ↑(aeval (↑(algebraMap K E) x)) (minpoly F (↑(algebraMap K E) x)) = 0
exact minpoly.aeval F (algebraMap K E x)