refine' ⟨_, fun hst u hu hau hbu => hst _⟩
α : 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 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'_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