exact ⟨t, hxt, fun u ⟨huP, hxu⟩ ↦ eq_of_mem_inter huP hxt.1 ⟨hxu, hxt.2⟩⟩
case intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
t : Set α
hxt : t ∈ ↑P ∧ x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t
no goals