obtain ⟨S, hs1, hs2⟩ := h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
h : ∃ t_1, IsNClique (mp M) (t + 2) t_1
⊢ 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 : IsClique (mp M) ↑S
hs2 : card S = t + 2
⊢ False