rw [GroupLabelledGraph.pathLabel_nil, Graph.PathClass.nil_eq_id, Γ.surround_nil,
Graph.π₁.one_def, map_one]
case nil
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
u v v✝ : V
⊢ GroupLabelledGraph.pathLabel (inducedLabelling φ) (Graph.EdgePath.nil v✝) =
    φ (Graph.SpanningSubtree.surround Γ [[Graph.EdgePath.nil v✝]])
no goals