induction p with
  | nil _ => rw [GroupLabelledGraph.pathLabel_nil, Graph.PathClass.nil_eq_id, Γ.surround_nil,
      Graph.π₁.one_def, map_one]
  | cons e p ih => simp only [Γ.surround_cons, GroupLabelledGraph.pathLabel_cons, ih,
      Graph.π₁.mul_def, map_mul, mul_right_cancel_iff, induced_label_eq_surround_map]
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
p : Graph.EdgePath X u v
⊢ GroupLabelledGraph.pathLabel (inducedLabelling φ) p = φ (Graph.SpanningSubtree.surround Γ [[p]])
no goals