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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
p : base Γ ⟶ base Γ
⊢ surround Γ p = p
Tactic:
simp only [surround, tree_path_id, Category.comp_id, Category.id_comp]
State after:
no goals