α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
⊢ IsNClique G 3 {a, b, c} ↔ Adj G a b ∧ Adj G a c ∧ Adj G b c
simp only [isNClique_iff, isClique_iff, Set.pairwise_insert_of_symmetric G.symm, coe_insert]
no goals
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
by_cases hab : a = b <;> by_cases hbc : b = c <;> by_cases hac : a = c <;> subst_vars <;>
  simp [G.ne_of_adj, and_rotate, *]