α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
⊢ Set.Subsingleton ↑s ∧ Finset.card s = n ↔ n ≤ 1 ∧ Finset.card s = n
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
⊢ IsNClique ⊥ n s ↔ n ≤ 1 ∧ Finset.card s = n
rw [isNClique_iff, isClique_bot_iff]
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
⊢ Finset.card s = n → (Set.Subsingleton ↑s ↔ n ≤ 1)
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
⊢ Set.Subsingleton ↑s ∧ Finset.card s = n ↔ n ≤ 1 ∧ Finset.card s = n
refine' and_congr_left _
α : Type u_1
G H : SimpleGraph α
s : Finset α
⊢ Set.Subsingleton ↑s ↔ Finset.card s ≤ 1
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
⊢ Finset.card s = n → (Set.Subsingleton ↑s ↔ n ≤ 1)
rintro rfl
no goals
α : Type u_1
G H : SimpleGraph α
s : Finset α
⊢ Set.Subsingleton ↑s ↔ Finset.card s ≤ 1
exact card_le_one.symm