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
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
let s := Basis.ofVectorSpace F K
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
        ↑(Multiset.toFinset (roots (map (algebraMap F K) (∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (↑s x)))))) =
    ↑Subalgebra.toSubmodule ⊤
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
refine'
  ⟨∏ x, minpoly F (s x), splits_prod _ fun x _ => h.splits (s x),
    Subalgebra.toSubmodule.injective _⟩
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
            ↑(Multiset.toFinset
                (roots (map (algebraMap F K) (∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (↑s x)))))))
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
        ↑(Multiset.toFinset (roots (map (algebraMap F K) (∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (↑s x)))))) =
    ↑Subalgebra.toSubmodule ⊤
rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
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)
⊢ IsRoot (map (algebraMap F K) (∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (↑s x))) (↑s x)
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
            ↑(Multiset.toFinset
                (roots (map (algebraMap F K) (∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (↑s x)))))))
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
        _)
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
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)
⊢ IsRoot (map (algebraMap F K) (∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (↑s x))) (↑s x)
rw [IsRoot.def, eval_map, ← aeval_def, AlgHom.map_prod]
no goals
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
exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)
no goals
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
exact minpoly.ne_zero (h.isIntegral (s x))