obtain ⟨x, hx⟩ := P.nonempty_of_mem h
case hP.refine_2
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a✝ b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
a : Set α
h : a ∈ P
⊢ ∃ x ∈ s, a = {y | P.Rel x y}
case hP.refine_2.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x✝ y z : α
s✝ t : Set α
a✝ b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
a : Set α
h : a ∈ P
x : α
hx : x ∈ a
⊢ ∃ x ∈ s, a = {y | P.Rel x y}