rcases hx with ⟨s, hs, hx⟩
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ upperBounds S
x : Y
hx : x ∈ ⋃₀ S
⊢ x ∈ t
case mp.intro.intro
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ upperBounds S
x : Y
s : Set Y
hs : s ∈ S
hx : x ∈ s
⊢ x ∈ t