rw [nbhdRes] at hA
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ¬nbhdRes G v A = ∅
⊢ ∃ w, w ∈ A ∧ Adj G v w
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ¬A ∩ neighborFinset G v = ∅
⊢ ∃ w, w ∈ A ∧ Adj G v w