∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep k G} (f : A ⟶ B) (x : ↑(groupHomology A 0)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H0Iso B).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.map (MonoidHom.id G) f 0)) x) =
    (Representation.Coinvariants.map A.ρ B.ρ (ModuleCat.Hom.hom f.hom) ⋯)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.H0Iso A).hom) x)