Theorem: GroupLabelledGraph.pathLabel_reduction (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 : V
p✝ p'✝ : Graph.EdgePath Γ u v
u✝ u'✝ : V
e : Graph.EdgeBetween Γ u✝ u'✝
p : Graph.EdgePath Γ u u✝
p' : Graph.EdgePath Γ u✝ v
⊢ pathLabel 𝓖 (p ++ Graph.EdgePath.cons e (Graph.EdgePath.cons (Graph.EdgeBetween.bar e) p')) = pathLabel 𝓖 (p ++ p')
Tactic:
simp
State after:
no goals