Theorem: SimpleGraph.subset_res_nbhd (Turan4/NbhdRes.lean)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B : Finset α
v : α
A : Finset α
b : α
h : B ⊆ nbhdRes G v A
hb : b ∈ B
⊢ Adj G v b
Tactic:
exact (mem_neighborFinset _ _ _).1 ((G.mem_res_nbhd_iff _ _ _).1 (h hb)).2
State after:
no goals