no goals
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
⊢ card (filter (fun d => d.fst = v) univ) = degree G v
simpa only [dart_fst_fiber, Finset.card_univ, card_neighborSet_eq_degree] using
  card_image_of_injective univ (G.dartOfNeighborSet_injective v)