Theorem: Graph.τ_bar (GroupComp/Graph.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : E
⊢ τ G (G.bar e) = G.ι e
Tactic:
aesop (add norm unfold [τ])
State after:
no goals