simp_all [ih]
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
no goals