Theorem: Graph.pathLabel_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.113042
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
p : EdgePath X u v
hpΓ : Subgraph.contains Γ.toSubgraph p
⊢ GroupLabelledGraph.pathLabel (SpanningSubtree.edgeLabelExtension φ) p = 1
Tactic:
induction p with
  | nil _ => simp
  | cons _ _ ih => simp_all [ih]
State after:
no goals

State before:
case nil
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.113042
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✝ : V
hpΓ : Subgraph.contains Γ.toSubgraph (EdgePath.nil v✝)
⊢ GroupLabelledGraph.pathLabel (SpanningSubtree.edgeLabelExtension φ) (EdgePath.nil v✝) = 1
Tactic:
simp
State after:
no goals

State before:
case cons
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.113042
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✝ w✝ u✝ : V
a✝¹ : EdgeBetween X v✝ w✝
a✝ : EdgePath X w✝ u✝
ih : Subgraph.contains Γ.toSubgraph a✝ → GroupLabelledGraph.pathLabel (SpanningSubtree.edgeLabelExtension φ) a✝ = 1
hpΓ : Subgraph.contains Γ.toSubgraph (EdgePath.cons a✝¹ a✝)
⊢ GroupLabelledGraph.pathLabel (SpanningSubtree.edgeLabelExtension φ) (EdgePath.cons a✝¹ a✝) = 1
Tactic:
simp_all [ih]
State after:
no goals