simp only [Γ.surround_cons, GroupLabelledGraph.pathLabel_cons, ih,
Graph.π₁.mul_def, map_mul, mul_right_cancel_iff, induced_label_eq_surround_map]
case cons
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✝ w✝ u✝ : V
e : Graph.EdgeBetween X v✝ w✝
p : Graph.EdgePath X w✝ u✝
ih : GroupLabelledGraph.pathLabel (inducedLabelling φ) p = φ (Graph.SpanningSubtree.surround Γ [[p]])
⊢ GroupLabelledGraph.pathLabel (inducedLabelling φ) (Graph.EdgePath.cons e p) =
    φ (Graph.SpanningSubtree.surround Γ [[Graph.EdgePath.cons e p]])
no goals