rw [surroundEdge, surroundEdge, ← surround_inv, Graph.EdgePath.singletonPath_bar,
  Graph.PathClass.reverse_class_eq_inv, Graph.PathClass.inv_eq_inv]
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
⊢ surroundEdge Γ (EdgeBetween.bar e) = inv (surroundEdge Γ e)
no goals