Theorem: Graph.SpanningSubtree.path_to_base_eq (GroupComp/Subgraph.lean)

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ (u ⤳[Γ] base Γ) = inv (base Γ ⤳[Γ] u)
Tactic:
apply opp_path_eq_inv
State after:
no goals