simp only [not_mem_empty, iff_false]
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : ∀ a ∈ P, a = ⊥
⊢ x ∈ P ↔ x ∈ Partition.empty α
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
hsup : ∀ a ∈ P, a = ⊥
⊢ x ∉ P