ext x
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P : Partition ⊥
⊢ P = Partition.empty α
case hP
α : Type u_1
inst✝ : CompleteLattice α
s x✝ y z : α
P : Partition ⊥
x : α
⊢ x ∈ P ↔ x ∈ Partition.empty α