-- 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 :
  (Iso.inv (I.isoRightDerivedObj F n) ≫ (F.rightDerived n).map f) ≫ Iso.hom (J.isoRightDerivedObj F n) =
    CategoryStruct.comp (Y := (F.rightDerived n).obj Y)
      (Functor.map
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          φ ≫
        Iso.inv (J.isoRightDerivedObj F n))
      (Iso.hom (J.isoRightDerivedObj F n))
rw₁ :
  Iso.inv (I.isoRightDerivedObj F n) ≫ (F.rightDerived n).map f ≫ Iso.hom (J.isoRightDerivedObj F n) =
    CategoryStruct.comp (Y := (F.rightDerived n).obj Y)
      (Functor.map
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          φ ≫
        Iso.inv (J.isoRightDerivedObj F n))
      (Iso.hom (J.isoRightDerivedObj F n))
rw₂ :
  Iso.inv (I.isoRightDerivedObj F n) ≫ (F.rightDerived n).map f ≫ Iso.hom (J.isoRightDerivedObj F n) =
    CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
        J.cocomplex)
      (Functor.map
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          φ :
        Functor.obj
            (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
            I.cocomplex ⟶
          Functor.obj
            (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
            J.cocomplex)
      (CategoryStruct.comp (Y := (F.rightDerived n).obj Y) (Iso.inv (J.isoRightDerivedObj F n))
          (Iso.hom (J.isoRightDerivedObj F n)) :
        Functor.obj
            (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
            J.cocomplex ⟶
          Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex))
rw₃ :
  Eq (α :=
    Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) ⟶
      Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex))
    (CategoryStruct.comp (Y := (F.rightDerived n).obj X) (Iso.inv (I.isoRightDerivedObj F n))
        (Iso.hom (I.isoRightDerivedObj F n) ≫
          Functor.map
            (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
            φ) :
      Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) ⟶
        Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex))
    (CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          J.cocomplex)
        (Functor.map
            (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
            φ :
          Functor.obj
              (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ))
                (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
              I.cocomplex ⟶
            Functor.obj
              (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ))
                (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
              J.cocomplex)
        (CategoryStruct.comp (Y := (F.rightDerived n).obj Y) (Iso.inv (J.isoRightDerivedObj F n))
            (Iso.hom (J.isoRightDerivedObj F n)) :
          Functor.obj
              (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ))
                (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
              J.cocomplex ⟶
            Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
              (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex)) :
      Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) ⟶
        Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex))
rw₄ :
  Eq (α :=
    Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) ⟶
      Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex))
    (Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
        φ :
      Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          I.cocomplex ⟶
        Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          J.cocomplex)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
        J.cocomplex)
      (Functor.map
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          φ :
        Functor.obj
            (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
            I.cocomplex ⟶
          Functor.obj
            (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
            J.cocomplex)
      (CategoryStruct.comp (Y := (F.rightDerived n).obj Y) (Iso.inv (J.isoRightDerivedObj F n))
          (Iso.hom (J.isoRightDerivedObj F n)) :
        Functor.obj
            (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
            J.cocomplex ⟶
          Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex)))
rw₅ :
  Functor.map
      (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
      φ =
    Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
        φ ≫
      𝟙
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          J.cocomplex)
rw₆ rw₇ :
  Eq (α :=
    Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) ⟶
      Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex))
    (Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
        φ :
      Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          I.cocomplex ⟶
        Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          J.cocomplex)
    (Functor.map
      (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
      φ)
⊢ Iso.inv (I.isoRightDerivedObj F n) ≫ (F.rightDerived n).map f =
    Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
        φ ≫
      Iso.inv (J.isoRightDerivedObj F n)

Tactic:
rw [← cancel_mono (J.isoRightDerivedObj F n).hom, assoc, assoc,
    InjectiveResolution.isoRightDerivedObj_hom_naturality f I J φ comm F n,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.InjectiveResolution.isoRightDerivedObj, CategoryTheory.Iso.inv_hom_id, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.hom