rw [f.apply_of_not_mem ha, f.apply_of_not_mem hb] at hab
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
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 : a = b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b