intro x
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (x : π₁ G x₀),
    x ∈
        MonoidHom.range
          (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) ↔
      x ∈ 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₀)
x : π₁ G x₀
⊢ x ∈
      MonoidHom.range
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) ↔
    x ∈ H