-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
refine_1 :
  (∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑∅ : Set K))) L)
refine_2 refine_2₁ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀
        (ih :
          (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
        (H : ∀ x ∈ insert a s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))),
        Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
refine_2₂ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀
        (ih :
          (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
        (H :
          (IsIntegral F a ∧ Splits (map (algebraMap F L) (minpoly F a))) ∧
            ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))),
        Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
refine_2₃ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀
        (ih :
          (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
        (H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) (H1 : IsIntegral F a)
        (H2 : Splits (map (algebraMap F L) (minpoly F a))),
        Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
refine_2₄ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀
        (ih :
          (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
        (H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) (H1 : IsIntegral F a)
        (H2 : Splits (map (algebraMap F L) (minpoly F a)))
        (f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L),
        Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
refine_2₅ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀
        (ih :
          (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
        (H1 : IsIntegral F a) (H2 : Splits (map (algebraMap F L) (minpoly F a)))
        (f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L) (H3 : ∀ x ∈ s, IsIntegral F x),
        (∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))) →
          Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
⊢ (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
have refine_2₆ : ∀ (a : K) (s : Finset K),
  a ∉ s →
    ∀
      (ih :
        (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
          Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
      (H1 : IsIntegral F a) (H2 : Splits (map (algebraMap F L) (minpoly F a)))
      (f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L) (H3 : ∀ x ∈ s, IsIntegral F x),
      (∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))) →
        Nonempty
          (AlgHom.{u_2, u_3, u_4} F
            (↥(Subalgebra.restrictScalars F (S := ↥(Algebra.adjoin F (↑s : Set K)))
                (↥(Algebra.adjoin F (↑s : Set K)))[a]))
            L)
Tactic: classical
    refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
    · rw [coe_empty, Algebra.adjoin_empty]
      exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
    rw [forall_mem_insert] at H
    rcases H with ⟨⟨H1, H2⟩, H3⟩
    obtain ⟨f⟩ := ih H3
    choose H3 _ using H3
    rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
    set Ks := Algebra.adjoin F (s : Set K)
    haveI : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
    letI := fieldOfFiniteDimensional F Ks
    letI := (f : Ks →+* L).toAlgebra
    have H5 : IsIntegral Ks a := H1.tower_top
    have H6 : ((minpoly Ks a).map (algebraMap Ks L)).Splits := by
      refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
      rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']
      exact minpoly.dvd_map_of_isScalarTower F Ks a
    obtain ⟨y, hy⟩ := H6.exists_eval_eq_zero (by simp [(minpoly.degree_pos H5).ne'])
    rw [eval_map] at hy
    exact ⟨Subalgebra.ofRestrictScalars F _ <| Algebra.adjoin.liftSingleton Ks a y hy⟩