simp only [partOf, eq_empty_iff_forall_not_mem, mem_sUnion, mem_setOf, not_exists, not_and,
  and_imp]
α : 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 = ∅
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ ⋃₀ ↑P
⊢ ∀ (x_1 : α), ∀ x_2 ∈ P, x ∈ x_2 → x_1 ∉ x_2