∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep k G) [inst_2 : A.IsTrivial],
  groupCohomology.H1IsoOfIsTrivial A =
    (HomologicalComplex.isoHomologyπ (groupCohomology.inhomogeneousCochains A) 0 1
          groupCohomology.H1IsoOfIsTrivial._proof_2 ⋯).symm ≪≫
      groupCohomology.isoCocycles₁ A ≪≫ groupCohomology.cocycles₁IsoOfIsTrivial A