Theorem: GroupLabelledGraph.pathLabel_singletonPath (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
e : Graph.EdgeBetween Γ u v
⊢ pathLabel 𝓖 (Graph.singletonPath e) = 𝓖.label e
Tactic:
simp
State after:
no goals