rw [← P.sUnion_eq]
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ s
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ ⋃₀ ↑P