ι : Sort ?u.274831
𝕜 : Type ?u.274834
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 ↑(neighborSet G v)
inst✝ : DecidableEq V
⊢ Fintype.card ↑(neighborSet G v) = degree G v
ι : Sort ?u.274831
𝕜 : Type ?u.274834
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 ↑(neighborSet G v)
inst✝ : DecidableEq V
⊢ Fintype.card ↑(incidenceSet G v) = degree G v
rw [Fintype.card_congr (G.incidenceSetEquivNeighborSet v)]
no goals
ι : Sort ?u.274831
𝕜 : Type ?u.274834
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 ↑(neighborSet G v)
inst✝ : DecidableEq V
⊢ Fintype.card ↑(neighborSet G v) = degree G v
simp