∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.π A 2) (groupHomology.H2Iso A).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).hom
      (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.π