-- 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
F G : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution.{v, u} X
n : ℕ
erw :
  Eq (α := (F.rightDerived n).obj X ⟶ (G.rightDerived n).obj X)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (P.isoRightDerivedToHomotopyCategoryObj F)) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Functor.map (HomotopyCategory.quotient D (ComplexShape.up ℕ))
            (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex)) ≫
        Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Iso.inv (P.isoRightDerivedToHomotopyCategoryObj G)))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (P.isoRightDerivedToHomotopyCategoryObj F)) ≫
      Functor.map
          (HomotopyCategory.quotient D (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
            (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) ≫
          NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
              (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) ≫
            Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
              (Iso.inv (P.isoRightDerivedToHomotopyCategoryObj G)))
⊢ Eq (α := (F.rightDerived n).obj X ⟶ (G.rightDerived n).obj X)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (P.isoRightDerivedToHomotopyCategoryObj F)) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Functor.map (HomotopyCategory.quotient D (ComplexShape.up ℕ))
            (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex)) ≫
        Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Iso.inv (P.isoRightDerivedToHomotopyCategoryObj G)))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (P.isoRightDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) ≫
        HomologicalComplex.homologyMap (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex)
            n ≫
          NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
              (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) ≫
            Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
              (Iso.inv (P.isoRightDerivedToHomotopyCategoryObj G)))

Tactic:
erw [← (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.naturality_assoc
    ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)]

Premises used: HomotopyCategory.homologyFunctorFactors, CategoryTheory.NatTrans.mapHomologicalComplex, Nat, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, CategoryTheory.NatTrans.naturality_assoc, ComplexShape.up, CategoryTheory.InjectiveResolution.cocomplex