let hf :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥H
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥H