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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v w x : V
p : w ⟶ x
⊢ (u ⤳[Γ] v) ≫ (v ⤳[Γ] w) ≫ p = (u ⤳[Γ] w) ≫ p
Tactic:
rw [← Category.assoc, tree_path_comp]
State after:
no goals