-- Module: Mathlib.RingTheory.Adjoin.Field
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)
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)
refine_2₇ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀ (H1 : IsIntegral F a) (H2 : Splits (map (algebraMap F L) (minpoly F a))) (H3 : ∀ x ∈ s, IsIntegral F x),
        (∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))) →
          let Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K);
          ∀
            (ih :
              (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
                Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L))
            (f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L),
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
refine_2₈ refine_2₉ refine_2₁₀ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀ (H1 : IsIntegral F a) (H2 : Splits (map (algebraMap F L) (minpoly F a))) (H3 : ∀ x ∈ s, IsIntegral F x),
        (∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))) →
          let Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K);
          ∀
            (ih :
              (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
                Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L))
            (f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L) (this : FiniteDimensional.{u_2, u_3} F ↥Ks),
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
refine_2₁₁ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀ (H1 : IsIntegral F a) (H2 : Splits (map (algebraMap F L) (minpoly F a))) (H3 : ∀ x ∈ s, IsIntegral F x),
        (∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))) →
          let Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K);
          ∀
            (ih :
              (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
                Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L))
            (f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L) (this : FiniteDimensional.{u_2, u_3} F ↥Ks)
            (H5 : IsIntegral (↥Ks) a),
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
refine_2₁₂ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀ (H1 : IsIntegral F a) (H2 : Splits (map (algebraMap F L) (minpoly F a))) (H3 : ∀ x ∈ s, IsIntegral F x),
        (∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))) →
          let Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K);
          ∀
            (ih :
              (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
                Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L))
            (f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L) (this : FiniteDimensional.{u_2, u_3} F ↥Ks),
            let this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L);
            ∀ (H5 : IsIntegral (↥Ks) a) (H6 : Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))),
              Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
refine_2₁₃ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀ (H1 : IsIntegral F a) (H2 : Splits (map (algebraMap F L) (minpoly F a))) (H3 : ∀ x ∈ s, IsIntegral F x),
        (∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))) →
          let Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K);
          ∀
            (ih :
              (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
                Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L))
            (f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L) (this : FiniteDimensional.{u_2, u_3} F ↥Ks),
            let this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L);
            ∀ (H5 : IsIntegral (↥Ks) a) (H6 : Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))) (y : L)
              (hy : eval y (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a)) = 0),
              Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
refine_2₁₄ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀ (H1 : IsIntegral F a) (H2 : Splits (map (algebraMap F L) (minpoly F a))) (H3 : ∀ x ∈ s, IsIntegral F x),
        (∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))) →
          let Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K);
          ∀
            (ih :
              (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
                Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L))
            (f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L) (this : FiniteDimensional.{u_2, u_3} F ↥Ks),
            let this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L);
            ∀ (H5 : IsIntegral (↥Ks) a) (H6 : Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))) (y : L)
              (hy : eval₂ (R := ↥Ks) (algebraMap (↥Ks) L) y (minpoly (↥Ks) a) = 0),
              Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) 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)

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⟩

Premises used: Finset.coe_empty, Polynomial.eval_map, Set.insert_eq, Algebra.adjoin, Finset.forall_mem_insert, Set.union_comm, SetLike.coe, Algebra.adjoin_union_eq_adjoin_adjoin, Finset.coe_insert, Algebra.adjoin_empty