cases hx with
| inl hx => 
  cases hy with
  | inl hy => rw [hx,hy] at hne; contradiction
  | inr hy => 
    rw [hx]; 
    apply G.subset_res_nbhd hB hy
| inr hx => 
  cases hy with
  | inl hy => 
    rw [hy, G.adj_comm]
    apply G.subset_res_nbhd hB hx
  | inr hy => exact h hx hy hne
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x : α
hx : x ∈ insert v ↑B
y : α
hy : y ∈ insert v ↑B
hne : x ≠ y
⊢ Adj G x y
no goals