rw [mem_neighborFinset] at ha
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp M) v
⊢ Adj (mp (minsert M h)) v a✝
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ Adj (mp M) v a✝
⊢ Adj (mp (minsert M h)) v a✝