Theorem: hom_induce_induce_eq_self (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
⊢ GroupLabelledGraph.inducedHom (inducedLabelling φ) = φ
Tactic:
ext x
State after:
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

State before:
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
Tactic:
revert x
State after:
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

State before:
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
Tactic:
apply Graph.PathClass.ind
State after:
case h.a
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
⊢ ∀ (p : Graph.EdgePath X (Graph.SpanningSubtree.base Γ) (Graph.SpanningSubtree.base Γ)),
    (GroupLabelledGraph.inducedHom (inducedLabelling φ)) [[p]] = φ [[p]]

State before:
case h.a
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
⊢ ∀ (p : Graph.EdgePath X (Graph.SpanningSubtree.base Γ) (Graph.SpanningSubtree.base Γ)),
    (GroupLabelledGraph.inducedHom (inducedLabelling φ)) [[p]] = φ [[p]]
Tactic:
intro p
State after:
case h.a
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
p : Graph.EdgePath X (Graph.SpanningSubtree.base Γ) (Graph.SpanningSubtree.base Γ)
⊢ (GroupLabelledGraph.inducedHom (inducedLabelling φ)) [[p]] = φ [[p]]

State before:
case h.a
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
p : Graph.EdgePath X (Graph.SpanningSubtree.base Γ) (Graph.SpanningSubtree.base Γ)
⊢ (GroupLabelledGraph.inducedHom (inducedLabelling φ)) [[p]] = φ [[p]]
Tactic:
simp only [GroupLabelledGraph.inducedHom, MonoidHom.coe_mk, OneHom.coe_mk,
  GroupLabelledGraph.pathClassLabel_of_pathLabel, label_path_map, Graph.SpanningSubtree.surround_loop]
State after:
no goals