∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep k G) [inst_2 : A.IsTrivial] (g : G) (a : ↑A.V),
  (groupHomology.H1AddEquivOfIsTrivial A)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A))
        ((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial A).inv) fun₀ | g => a)) =
    Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a