simp [Morphism.π₁map, PathClass.map]
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
⊢ (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      (Quot.mk Reduction η) ∈
    H
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
⊢ [[EdgePath.map η (groupCoverProj H)]] ∈ H