-- 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 Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
φ : P.complex ⟶ Q.complex
comm :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Y) 0) (φ.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
erw :
  Eq (α :=
    Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) (Functor.obj F.leftDerivedToHomotopyCategory X) ⟶
      HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex) n)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
        Functor.map (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)
          (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
        HomologicalComplex.homologyMap (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) n)
⊢ Eq (α :=
    Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) (Functor.obj F.leftDerivedToHomotopyCategory X) ⟶
      HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex) n)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Functor.map
            (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)) φ) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
        HomologicalComplex.homologyMap (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) n)

Tactic:
erw [(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.naturality]

Premises used: HomotopyCategory.homologyFunctorFactors, CategoryTheory.NatTrans.naturality, Nat, ComplexShape.down, CategoryTheory.Iso.hom