no goals
ι : Sort ?u.283769
𝕜 : Type ?u.283772
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
⊢ neighborFinset (Gᶜ) v = neighborFinset G vᶜ \ {v}
simp only [neighborFinset, neighborSet_compl, Set.toFinset_diff, Set.toFinset_compl,
  Set.toFinset_singleton]