∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] (F : C ⥤ₗ AddCommGrpCat) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.id (C ⥤ₗ AddCommGrpCat)).obj F).obj.map f)
      ((fun X =>
            commGroupAddCommGroupEquivalence.counitIso.app
                (((CategoryTheory.Functor.id (C ⥤ₗ AddCommGrpCat)).obj F).obj.1 X) ≪≫
              (CommGrpCat.toAddCommGrp.mapIso
                    (commGrpTypeEquivalenceCommGrp.counitIso.app (AddCommGrpCat.toCommGrp.obj (F.obj.obj X)))).symm ≪≫
                CommGrpCat.toAddCommGrp.mapIso
                  (CommGrpTypeEquivalenceCommGrp.functor.mapIso
                    (AddCommGrpCat.leftExactFunctorForgetEquivalence.unitIsoAux F.obj X)))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X =>
            commGroupAddCommGroupEquivalence.counitIso.app
                (((CategoryTheory.Functor.id (C ⥤ₗ AddCommGrpCat)).obj F).obj.1 X) ≪≫
              (CommGrpCat.toAddCommGrp.mapIso
                    (commGrpTypeEquivalenceCommGrp.counitIso.app (AddCommGrpCat.toCommGrp.obj (F.obj.obj X)))).symm ≪≫
                CommGrpCat.toAddCommGrp.mapIso
                  (CommGrpTypeEquivalenceCommGrp.functor.mapIso
                    (AddCommGrpCat.leftExactFunctorForgetEquivalence.unitIsoAux F.obj X)))
          X).hom
      (((((CategoryTheory.LeftExactFunctor.whiskeringRight C AddCommGrpCat (Type u_1)).obj
                      (CategoryTheory.LeftExactFunctor.of (CategoryTheory.forget AddCommGrpCat))).comp
                  AddCommGrpCat.leftExactFunctorForgetEquivalence.inverse).obj
              F).obj.map
        f)