Theorem: label_path_map (GroupComp/FundamentalGroup.lean)

State before:
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
u v : V
p : Graph.EdgePath X u v
⊢ GroupLabelledGraph.pathLabel (inducedLabelling φ) p = φ (Graph.SpanningSubtree.surround Γ [[p]])
Tactic:
induction p with
  | nil _ => rw [GroupLabelledGraph.pathLabel_nil, Graph.PathClass.nil_eq_id, Γ.surround_nil,
      Graph.π₁.one_def, map_one]
  | cons e p ih => simp only [Γ.surround_cons, GroupLabelledGraph.pathLabel_cons, ih,
      Graph.π₁.mul_def, map_mul, mul_right_cancel_iff, induced_label_eq_surround_map]
State after:
no goals

State before:
case nil
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
u v v✝ : V
⊢ GroupLabelledGraph.pathLabel (inducedLabelling φ) (Graph.EdgePath.nil v✝) =
    φ (Graph.SpanningSubtree.surround Γ [[Graph.EdgePath.nil v✝]])
Tactic:
rw [GroupLabelledGraph.pathLabel_nil, Graph.PathClass.nil_eq_id, Γ.surround_nil,
Graph.π₁.one_def, map_one]
State after:
no goals

State before:
case cons
V : Type u_2
E : Type u_3
X : Graph V E
Γ : Graph.SpanningSubtree X
G : Type u_1
inst✝ : Group G
φ : Graph.π₁ X (Graph.SpanningSubtree.base Γ) →* G
u v v✝ w✝ u✝ : V
e : Graph.EdgeBetween X v✝ w✝
p : Graph.EdgePath X w✝ u✝
ih : GroupLabelledGraph.pathLabel (inducedLabelling φ) p = φ (Graph.SpanningSubtree.surround Γ [[p]])
⊢ GroupLabelledGraph.pathLabel (inducedLabelling φ) (Graph.EdgePath.cons e p) =
    φ (Graph.SpanningSubtree.surround Γ [[Graph.EdgePath.cons e p]])
Tactic:
simp only [Γ.surround_cons, GroupLabelledGraph.pathLabel_cons, ih,
Graph.π₁.mul_def, map_mul, mul_right_cancel_iff, induced_label_eq_surround_map]
State after:
no goals