∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.Abelian D] {C : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} C] [inst_3 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  (P : CategoryTheory.InjectiveResolution X) (Q : CategoryTheory.InjectiveResolution Y) (φ : P.cocomplex ⟶ Q.cocomplex),
  CategoryTheory.CategoryStruct.comp (P.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (Q.ι.f 0) →
    ∀ (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {Z : D}
      (h : ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj Q.cocomplex).cycles 0 ⟶ Z),
      CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (Q.toRightDerivedZero' F) h) =
        CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F)
          (CategoryTheory.CategoryStruct.comp
            (HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0) h)