simp only [surround, Subgraph.contains_nil, SpanningSubgraph.spanning, Set.top_eq_univ, Set.mem_univ,
Graph.PathClass.nil_eq_id, path_to_base_eq, Category.id_comp, IsIso.hom_inv_id, surroundEdgewise_nil]
case nil
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v v✝ : V
⊢ surround Γ [[EdgePath.nil v✝]] = surroundEdgewise Γ (EdgePath.nil v✝)
no goals