Theorem: SimpleGraph.coe_neighborFinset (ExponentialRamsey/Prereq/Mathlib/Combinatorics/SimpleGraph/Basic.lean)

State before:
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
Tactic:
rw [neighborFinset_def, Set.coe_toFinset]
State after:
no goals