ι : Sort ?u.202740
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : ↑G'.verts
inst✝¹ : Fintype ↑(SimpleGraph.neighborSet (Subgraph.coe G') v)
inst✝ : Fintype ↑(neighborSet G' ↑v)
⊢ Fintype.card ↑(SimpleGraph.neighborSet (Subgraph.coe G') v) = degree G' ↑v
ι : Sort ?u.202740
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : ↑G'.verts
inst✝¹ : Fintype ↑(SimpleGraph.neighborSet (Subgraph.coe G') v)
inst✝ : Fintype ↑(neighborSet G' ↑v)
⊢ SimpleGraph.degree (Subgraph.coe G') v = degree G' ↑v
rw [← card_neighborSet_eq_degree]
no goals
ι : Sort ?u.202740
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
v : ↑G'.verts
inst✝¹ : Fintype ↑(SimpleGraph.neighborSet (Subgraph.coe G') v)
inst✝ : Fintype ↑(neighborSet G' ↑v)
⊢ Fintype.card ↑(SimpleGraph.neighborSet (Subgraph.coe G') v) = degree G' ↑v
exact Fintype.card_congr (coeNeighborSetEquiv v)