-- Mathlib/CategoryTheory/Abelian/RightDerived.lean
/-- A component of the natural transformation between right-derived functors can be computed
using a chosen injective resolution. -/
lemma rightDerived_app_eq
    {F G : C ⥤ D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : InjectiveResolution X)
    (n : ℕ) : (NatTrans.rightDerived α n).app X =
      (P.isoRightDerivedObj F n).hom ≫
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
        ((NatTrans.mapHomologicalComplex α _).app P.cocomplex) ≫
        (P.isoRightDerivedObj G n).inv

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
        HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) n ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
              (P.isoRightDerivedToHomotopyCategoryObj G).inv

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

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
            ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
              (P.isoRightDerivedToHomotopyCategoryObj G).inv

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (NatTrans.rightDerived α n).app X =
    (P.isoRightDerivedObj F n).hom ≫
      (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
        (P.isoRightDerivedObj G n).inv

Tactic:
dsimp [NatTrans.rightDerived, isoRightDerivedObj]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((NatTrans.rightDerivedToHomotopyCategory α).app X) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex)) ≫
      HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) n ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
            ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((NatTrans.rightDerivedToHomotopyCategory α).app X) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex)) ≫
      HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) n ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
            ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv

Tactic:
rw [InjectiveResolution.rightDerivedToHomotopyCategory_app_eq α P,
  Functor.map_comp, Functor.map_comp, assoc]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
        HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) n ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
              (P.isoRightDerivedToHomotopyCategoryObj G).inv