-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
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 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X : C
P : ProjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
h₂ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
        P.complex)
      (Functor.obj F.leftDerivedToHomotopyCategory X))
    (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj F))
    (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
      (lift (𝟙 X) P (projectiveResolution X)))
h₁ :
  Eq (α :=
    HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.opcycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
          0)
        (HomologicalComplex.opcyclesMap
            (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) (lift (𝟙 X) P (projectiveResolution X))) 0 :
          HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶
            HomologicalComplex.opcycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
              0)
        (fromLeftDerivedZero' (projectiveResolution X) F :
          HomologicalComplex.opcycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
              0 ⟶
            F.obj X) :
      HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
    (P.fromLeftDerivedZero' F :
      HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
erw :
  Eq (α :=
    Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0)
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
          P.complex) ⟶
      F.obj X)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0) (Functor.obj F.leftDerivedToHomotopyCategory X))
      (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0)
        (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (lift (𝟙 X) P (projectiveResolution X))))
      (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X))) ≫
        HomologicalComplex.homologyι
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X)))
            0 ≫
          fromLeftDerivedZero' (projectiveResolution X) F))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0)
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X))))
      (Functor.map
        (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0)
        (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) (lift (𝟙 X) P (projectiveResolution X))))
      (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X))) ≫
        HomologicalComplex.homologyι
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
            0 ≫
          fromLeftDerivedZero' (projectiveResolution X) F))
⊢ Eq (α :=
    Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0)
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
          P.complex) ⟶
      F.obj X)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0) (Functor.obj F.leftDerivedToHomotopyCategory X))
      (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0)
        (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (lift (𝟙 X) P (projectiveResolution X))))
      (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X))) ≫
        HomologicalComplex.homologyι
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X)))
            0 ≫
          fromLeftDerivedZero' (projectiveResolution X) F))
    (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
      CategoryStruct.comp (Y :=
        HomologicalComplex.homology
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
          0)
        (HomologicalComplex.homologyMap
            (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) (lift (𝟙 X) P (projectiveResolution X))) 0 :
          HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶
            HomologicalComplex.homology
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
              0)
        (HomologicalComplex.homologyι
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
              0 ≫
            fromLeftDerivedZero' (projectiveResolution X) F :
          HomologicalComplex.homology
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
              0 ⟶
            F.obj X))

Tactic:
erw [← NatTrans.naturality_assoc]

Premises used: CategoryTheory.NatTrans.naturality_assoc