no goals
ι : Sort ?u.200590
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : V
inst✝ : Fintype ↑(neighborSet G' v)
⊢ Finset.card (Set.toFinset (neighborSet G' v)) = degree G' v
rw [degree, Set.toFinset_card]