∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupHomology.H1CoresCoinf A S).f =
    groupHomology.map S.subtype (CategoryTheory.CategoryStruct.id ((Action.res (ModuleCat k) S.subtype).obj A)) 1