-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor (goal)
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 (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)
have 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))))
Tactic: dsimp