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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ surround Γ (𝟙 u) = 𝟙 (base Γ)
Tactic:
simp only [surround, path_to_base_eq, Category.id_comp, IsIso.hom_inv_id]
State after:
no goals