rw [neighborFinset_def, Set.coe_toFinset]
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G : SimpleGraph V
x : V
inst✝ : Fintype ↑(neighborSet G x)
⊢ ↑(neighborFinset G x) = neighborSet G x
no goals