Theorem: GroupLabelledGraph.pathLabel_concat (GroupComp/GroupLabelledGraph.lean)

State before:
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
Tactic:
induction p <;> aesop (add norm simp [Graph.EdgePath.concat, mul_assoc])
State after:
no goals