rw [← P.sUnion_eq] at hx
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ s
⊢ P.partOf x = ∅
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ ⋃₀ ↑P
⊢ P.partOf x = ∅