rw [P.eq_of_mem_parts hs hu ha hau, P.eq_of_mem_parts ht hu hb hbu]
case refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s t : Finset α
a b : α
hs : s ∈ P.parts
ht : t ∈ P.parts
ha : a ∈ s
hb : b ∈ t
hst : s ≠ t
u : Finset α
hu : u ∈ P.parts
hau : a ∈ u
hbu : b ∈ u
⊢ s = t
no goals