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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ nbhdRes G v A = filter (fun x => Adj G v x) A
Tactic:
ext x
State after:
case a
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
x : α
⊢ x ∈ nbhdRes G v A ↔ x ∈ filter (fun x => Adj G v x) A

State before:
case a
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
x : α
⊢ x ∈ nbhdRes G v A ↔ x ∈ filter (fun x => Adj G v x) A
Tactic:
rw [nbhdRes,mem_inter,mem_filter,mem_neighborFinset]
State after:
no goals