induction p <;> aesop (add norm simp [Graph.EdgePath.concat, mul_assoc])
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
e : Graph.EdgeBetween Γ v w
⊢ pathLabel 𝓖 (Graph.EdgePath.concat p e) = pathLabel 𝓖 p * 𝓖.label e
no goals