Theorem: Graph.pathClassLabel_on_tree_path (GroupComp/FundamentalGroup.lean)

State before:
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.116565
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
inst✝ : {u v : V} → (e : EdgeBetween X u v) → Decidable (e.edge ∈ Γ.edges)
φ : ↑Γ.edgesᶜ →⁻¹ H
u v : V
⊢ GroupLabelledGraph.pathClassLabel (SpanningSubtree.edgeLabelExtension φ) (u ⤳[Γ] v) = 1
Tactic:
show (Γ.edgeLabelExtension φ).pathClassLabel ([[_]]) = _
State after:
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.116565
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
inst✝ : {u v : V} → (e : EdgeBetween X u v) → Decidable (e.edge ∈ Γ.edges)
φ : ↑Γ.edgesᶜ →⁻¹ H
u v : V
⊢ GroupLabelledGraph.pathClassLabel (SpanningSubtree.edgeLabelExtension φ)
      [[↑((SpanningSubtree.toSubtree Γ).toPreconnectedSubgraph.path (SpanningSubtree.vertex_coe Γ u)
            (SpanningSubtree.vertex_coe Γ v))]] =
    1

State before:
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.116565
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
inst✝ : {u v : V} → (e : EdgeBetween X u v) → Decidable (e.edge ∈ Γ.edges)
φ : ↑Γ.edgesᶜ →⁻¹ H
u v : V
⊢ GroupLabelledGraph.pathClassLabel (SpanningSubtree.edgeLabelExtension φ)
      [[↑((SpanningSubtree.toSubtree Γ).toPreconnectedSubgraph.path (SpanningSubtree.vertex_coe Γ u)
            (SpanningSubtree.vertex_coe Γ v))]] =
    1
Tactic:
simp only [GroupLabelledGraph.pathClassLabel_of_pathLabel, SpanningSubtree.contains_path, pathLabel_on_tree_path]
State after:
no goals