simp only [mem_setOf_eq, mem_singleton_iff]
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' ∈ {t | t ∈ P ∧ x ∈ t} ↔ t' ∈ {t}
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' ∈ P ∧ x ∈ t' ↔ t' = t