∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep k G) {Z : ModuleCat k}
  (h : (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.π A 1)
      (CategoryTheory.CategoryStruct.comp (groupHomology.H1Iso A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.π h)