apply MulEquiv.trans lem
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
lem : π₁ (groupCover H) (basepoint H) ≃*
  ↥(MonoidHom.range
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) :=
  MonoidHom.ofInjective hf
⊢ π₁ (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
lem : π₁ (groupCover H) (basepoint H) ≃*
  ↥(MonoidHom.range
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) :=
  MonoidHom.ofInjective hf
⊢ ↥(MonoidHom.range
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) ≃*
    ↥H