∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] {X Y : Rep.{w, u, v} k G} (f : X ⟶ Y),
  ModuleCat.Hom.hom ((Rep.coinvariantsFunctor k G).map f) =
    Representation.Coinvariants.map X.ρ Y.ρ (Rep.Hom.hom f).toLinearMap ⋯