-- 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 : C
I : InjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
h₁ :
  Eq (α :=
    F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
    (I.toRightDerivedZero' F :
      F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.cycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
          0)
        (toRightDerivedZero' (injectiveResolution X) F :
          F.obj X ⟶
            HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0)
        (HomologicalComplex.cyclesMap
            (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) (desc (𝟙 X) I (injectiveResolution X))) 0 :
          HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0 ⟶
            HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0) :
      F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
h₂ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (Functor.obj F.rightDerivedToHomotopyCategory X)
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
        I.cocomplex))
    (Iso.hom (I.isoRightDerivedToHomotopyCategoryObj F))
    (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
      (desc (𝟙 X) I (injectiveResolution X)))
rw :
  Eq (α :=
    F.obj X ⟶
      Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0)
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
          I.cocomplex))
    (CategoryStruct.comp (Y :=
        HomologicalComplex.cycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
          0)
        (toRightDerivedZero' (injectiveResolution X) F :
          F.obj X ⟶
            HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0)
        (HomologicalComplex.homologyπ
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0 ≫
            CategoryStruct.comp (Y :=
              Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
                (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0)
                (Functor.obj F.rightDerivedToHomotopyCategory X))
              (NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0))
                (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                  (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X))))
              (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0)
                (Functor.map
                  (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
                  (desc (𝟙 X) I (injectiveResolution X)))) :
          HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0 ⟶
            Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0)
              (Functor.obj
                (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
                I.cocomplex)) :
      F.obj X ⟶
        Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0)
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
            I.cocomplex))
    (CategoryStruct.comp (Y :=
        HomologicalComplex.cycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
          0)
        (toRightDerivedZero' (injectiveResolution X) F :
          F.obj X ⟶
            HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0)
        (HomologicalComplex.homologyπ
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0 ≫
            HomologicalComplex.homologyMap
                (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) (desc (𝟙 X) I (injectiveResolution X))) 0 ≫
              NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0))
                (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) :
          HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0 ⟶
            Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0)
              (Functor.obj
                (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
                I.cocomplex)) :
      F.obj X ⟶
        Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0)
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
            I.cocomplex))
⊢ Eq (α := F.obj X ⟶ (F.rightDerived 0).obj X)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.cycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
          0)
        (toRightDerivedZero' (injectiveResolution X) F :
          F.obj X ⟶
            HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0)
        (HomologicalComplex.homologyπ
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0 ≫
            NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0))
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X))) :
          HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0 ⟶
            (F.rightDerived 0).obj X) :
      F.obj X ⟶ (F.rightDerived 0).obj X)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
        (I.toRightDerivedZero' F :
          F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
        (HomologicalComplex.homologyπ (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0 ≫
            NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0))
                (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) ≫
              Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0)
                (Iso.inv (I.isoRightDerivedToHomotopyCategoryObj F)) :
          HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0 ⟶
            (F.rightDerived 0).obj X) :
      F.obj X ⟶ (F.rightDerived 0).obj X)

Tactic:
rw [← cancel_mono ((HomotopyCategory.homologyFunctor _ _ 0).map
      (I.isoRightDerivedToHomotopyCategoryObj F).hom),
    assoc, assoc, assoc, assoc, assoc, ← Functor.map_comp,
    Iso.inv_hom_id, Functor.map_id, comp_id,
    reassoc_of% h₁, h₂, ← HomologicalComplex.homologyπ_naturality_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, HomologicalComplex.homologyπ_naturality_assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, CategoryTheory.Functor.map_id, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj, CategoryTheory.Functor.map_comp, HomotopyCategory.homologyFunctor, OfNat.ofNat, CategoryTheory.Iso.hom