simp only [GroupLabelledGraph.inducedHom, MonoidHom.coe_mk, OneHom.coe_mk,
  GroupLabelledGraph.pathClassLabel_of_pathLabel, label_path_map, Graph.SpanningSubtree.surround_loop]
case h.a
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
p : Graph.EdgePath X (Graph.SpanningSubtree.base Γ) (Graph.SpanningSubtree.base Γ)
⊢ (GroupLabelledGraph.inducedHom (inducedLabelling φ)) [[p]] = φ [[p]]
no goals