-- Mathlib/FieldTheory/Normal/Basic.lean
theorem Normal.of_isSplittingField (p : F[X]) [hFEp : IsSplittingField F E p] : Normal F E

Proof state:
case inr.refine_2.refine_2
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (algebraMap F (p * minpoly F x).SplittingField) p ∧
    Splits (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)
j : E →ₐ[F] L := IsSplittingField.lift E p ⋯
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
j' : E →ₐ[↥F⟮x⟯] L := IsSplittingField.lift E (Polynomial.map (algebraMap F ↥F⟮x⟯) p) ?inr.refine_2.refine_1
⊢ a ∈ (AlgHom.restrictScalars F j').range

Tactic:
exact ⟨x, (j'.commutes _).trans (algHomAdjoinIntegralEquiv_symm_apply_gen F hx _)⟩

Result:
no goals

Proof state:
case inr.refine_2
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (algebraMap F (p * minpoly F x).SplittingField) p ∧
    Splits (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)
j : E →ₐ[F] L := IsSplittingField.lift E p ⋯
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)

Tactic:
refine ⟨hx, splits_of_comp _ (j : E →+* L) (j.comp_algebraMap ▸ hL.2) fun a ha ↦ ?_⟩

Result:
case inr.refine_2
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (algebraMap F (p * minpoly F x).SplittingField) p ∧
    Splits (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)
j : E →ₐ[F] L := IsSplittingField.lift E p ⋯
a : L
ha : a ∈ (Polynomial.map ((↑j).comp (algebraMap F E)) (minpoly F x)).roots
⊢ a ∈ (↑j).range

Proof state:
case inr.refine_2
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (algebraMap F (p * minpoly F x).SplittingField) p ∧
    Splits (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)
j : E →ₐ[F] L := IsSplittingField.lift E p ⋯
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
⊢ a ∈ (↑j).range

Tactic:
let j' : E →ₐ[F⟮x⟯] L := IsSplittingField.lift E (p.map (algebraMap F F⟮x⟯)) ?_

Result:
case inr.refine_2.refine_2
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (algebraMap F (p * minpoly F x).SplittingField) p ∧
    Splits (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)
j : E →ₐ[F] L := IsSplittingField.lift E p ⋯
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
j' : E →ₐ[↥F⟮x⟯] L := IsSplittingField.lift E (Polynomial.map (algebraMap F ↥F⟮x⟯) p) ?inr.refine_2.refine_1
⊢ a ∈ (↑j).range

case inr.refine_2.refine_1
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (algebraMap F (p * minpoly F x).SplittingField) p ∧
    Splits (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)
j : E →ₐ[F] L := IsSplittingField.lift E p ⋯
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
⊢ Splits (algebraMap (↥F⟮x⟯) L) (Polynomial.map (algebraMap F ↥F⟮x⟯) p)

Proof state:
case inr.refine_2.refine_1
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (algebraMap F (p * minpoly F x).SplittingField) p ∧
    Splits (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)
j : E →ₐ[F] L := IsSplittingField.lift E p ⋯
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
⊢ Splits (algebraMap (↥F⟮x⟯) L) (Polynomial.map (algebraMap F ↥F⟮x⟯) p)

Tactic:
rw [splits_map_iff, ← IsScalarTower.algebraMap_eq]

Result:
case inr.refine_2.refine_1
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (algebraMap F (p * minpoly F x).SplittingField) p ∧
    Splits (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)
j : E →ₐ[F] L := IsSplittingField.lift E p ⋯
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
⊢ Splits (algebraMap F L) p

Proof state:
case inr.refine_1
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
⊢ Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (p * minpoly F x) ≠ 0

Tactic:
rw [Polynomial.map_ne_zero_iff (algebraMap F L).injective, mul_ne_zero_iff]

Result:
case inr.refine_1
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
⊢ p ≠ 0 ∧ minpoly F x ≠ 0

Proof state:
case inr.refine_2
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (algebraMap F (p * minpoly F x).SplittingField) p ∧
    Splits (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)

Tactic:
let j : E →ₐ[F] L := IsSplittingField.lift E p hL.1

Result:
case inr.refine_2
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (algebraMap F (p * minpoly F x).SplittingField) p ∧
    Splits (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)
j : E →ₐ[F] L := IsSplittingField.lift E p ⋯
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)

Proof state:
case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)

Tactic:
haveI : FiniteDimensional F E := IsSplittingField.finiteDimensional E p

Result:
case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)