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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
⊢ (u ⤳[Γ] v) = inv (v ⤳[Γ] u)
Tactic:
rw [← hom_comp_eq_id]
State after:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
⊢ ((v ⤳[Γ] u) ≫ u ⤳[Γ] v) = 𝟙 v

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
⊢ ((v ⤳[Γ] u) ≫ u ⤳[Γ] v) = 𝟙 v
Tactic:
trans (v ⤳[Γ] v)
<;> simp
State after:
no goals