∀ (k G : Type u_1) [inst : CommRing k] [inst_1 : Monoid G] (X : Rep k G) (x : G),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.id (Rep k G)).obj X).ρ x)
      ((Rep.coinvariantsMk k G).app X) =
    CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app X)
      ((((Rep.coinvariantsFunctor k G).comp (Rep.trivialFunctor k G)).obj X).ρ x)