rw [mem_res_nbhd_iff]
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
⊢ a ∈ nbhdRes (mp (minsert M h)) v M.A ↔ a ∈ M.A
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
⊢ a ∈ M.A ∧ a ∈ neighborFinset (mp (minsert M h)) v ↔ a ∈ M.A