-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f : K ⟶ Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L
a a' : ℤ
h : n + a = a'
rw :
  Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a) (Functor.obj Q K) ⟶
      Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a') (Functor.obj Q L))
    (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C 0) a)
        (NatTrans.app (Iso.inv (quotientCompQhIso C)) K) ≫
      ((CategoryTheory.Functor.map (homologyFunctor C a) (NatTrans.app (Iso.hom (quotientCompQhIso C)) K) ≫
            NatTrans.app (Iso.hom (homologyFunctorFactors C a)) K ≫
              NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a)) K) ≫
          (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a)) K ≫
              Functor.shiftMap (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0) f a a' ⋯ ≫
                NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a')) L) ≫
            NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a')) L ≫
              NatTrans.app (Iso.inv (homologyFunctorFactors C a')) L ≫
                CategoryTheory.Functor.map (homologyFunctor C a') (NatTrans.app (Iso.inv (quotientCompQhIso C)) L)) ≫
        CategoryTheory.Functor.map (Functor.shift (homologyFunctor C 0) a')
          (NatTrans.app (Iso.hom (quotientCompQhIso C)) L))
    (NatTrans.app (Iso.hom (homologyFunctorFactors C a)) K ≫
      Functor.shiftMap (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0) f a a' h ≫
        NatTrans.app (Iso.inv (homologyFunctorFactors C a')) L)
⊢ Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a) (Functor.obj Q K) ⟶
      Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a') (Functor.obj Q L))
    (Functor.shiftMap (homologyFunctor C 0) (ShiftedHom.map f Q) a a' h)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C a)) K ≫
      Functor.shiftMap (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0) f a a' h ≫
        NatTrans.app (Iso.inv (homologyFunctorFactors C a')) L)

Tactic:
rw [← ShiftedHom.map_naturality_1 f (quotientCompQhIso C),
    ShiftedHom.mk₀_comp, ShiftedHom.comp_mk₀,
    Functor.shiftMap_comp', Functor.shiftMap_comp,
    ShiftedHom.comp_map, shiftMap_homologyFunctor_map_Qh ..,
    homologyFunctorFactorsh_hom_app_quotient_obj,
    homologyFunctorFactorsh_inv_app_quotient_obj,
    HomotopyCategory.homologyFunctor_shiftMap]

Premises used: CategoryTheory.Functor.shiftMap_comp', CategoryTheory.ShiftedHom.comp_mk₀, CategoryTheory.ShiftedHom.mk₀_comp, CategoryTheory.Functor.shiftMap_comp, CategoryTheory.ShiftedHom.comp_map, CategoryTheory.ShiftedHom.map_naturality_1, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj, DerivedCategory.quotientCompQhIso, DerivedCategory.shiftMap_homologyFunctor_map_Qh, HomotopyCategory.homologyFunctor_shiftMap, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj