Theorem: SimpleGraph.adj_is2Clique (Turan4/CliqueFreeSets.lean)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : Adj G a b
⊢ IsNClique G 2 {a, b}
Tactic:
rw [isNClique_iff, coe_insert, coe_singleton, isClique_iff, Set.pairwise_pair_of_symmetric G.symm]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : Adj G a b
⊢ (a ≠ b → Adj G a b) ∧ card {a, b} = 2

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : Adj G a b
⊢ (a ≠ b → Adj G a b) ∧ card {a, b} = 2
Tactic:
exact ⟨fun _ => h, card_eq_two.2 ⟨a,b,G.ne_of_adj h,rfl⟩⟩
State after:
no goals