case inl
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
x y : Lifts F E K
hc : IsChain (fun x x_1 => x ≤ x_1) c
hx : x ∈ insert ⊥ c
hy : y ∈ insert ⊥ c
hxy : x ≤ y
⊢ ∃ z, z ∈ insert ⊥ c ∧ x ≤ z ∧ y ≤ z

case inr
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
x y : Lifts F E K
hc : IsChain (fun x x_1 => x ≤ x_1) c
hx : x ∈ insert ⊥ c
hy : y ∈ insert ⊥ c
hyx : y ≤ x
⊢ ∃ z, z ∈ insert ⊥ c ∧ x ≤ z ∧ y ≤ z
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
x y : Lifts F E K
hc : IsChain (fun x x_1 => x ≤ x_1) c
hx : x ∈ insert ⊥ c
hy : y ∈ insert ⊥ c
⊢ ∃ z, z ∈ insert ⊥ c ∧ x ≤ z ∧ y ≤ z
cases' (hc.insert fun _ _ _ => Or.inl bot_le).total hx hy with hxy hyx
no goals
case inl
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
x y : Lifts F E K
hc : IsChain (fun x x_1 => x ≤ x_1) c
hx : x ∈ insert ⊥ c
hy : y ∈ insert ⊥ c
hxy : x ≤ y
⊢ ∃ z, z ∈ insert ⊥ c ∧ x ≤ z ∧ y ≤ z
exact ⟨y, hy, hxy, le_refl y⟩
no goals
case inr
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
x y : Lifts F E K
hc : IsChain (fun x x_1 => x ≤ x_1) c
hx : x ∈ insert ⊥ c
hy : y ∈ insert ⊥ c
hyx : y ≤ x
⊢ ∃ z, z ∈ insert ⊥ c ∧ x ≤ z ∧ y ≤ z
exact ⟨x, hx, le_refl x, hyx⟩