obtain (hb | hb) := em (b ∈ s)
case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
⊢ P.Rel a b
case inr.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∈ s
⊢ P.Rel a b

case inr.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b