-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
inst_3 : FiniteDimensional F K
let let₁ let₂ : ∃ (p : F[X]), IsSplittingField F K p
let₃ :
  let s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K;
  Eq (α := Submodule F K)
    ((Subalgebra.toSubmodule : (a : Subalgebra F K) → Submodule F K)
        (Algebra.adjoin F
          (rootSet.{u_1, u_2} (T := F)
            (∏ x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
              minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K))
            K)) :
      Submodule F K)
    ((Subalgebra.toSubmodule : (a : Subalgebra F K) → Submodule F K) ⊤ : Submodule F K)
let₄ :
  let s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K;
  ∀ (y : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)),
    Membership.mem (α := K)
      (↑((Subalgebra.toSubmodule : (a : Subalgebra F K) → Submodule F K)
              (Algebra.adjoin F
                (rootSet.{u_1, u_2} (T := F)
                  (∏ x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
                    minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K))
                  K)) :
            Submodule F K) :
        Set K)
      ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) y : K)
refine_1 :
  let s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K;
  ∀ (x x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)),
    Membership.mem (γ := Finset (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) Finset.univ x →
      Ne (α := F[X]) (minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K)) 0
refine_2 refine_2₁ :
  let s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K;
  ∀ (x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)),
    IsRoot
      (map (algebraMap F K : F →+* K)
        (∏ x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
          minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K)))
      ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x)
refine_2₂ :
  let s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K;
  ∀ (x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)),
    Eq.{u_2 + 1} (α := K)
      (∏ x_1 : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
        ((aeval ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x) : F[X] →ₐ[F] K) :
            (a : F[X]) → K)
          (minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x_1 : K)))
      0
⊢ ∃ (p : F[X]), IsSplittingField F K p

Tactic:
classical
  let s := Module.Basis.ofVectorSpace F K
  refine
    ⟨∏ x, minpoly F (s x), Polynomial.map_prod (algebraMap F K) _ _ ▸
      Splits.prod fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩
  rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
  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 ?_)
  · exact minpoly.ne_zero (h.isIntegral (s x))
  rw [IsRoot.def, eval_map_algebraMap, map_prod]
  exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)

Premises used: Iff.mpr, Finset.mem_univ, eq_top_iff, Algebra.algebraMap, Algebra.subset_adjoin, Algebra.top_toSubmodule, Polynomial.IsRoot.def, mt, Finset.prod_ne_zero_iff, map_prod, Polynomial.mem_roots, Finset.prod_eq_zero, Iff.mp, Polynomial.eval_map_algebraMap, Polynomial.map_eq_zero, Set.range_subset_iff, Multiset.mem_toFinset, Submodule.span_le