suffices ∃ i ∈ range (M.t + 1), 1 < (S ∩ M.P i).card
by
  obtain ⟨i, hi, hc⟩ := this; rw [one_lt_card_iff] at hc 
  obtain ⟨a, b, ha, hb, ne⟩ := hc; rw [mem_inter] at *
  have nadj := not_nbhr_same_part' hi ha.2 hb.2
  exact nadj (hs1 ha.1 hb.1 ne)
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
⊢ False
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
⊢ ∃ i, i ∈ range (M.t + 1) ∧ 1 < card (S ∩ MultiPart.P M i)