∀ (k : Type u_1) {G : Type u_1} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G) [inst_2 : S.Normal] (n : ℕ)
  {X Y : Rep.{u_1, u_1, u_1} k G} (φ : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((Rep.quotientToInvariantsFunctor k S).comp (groupCohomology.functor k (G ⧸ S) n)).map φ)
      (groupCohomology.map (QuotientGroup.mk' S) (Rep.ofHom (Y.ρ.quotientToInvariants_lift S)) n) =
    CategoryTheory.CategoryStruct.comp
      (groupCohomology.map (QuotientGroup.mk' S) (Rep.ofHom (X.ρ.quotientToInvariants_lift S)) n)
      ((groupCohomology.functor k G n).map φ)