-- Mathlib/FieldTheory/Normal/Basic.lean
theorem Normal.exists_isSplittingField [h : Normal F K] [FiniteDimensional F K] :
    ∃ p : F[X], IsSplittingField F K p

Proof state:
case refine_2
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
x : ↑(Basis.ofVectorSpaceIndex F K)
⊢ (map (algebraMap F K) (∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (s x))).IsRoot (s x)

Tactic:
rw [IsRoot.def, eval_map, ← aeval_def, map_prod]

Result:
case refine_2
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
x : ↑(Basis.ofVectorSpaceIndex F K)
⊢ ∏ x_1 : ↑(Basis.ofVectorSpaceIndex F K), (aeval (s x)) (minpoly F (s x_1)) = 0

Proof state:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
⊢ ∃ p, IsSplittingField F K p

Tactic:
refine
  ⟨∏ x, minpoly F (s x), splits_prod _ fun x _ => h.splits (s x),
    Subalgebra.toSubmodule.injective ?_⟩

Result:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
⊢ Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (s x)).rootSet K)) =
    Subalgebra.toSubmodule ⊤

Proof state:
case refine_2
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
x : ↑(Basis.ofVectorSpaceIndex F K)
⊢ ∏ x_1 : ↑(Basis.ofVectorSpaceIndex F K), (aeval (s x)) (minpoly F (s x_1)) = 0

Tactic:
exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)

Result:
no goals

Proof state:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
⊢ ∃ p, IsSplittingField F K p

Tactic:
let s := Basis.ofVectorSpace F K

Result:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
⊢ ∃ p, IsSplittingField F K p

Proof state:
case refine_1
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
x✝¹ x : ↑(Basis.ofVectorSpaceIndex F K)
x✝ : x ∈ Finset.univ
⊢ minpoly F (s x) ≠ 0

Tactic:
exact minpoly.ne_zero (h.isIntegral (s x))

Result:
no goals

Proof state:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
⊢ ∀ (y : ↑(Basis.ofVectorSpaceIndex F K)),
    s y ∈
      ↑(Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (s x)).rootSet K)))

Tactic:
refine fun x =>
  Algebra.subset_adjoin
    (Multiset.mem_toFinset.mpr <|
      (mem_roots <|
            mt (Polynomial.map_eq_zero <| algebraMap F K).1 <|
              Finset.prod_ne_zero_iff.2 fun x _ => ?_).2 ?_)

Result:
case refine_1
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
x✝¹ x : ↑(Basis.ofVectorSpaceIndex F K)
x✝ : x ∈ Finset.univ
⊢ minpoly F (s x) ≠ 0

case refine_2
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
x : ↑(Basis.ofVectorSpaceIndex F K)
⊢ (map (algebraMap F K) (∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (s x))).IsRoot (s x)

Proof state:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
⊢ Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (s x)).rootSet K)) =
    Subalgebra.toSubmodule ⊤

Tactic:
rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]

Result:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K
⊢ ∀ (y : ↑(Basis.ofVectorSpaceIndex F K)),
    s y ∈
      ↑(Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (s x)).rootSet K)))