rintro hab rfl
case refine'_1
α : 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
⊢ P.multipartiteGraph.Adj a b → s ≠ t
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s : Finset α
a b : α
hs : s ∈ P.parts
ha : a ∈ s
hab : P.multipartiteGraph.Adj a b
ht : s ∈ P.parts
hb : b ∈ s
⊢ False