simp [Morphism.π₁map, PathClass.map]
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ Quot.mk Reduction η =
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h'
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ Quot.mk Reduction η =
    [[EdgePath.map
        (shiftTarget
          (lift (reduction η) (groupCoverProj H) (basepoint H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
          term_lift')
        (groupCoverProj H)]]