ι : Sort ?u.203693
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)
inst✝ : Fintype ↑(SimpleGraph.neighborSet (Subgraph.spanningCoe G') v)
⊢ Fintype.card ↑(SimpleGraph.neighborSet (Subgraph.spanningCoe G') v) = Fintype.card ↑(neighborSet G' v)
ι : Sort ?u.203693
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)
inst✝ : Fintype ↑(SimpleGraph.neighborSet (Subgraph.spanningCoe G') v)
⊢ SimpleGraph.degree (Subgraph.spanningCoe G') v = degree G' v
rw [← card_neighborSet_eq_degree, Subgraph.degree]
no goals
ι : Sort ?u.203693
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)
inst✝ : Fintype ↑(SimpleGraph.neighborSet (Subgraph.spanningCoe G') v)
⊢ Fintype.card ↑(SimpleGraph.neighborSet (Subgraph.spanningCoe G') v) = Fintype.card ↑(neighborSet G' v)
congr!