-- 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
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
X Y : C
f : X ⟶ Y
rw :
  Eq (α :=
    obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0) (obj F.leftDerivedToHomotopyCategory X) ⟶
      F.obj Y)
    (map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0) (map F.leftDerivedToHomotopyCategory f) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (obj (projectiveResolutions C) Y))) ≫
        HomologicalComplex.homologyι
            (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (obj (projectiveResolutions C) Y)))
            0 ≫
          ProjectiveResolution.fromLeftDerivedZero' (projectiveResolution Y) F)
    (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
        (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ)) (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (obj (projectiveResolutions C) X))) ≫
      CategoryStruct.comp (Y :=
        HomologicalComplex.homology
          (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (ProjectiveResolution.complex (projectiveResolution Y)))
          0)
        (HomologicalComplex.homologyMap
            (map (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y)))
            0 :
          HomologicalComplex.homology
              (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ))
                (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (obj (projectiveResolutions C) X)))
              0 ⟶
            HomologicalComplex.homology
              (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (ProjectiveResolution.complex (projectiveResolution Y)))
              0)
        (HomologicalComplex.homologyι
              (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (ProjectiveResolution.complex (projectiveResolution Y)))
              0 ≫
            ProjectiveResolution.fromLeftDerivedZero' (projectiveResolution Y) F :
          HomologicalComplex.homology
              (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (ProjectiveResolution.complex (projectiveResolution Y)))
              0 ⟶
            F.obj Y))
⊢ Eq (α :=
    obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0) (obj F.leftDerivedToHomotopyCategory X) ⟶
      F.obj Y)
    (map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0) (map F.leftDerivedToHomotopyCategory f) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (obj (projectiveResolutions C) Y))) ≫
        HomologicalComplex.homologyι
            (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (obj (projectiveResolutions C) Y)))
            0 ≫
          ProjectiveResolution.fromLeftDerivedZero' (projectiveResolution Y) F)
    ((NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (obj (projectiveResolutions C) X))) ≫
        HomologicalComplex.homologyι
            (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (obj (projectiveResolutions C) X)))
            0 ≫
          ProjectiveResolution.fromLeftDerivedZero' (projectiveResolution X) F) ≫
      F.map f)

Tactic:
rw [assoc, assoc, ← ProjectiveResolution.fromLeftDerivedZero'_naturality f
      (projectiveResolution X) (projectiveResolution Y)
      (ProjectiveResolution.lift f _ _) (by simp),
      ← HomologicalComplex.homologyι_naturality_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ProjectiveResolution.lift, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality, CategoryTheory.projectiveResolution, HomologicalComplex.homologyι_naturality_assoc