Theorem: Graph.SubgroupCover.projections_compose (GroupComp/Graph/SubgroupCover.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ Morphism.comp (groupCoverProj H) (univGroupProj H) = proj G x₀
Tactic:
ext
State after:
case toFuncV.h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x✝ : Vert G x₀
⊢ (Morphism.comp (groupCoverProj H) (univGroupProj H)).toFuncV x✝ = (proj G x₀).toFuncV x✝

case toFuncE.h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x✝ : Edge G x₀
⊢ (Morphism.comp (groupCoverProj H) (univGroupProj H)).toFuncE x✝ = (proj G x₀).toFuncE x✝

State before:
case toFuncV.h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x✝ : Vert G x₀
⊢ (Morphism.comp (groupCoverProj H) (univGroupProj H)).toFuncV x✝ = (proj G x₀).toFuncV x✝
Tactic:
rfl
State after:
no goals

State before:
case toFuncE.h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x✝ : Edge G x₀
⊢ (Morphism.comp (groupCoverProj H) (univGroupProj H)).toFuncE x✝ = (proj G x₀).toFuncE x✝
Tactic:
rfl
State after:
no goals