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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ surroundEdge Γ e = 𝟙 (base Γ)
Tactic:
simp [surroundEdge, Γ.singleton_tree_path heΓ]
State after:
no goals