exact not_disjoint_iff.2 ⟨v, hv, lkc.1⟩ h
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : ¬k ≠ M.t + 1
h✝ : l ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ MultiPart.P M l
⊢ False
no goals