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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : u ⟶ v
⊢ surround Γ (inv p) = inv (surround Γ p)
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
p : u ⟶ v
⊢ surround Γ p ≫ surround Γ (inv p) = 𝟙 (base Γ)

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