∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_3}
  [inst_2 : CategoryTheory.Category.{u_2, u_3} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] (X : C) ⦃X_1 Y : Cᵒᵖ⦄ (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.preadditiveYoneda.obj X).map f)
      (AddCommGrpCat.ofHom F.mapAddHom) =
    CategoryTheory.CategoryStruct.comp (AddCommGrpCat.ofHom F.mapAddHom)
      ((F.op.comp (CategoryTheory.preadditiveYoneda.obj (F.obj X))).map f)