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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
v✝ w✝ : V
e : EdgeBetween G v✝ w✝
a✝ : V
p : EdgePath G w✝ a✝
⊢ surround Γ [[EdgePath.cons e p]] = surroundEdge Γ e ≫ surround Γ [[p]]
Tactic:
erw [Graph.EdgePath.cons_eq_append_singletonPath, surround_append]
State after:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
v✝ w✝ : V
e : EdgeBetween G v✝ w✝
a✝ : V
p : EdgePath G w✝ a✝
⊢ surround Γ [[singletonPath e ++ p]] = surround Γ ([[singletonPath e]] ≫ [[p]])

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
v✝ w✝ : V
e : EdgeBetween G v✝ w✝
a✝ : V
p : EdgePath G w✝ a✝
⊢ surround Γ [[singletonPath e ++ p]] = surround Γ ([[singletonPath e]] ≫ [[p]])
Tactic:
rfl
State after:
no goals