revert x
case h
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
x : Graph.π₁ X (Graph.SpanningSubtree.base Γ)
⊢ (GroupLabelledGraph.inducedHom (inducedLabelling φ)) x = φ x
case h
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
⊢ ∀ (x : Graph.π₁ X (Graph.SpanningSubtree.base Γ)), (GroupLabelledGraph.inducedHom (inducedLabelling φ)) x = φ x