case intro.intro.intro
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 z : Lifts F E K
hc : IsChain (fun x x_1 => x ≤ x_1) c
hx : x ∈ insert ⊥ c
hy : y ∈ insert ⊥ c
hz : z ∈ insert ⊥ c
v : Lifts F E K
hv : v ∈ insert ⊥ c
hxv : x ≤ v
hyv : y ≤ v
⊢ ∃ w, w ∈ insert ⊥ c ∧ x ≤ w ∧ y ≤ w ∧ z ≤ w
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 z : Lifts F E K
hc : IsChain (fun x x_1 => x ≤ x_1) c
hx : x ∈ insert ⊥ c
hy : y ∈ insert ⊥ c
hz : z ∈ insert ⊥ c
⊢ ∃ w, w ∈ insert ⊥ c ∧ x ≤ w ∧ y ≤ w ∧ z ≤ w
obtain ⟨v, hv, hxv, hyv⟩ := Lifts.exists_max_two hc hx hy
case intro.intro.intro.intro.intro.intro
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 z : Lifts F E K
hc : IsChain (fun x x_1 => x ≤ x_1) c
hx : x ∈ insert ⊥ c
hy : y ∈ insert ⊥ c
hz : z ∈ insert ⊥ c
v : Lifts F E K
hv : v ∈ insert ⊥ c
hxv : x ≤ v
hyv : y ≤ v
w : Lifts F E K
hw : w ∈ insert ⊥ c
hzw : z ≤ w
hvw : v ≤ w
⊢ ∃ w, w ∈ insert ⊥ c ∧ x ≤ w ∧ y ≤ w ∧ z ≤ w
case intro.intro.intro
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 z : Lifts F E K
hc : IsChain (fun x x_1 => x ≤ x_1) c
hx : x ∈ insert ⊥ c
hy : y ∈ insert ⊥ c
hz : z ∈ insert ⊥ c
v : Lifts F E K
hv : v ∈ insert ⊥ c
hxv : x ≤ v
hyv : y ≤ v
⊢ ∃ w, w ∈ insert ⊥ c ∧ x ≤ w ∧ y ≤ w ∧ z ≤ w
obtain ⟨w, hw, hzw, hvw⟩ := Lifts.exists_max_two hc hz hv
no goals
case intro.intro.intro.intro.intro.intro
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 z : Lifts F E K
hc : IsChain (fun x x_1 => x ≤ x_1) c
hx : x ∈ insert ⊥ c
hy : y ∈ insert ⊥ c
hz : z ∈ insert ⊥ c
v : Lifts F E K
hv : v ∈ insert ⊥ c
hxv : x ≤ v
hyv : y ≤ v
w : Lifts F E K
hw : w ∈ insert ⊥ c
hzw : z ≤ w
hvw : v ≤ w
⊢ ∃ w, w ∈ insert ⊥ c ∧ x ≤ w ∧ y ≤ w ∧ z ≤ w
exact ⟨w, hw, le_trans hxv hvw, le_trans hyv hvw, hzw⟩