-- 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
⊢ Normal F E

Tactic:
refine normal_iff.mpr fun x ↦ ?_

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

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 : ⊥ = ⊤
⊢ Normal F E

Tactic:
exact Normal.of_algEquiv
  (AlgEquiv.ofBijective (Algebra.ofId F E) (Algebra.bijective_algebraMap_iff.2 this.symm))

Result:
no goals

Proof state:
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
⊢ Normal F E

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

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
⊢ Normal F E

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

Tactic:
have hx := IsIntegral.of_finite F x

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

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:
rw [← IsSplittingField.adjoin_rootSet_eq_range E p j,
      IsSplittingField.adjoin_rootSet_eq_range E p (j'.restrictScalars F)]

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 ∈ (AlgHom.restrictScalars F j').range

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
⊢ p ≠ 0 ∧ minpoly F x ≠ 0

Tactic:
exact ⟨hp, minpoly.ne_zero hx⟩

Result:
no goals