-- 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
rw :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex))
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (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) Y)))))
    (CategoryStruct.comp (Y :=
        Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ))
            ((Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) P.complex).as (r :=
              homotopic C (ComplexShape.down ℕ)))))
        (NatTrans.app (Iso.inv (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ))) P.complex :
          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
              (HomotopyCategory.quotient C (ComplexShape.down ℕ) ⋙ F.mapHomotopyCategory (ComplexShape.down ℕ))
              P.complex))
        (Functor.map (F.mapHomotopyCategory (ComplexShape.down ℕ))
            (Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ) ≫
          Functor.map (F.mapHomotopyCategory (ComplexShape.down ℕ)) (Iso.inv Q.iso)) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (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) Y)))))
    (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) ≫
        CategoryStruct.comp (Y :=
          Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ))
              ((Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) Q.complex).as (r :=
                homotopic C (ComplexShape.down ℕ)))))
          (NatTrans.app (Iso.inv (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ))) Q.complex :
            Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
              (Functor.obj
                (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
                Q.complex)
              (Functor.obj
                (HomotopyCategory.quotient C (ComplexShape.down ℕ) ⋙ F.mapHomotopyCategory (ComplexShape.down ℕ))
                Q.complex))
          (Functor.map (F.mapHomotopyCategory (ComplexShape.down ℕ)) (Iso.inv Q.iso)) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (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) Y)))))
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex))
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (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) Y)))))
    (CategoryStruct.comp (Y :=
        Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (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))))
        (CategoryStruct.comp (Y :=
          Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ))
              ((Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) P.complex).as (r :=
                homotopic C (ComplexShape.down ℕ)))))
          (NatTrans.app (Iso.inv (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ))) P.complex :
            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
                (HomotopyCategory.quotient C (ComplexShape.down ℕ) ⋙ F.mapHomotopyCategory (ComplexShape.down ℕ))
                P.complex))
          (Functor.map (F.mapHomotopyCategory (ComplexShape.down ℕ)) (Iso.inv P.iso)))
        (Functor.map (F.mapHomotopyCategory (ComplexShape.down ℕ)) (Functor.map (projectiveResolutions C) f)) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (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) Y)))))
    (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) ≫
        CategoryStruct.comp (Y :=
          Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ))
              ((Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) Q.complex).as (r :=
                homotopic C (ComplexShape.down ℕ)))))
          (NatTrans.app (Iso.inv (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ))) Q.complex :
            Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
              (Functor.obj
                (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
                Q.complex)
              (Functor.obj
                (HomotopyCategory.quotient C (ComplexShape.down ℕ) ⋙ F.mapHomotopyCategory (ComplexShape.down ℕ))
                Q.complex))
          (Functor.map (F.mapHomotopyCategory (ComplexShape.down ℕ)) (Iso.inv Q.iso)) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (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) Y)))))

Tactic:
rw [assoc, ← Functor.map_comp, iso_inv_naturality f P Q φ comm, Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.ProjectiveResolution.iso_inv_naturality