no goals
ι : Sort ?u.286096
𝕜 : Type ?u.286099
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
v : V
⊢ degree ⊤ v = Fintype.card V - 1
erw [degree, neighborFinset_eq_filter, filter_ne, card_erase_of_mem (mem_univ v), card_univ]