-- 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₁ ℤ
w :
  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))))
⊢ Eq.{w₂ + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
      (obj (comp (D := DerivedCategory.{w₁, v₁, u₁} C₁) DerivedCategory.Q F.mapDerivedCategory) K)
      (obj (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q) K))
    (NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) K)
    (NatTrans.app
      (whiskerRight (Iso.inv (DerivedCategory.quotientCompQhIso C₁)) F.mapDerivedCategory ≫
        Iso.hom
            (associator (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) DerivedCategory.Qh F.mapDerivedCategory) ≫
          whiskerLeft (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) (Iso.hom F.mapDerivedCategoryFactorsh) ≫
            Iso.inv
                (associator (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ))
                  (F.mapHomotopyCategory (ComplexShape.up ℤ)) DerivedCategory.Qh) ≫
              whiskerRight (Iso.hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ))) DerivedCategory.Qh ≫
                Iso.hom
                    (associator (F.mapHomologicalComplex (ComplexShape.up ℤ))
                      (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ)) DerivedCategory.Qh) ≫
                  whiskerLeft (F.mapHomologicalComplex (ComplexShape.up ℤ))
                    (Iso.hom (DerivedCategory.quotientCompQhIso C₂)))
      K)

Tactic:
dsimp