rw [isClique_iff] at hs1
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
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