-- 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
n : ℕ
rw :
  Eq (α :=
    Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) (Functor.obj F.rightDerivedToHomotopyCategory X) ⟶
      HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex) n)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (I.isoRightDerivedToHomotopyCategoryObj F)) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
            φ) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (I.isoRightDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) ≫
        HomologicalComplex.homologyMap (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) φ) n)
⊢ Eq (α :=
    Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) (Functor.obj F.rightDerivedToHomotopyCategory X) ⟶
      HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex) n)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Functor.map F.rightDerivedToHomotopyCategory f) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Iso.hom (J.isoRightDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex))
    ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Iso.hom (I.isoRightDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex)) ≫
      HomologicalComplex.homologyMap (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) φ) n)

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

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