let l := proj_image H 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_1,
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          x_1 =
        x) ↔
    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₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
⊢ (∃ x_1,
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          x_1 =
        x) ↔
    x ∈ H