∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.toCocycles A 0 1) (groupCohomology.isoCocycles₁ A).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₀ A).hom
      (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.f'