rw [mem_inter, mem_neighborFinset] at hx
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
x : α
hx : x ∈ A ∩ neighborFinset G v
⊢ False
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
x : α
hx : x ∈ A ∧ Adj G v x
⊢ False