Theorem: Graph.SpanningSubtree.surroundEdge_bar' (GroupComp/Subgraph.lean)

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
e : E
⊢ surroundEdge Γ (EdgeBetween.ofEdge (G.bar e)) = inv (surroundEdge Γ (EdgeBetween.ofEdge e))
Tactic:
rw [← surroundEdge_bar]
State after:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
e : E
⊢ surroundEdge Γ (EdgeBetween.ofEdge (G.bar e)) = surroundEdge Γ (EdgeBetween.bar (EdgeBetween.ofEdge e))

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
e : E
⊢ surroundEdge Γ (EdgeBetween.ofEdge (G.bar e)) = surroundEdge Γ (EdgeBetween.bar (EdgeBetween.ofEdge e))
Tactic:
apply surroundEdge_cast <;> simp
State after:
no goals