exact not_nbhr_same_part this vin win
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
win :
  ∃ i,
    i ∈ range ((minsert M h).t + 1) ∧
      ∃ j,
        j ∈ range ((minsert M h).t + 1) ∧
          i ≠ j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ w ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ w ∈ MultiPart.P (minsert M h) i)
⊢ ¬w ∈ MultiPart.P (minsert M h) (M.t + 1)
no goals