rw [mem_res_nbhd_iff] at *
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
x : α
hx : x ∈ nbhdRes G i B
⊢ x ∈ nbhdRes G i A
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
x : α
hx : x ∈ B ∧ x ∈ neighborFinset G i
⊢ x ∈ A ∧ x ∈ neighborFinset G i