∀ (k : Type u_1) {G : Type u_1} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G) [inst_2 : S.Normal]
  {X Y : Rep k G} (f : X ⟶ Y) (g : G),
  CategoryTheory.CategoryStruct.comp ((X.quotientToInvariants S).ρ ↑g)
      ((Rep.invariantsFunctor k ↥S).map ((Action.res (ModuleCat k) S.subtype).map f)) =
    CategoryTheory.CategoryStruct.comp ((Rep.invariantsFunctor k ↥S).map ((Action.res (ModuleCat k) S.subtype).map f))
      ((Y.quotientToInvariants S).ρ ↑g)