-- Mathlib/FieldTheory/Extension.lean
theorem exists_algHom_adjoin_of_splits'' {L : IntermediateField F E}
    (f : L →ₐ[F] K) (hK : ∀ s ∈ S, IsIntegral L s ∧ (minpoly L s).Splits f.toRingHom) :
    ∃ φ : adjoin L S →ₐ[F] K, φ.restrictDomain L = f

Proof state:
case intro.intro.refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝² : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝¹ : SMul ↥L ↥φ.carrier := Algebra.toSMul
this✝ : IsScalarTower (↥L) (↥φ.carrier) E
this : ∃ y, φ ≤ y ∧ s ∈ y.carrier
⊢ s ∈ ↑(extendScalars ⋯)

Tactic:
obtain ⟨y, h1, h2⟩ := this

Result:
case intro.intro.refine_2.intro.intro
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝¹ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝ : SMul ↥L ↥φ.carrier := Algebra.toSMul
this : IsScalarTower (↥L) (↥φ.carrier) E
y : Lifts F E K
h1 : φ ≤ y
h2 : s ∈ y.carrier
⊢ s ∈ ↑(extendScalars ⋯)

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)
⊢ ∃ φ, AlgHom.restrictDomain (↥L) φ = f

Tactic:
obtain ⟨φ, hfφ, hφ⟩ := zorn_le_nonempty_Ici₀ _
  (fun c _ hc _ _ ↦ Lifts.exists_upper_bound c hc) ⟨L, f⟩ le_rfl

Result:
case intro.intro
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
⊢ ∃ φ, AlgHom.restrictDomain (↥L) φ = f

Proof state:
case intro.intro
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
⊢ s ∈ ↑(extendScalars ⋯)

Tactic:
letI := (inclusion hfφ.1).toAlgebra

Result:
case intro.intro
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
⊢ s ∈ ↑(extendScalars ⋯)

Proof state:
case intro.intro.refine_2.intro.intro
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝¹ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝ : SMul ↥L ↥φ.carrier := Algebra.toSMul
this : IsScalarTower (↥L) (↥φ.carrier) E
y : Lifts F E K
h1 : φ ≤ y
h2 : s ∈ y.carrier
⊢ s ∈ ↑(extendScalars ⋯)

Tactic:
exact (hφ h1).1 h2

Result:
no goals