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

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
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)

Tactic:
have hL := splits_of_splits_mul' _ ?_ (SplittingField.splits (p * minpoly F x))

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)
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)

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

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
this : FiniteDimensional F E
hx : IsIntegral F x
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)

Tactic:
let L := (p * minpoly F x).SplittingField

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
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)

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 ((↑j).comp (algebraMap F E)) (minpoly F x)).roots
⊢ a ∈ (↑j).range

Tactic:
rw [j.comp_algebraMap] at 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 (algebraMap F L) (minpoly F x)).roots
⊢ a ∈ (↑j).range

Proof state:
case inl
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
hFEp : IsSplittingField F E 0
⊢ Normal F E

Tactic:
have := hFEp.adjoin_rootSet

Result:
case inl
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
hFEp : IsSplittingField F E 0
this : Algebra.adjoin F (rootSet 0 E) = ⊤
⊢ Normal F E

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 L) p

Tactic:
exact hL.1

Result:
no goals

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 ∈ (↑j).range

Tactic:
change a ∈ j.range

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

Proof state:
case inl
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
hFEp : IsSplittingField F E 0
this : Algebra.adjoin F (rootSet 0 E) = ⊤
⊢ Normal F E

Tactic:
rw [rootSet_zero, Algebra.adjoin_empty] at this

Result:
case inl
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
hFEp : IsSplittingField F E 0
this : ⊥ = ⊤
⊢ Normal F E

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
⊢ a ∈ (↑j).range

Tactic:
letI : Algebra F⟮x⟯ L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toRingHom.toAlgebra

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 (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
⊢ a ∈ (↑j).range