case intro
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ (s : E), s ∈ S → IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : Lifts F E K
hx : ∀ (a : Lifts F E K), x ≤ a → a = x
⊢ Nonempty ({ x // x ∈ adjoin F S } →ₐ[F] K)
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ (s : E), s ∈ S → IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
⊢ Nonempty ({ x // x ∈ adjoin F S } →ₐ[F] K)
obtain ⟨x : Lifts F E K, hx⟩ := zorn_partialOrder Lifts.exists_upper_bound
case intro
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ (s : E), s ∈ S → IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : Lifts F E K
hx : ∀ (a : Lifts F E K), x ≤ a → a = x
s✝ : { x // x ∈ adjoin F S }
s : E
hs : s ∈ S
⊢ s ∈ ↑x.fst
case intro
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ (s : E), s ∈ S → IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : Lifts F E K
hx : ∀ (a : Lifts F E K), x ≤ a → a = x
⊢ Nonempty ({ x // x ∈ adjoin F S } →ₐ[F] K)
refine'
  ⟨{ toFun := (fun s => x.2 ⟨s, adjoin_le_iff.mpr (fun s hs => _) s.mem⟩)
     map_one' := x.2.map_one
     map_mul' := (fun s t => x.2.map_mul ⟨s, _⟩ ⟨t, _⟩)
     map_zero' := x.2.map_zero
     map_add' := (fun s t => x.2.map_add ⟨s, _⟩ ⟨t, _⟩)
     commutes' := x.2.commutes }⟩
case intro.intro.intro
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ (s : E), s ∈ S → IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : Lifts F E K
hx : ∀ (a : Lifts F E K), x ≤ a → a = x
s✝ : { x // x ∈ adjoin F S }
s : E
hs : s ∈ S
y : Lifts F E K
h1 : x ≤ y
h2 : s ∈ y.fst
⊢ s ∈ ↑x.fst
case intro
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ (s : E), s ∈ S → IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : Lifts F E K
hx : ∀ (a : Lifts F E K), x ≤ a → a = x
s✝ : { x // x ∈ adjoin F S }
s : E
hs : s ∈ S
⊢ s ∈ ↑x.fst
rcases x.exists_lift_of_splits (hK s hs).1 (hK s hs).2 with ⟨y, h1, h2⟩
no goals
case intro.intro.intro
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ (s : E), s ∈ S → IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : Lifts F E K
hx : ∀ (a : Lifts F E K), x ≤ a → a = x
s✝ : { x // x ∈ adjoin F S }
s : E
hs : s ∈ S
y : Lifts F E K
h1 : x ≤ y
h2 : s ∈ y.fst
⊢ s ∈ ↑x.fst
rwa [hx y h1] at h2