-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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)
⊢ ∃ (p : F[X]), IsSplittingField F K p
have 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
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 _ _)