-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
rw :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ))
          (Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) X))))
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex)))
    (Functor.map (F.mapHomotopyCategory (ComplexShape.up ℕ)) (Iso.hom I.iso) ≫
        Functor.map (F.mapHomotopyCategory (ComplexShape.up ℕ))
            (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ) ≫
          NatTrans.app (Iso.hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ))) J.cocomplex :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (Functor.obj (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℕ)) (F.mapHomotopyCategory (ComplexShape.up ℕ))
          (Functor.obj (injectiveResolutions C) X))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex)))
    (CategoryStruct.comp (Y :=
      Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ))
          ((Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex).as (r :=
            homotopic C (ComplexShape.up ℕ)))))
      (Functor.map (F.mapHomotopyCategory (ComplexShape.up ℕ)) (Iso.hom I.iso) :
        Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (Functor.obj (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomotopyCategory (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) X))
          (Functor.obj (F.mapHomotopyCategory (ComplexShape.up ℕ))
            (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex)))
      (CategoryStruct.comp (Y :=
          Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex))
          (NatTrans.app (Iso.hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ))) I.cocomplex :
            Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ) ⋙ F.mapHomotopyCategory (ComplexShape.up ℕ))
                I.cocomplex)
              (Functor.obj
                (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
                I.cocomplex))
          (Functor.map (HomotopyCategory.quotient D (ComplexShape.up ℕ))
              (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) φ) :
            Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
                (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex))
              (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
                (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex))) :
        Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ))
              ((Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex).as (r :=
                homotopic C (ComplexShape.up ℕ)))))
          (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex))))
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ))
          (Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) X))))
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex)))
    (CategoryStruct.comp (Y :=
        Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y))))
        (Functor.map (F.mapHomotopyCategory (ComplexShape.up ℕ)) (Functor.map (injectiveResolutions C) f) :
          Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (Functor.obj (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomotopyCategory (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) X))
            (Functor.obj (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomotopyCategory (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y)))
        (CategoryStruct.comp (Y :=
          Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ))
              ((Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) J.cocomplex).as (r :=
                homotopic C (ComplexShape.up ℕ)))))
          (Functor.map (F.mapHomotopyCategory (ComplexShape.up ℕ)) (Iso.hom J.iso) :
            Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (Functor.obj (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomotopyCategory (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y))
              (Functor.obj (F.mapHomotopyCategory (ComplexShape.up ℕ))
                (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) J.cocomplex)))
          (NatTrans.app (Iso.hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ))) J.cocomplex :
            Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ) ⋙ F.mapHomotopyCategory (ComplexShape.up ℕ))
                J.cocomplex)
              (Functor.obj
                (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
                J.cocomplex))) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) X))))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex)))
    (CategoryStruct.comp (Y :=
          Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ))
              ((Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex).as (r :=
                homotopic C (ComplexShape.up ℕ)))))
          (Functor.map (F.mapHomotopyCategory (ComplexShape.up ℕ)) (Iso.hom I.iso) :
            Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (Functor.obj (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomotopyCategory (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) X))
              (Functor.obj (F.mapHomotopyCategory (ComplexShape.up ℕ))
                (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex)))
          (NatTrans.app (Iso.hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ))) I.cocomplex :
            Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ) ⋙ F.mapHomotopyCategory (ComplexShape.up ℕ))
                I.cocomplex)
              (Functor.obj
                (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
                I.cocomplex)) ≫
        Functor.map (HomotopyCategory.quotient D (ComplexShape.up ℕ))
          (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) φ) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) X))))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.up ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex)))

Tactic:
rw [← Functor.map_comp_assoc, iso_hom_naturality f I J φ comm, Functor.map_comp,
    assoc, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.InjectiveResolution.iso_hom_naturality, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp