rw [← SetLike.mem_coe, empty_coe_eq]
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α
⊢ a ∉ Partition.empty α
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
a : α
⊢ a ∉ ∅