rw [mem_res_nbhd_iff, mem_filter, mem_neighborFinset]
case e_f.h.e_s.a
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x a✝ : α
⊢ a✝ ∈ nbhdRes G x (A \ B) ↔ a✝ ∈ filter (fun x_1 => Adj G x x_1) (A \ B)
no goals