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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v w : V
p : u ⟶ v
q : v ⟶ w
⊢ surround Γ p ≫ surround Γ q = surround Γ (p ≫ q)
Tactic:
simp only [surround, path_to_base_eq, Category.assoc, IsIso.inv_hom_id_assoc]
State after:
no goals