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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : EdgePath G u v
⊢ surround Γ [[p]] = surroundEdgewise Γ p
Tactic:
induction p with
| nil _ => 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]
| cons _ _ ih => simp only [surroundEdgewise_cons, ← ih, surround_cons]
State after:
no goals

State before:
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✝)
Tactic:
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]
State after:
no goals

State before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v v✝ w✝ u✝ : V
a✝¹ : EdgeBetween G v✝ w✝
a✝ : EdgePath G w✝ u✝
ih : surround Γ [[a✝]] = surroundEdgewise Γ a✝
⊢ surround Γ [[EdgePath.cons a✝¹ a✝]] = surroundEdgewise Γ (EdgePath.cons a✝¹ a✝)
Tactic:
simp only [surroundEdgewise_cons, ← ih, surround_cons]
State after:
no goals