simp only [mem_neighborFinset, mem_range, Ne.def, exists_prop, and_iff_left_iff_imp]
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
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 →
    ∃ i,
      i < (minsert M h).t + 1 ∧
        ∃ j,
          j < (minsert M h).t + 1 ∧
            ¬i = j ∧
              (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
                v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)