-- Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
K : CochainComplex.{v₁, u₁, 0} C₁ ℤ
⊢ Eq.{w₂ + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
      (obj (C := DerivedCategory.{w₁, v₁, u₁} C₁) F.mapDerivedCategory (obj DerivedCategory.Q K))
      (obj DerivedCategory.Q (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) K)))
    (NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) K)
    (map F.mapDerivedCategory (NatTrans.app (Iso.inv (DerivedCategory.quotientCompQhIso C₁)) K) ≫
      𝟙
          (obj (C := DerivedCategory.{w₁, v₁, u₁} C₁) F.mapDerivedCategory
            (obj DerivedCategory.Qh (obj (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) K))) ≫
        NatTrans.app (Iso.hom F.mapDerivedCategoryFactorsh) (obj (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) K) ≫
          𝟙
              (obj DerivedCategory.Qh
                (obj (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ))
                  (obj (F.mapHomologicalComplex (ComplexShape.up ℤ))
                    ((obj (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) K).as (r :=
                      homotopic C₁ (ComplexShape.up ℤ)))))) ≫
            CategoryStruct.comp (Y :=
              obj DerivedCategory.Qh
                (obj (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ))
                  (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) K)))
              (map DerivedCategory.Qh (NatTrans.app (Iso.hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ))) K) :
                Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
                  (obj DerivedCategory.Qh
                    (obj (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ))
                      (obj (F.mapHomologicalComplex (ComplexShape.up ℤ))
                        ((obj (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) K).as (r :=
                          homotopic C₁ (ComplexShape.up ℤ))))))
                  (obj DerivedCategory.Qh
                    (obj (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ))
                      (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) K))))
              (𝟙
                    (obj DerivedCategory.Qh
                      (obj (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ))
                        (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) K))) ≫
                  NatTrans.app (Iso.hom (DerivedCategory.quotientCompQhIso C₂))
                    (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) K) :
                Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
                  (obj DerivedCategory.Qh
                    (obj (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ))
                      (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) K)))
                  (obj DerivedCategory.Q (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) K))))

Tactic:
simp only [id_comp, mapDerivedCategoryFactorsh_hom_app, assoc, comp_id,
        ← Functor.map_comp_assoc, Iso.inv_hom_id_app, map_id, comp_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, CategoryTheory.Category.id_comp