-- 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
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n : ℤ
rw :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫
      CategoryStruct.comp (Y := homology T.obj₂ n) (homologyMap T.mor₁ n) (homologyMap T.mor₂ n))
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
rw₁ :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
        (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
      NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₂ ≫ homologyMap T.mor₂ n)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
rw₂ :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
        (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
      CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
          (CategoryTheory.Functor.map DerivedCategory.Q T.mor₂) ≫
        NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₃)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
rw₃ :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
        (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁ ≫ CategoryTheory.Functor.map DerivedCategory.Q T.mor₂) ≫
      NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₃)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
rw₄ :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n) 0 ≫
      NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₃)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
rw₅ :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n)
        (Functor.obj DerivedCategory.Q T.obj₃))
      0 (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₃))
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
rw₆ :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    0 (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
rw₇ rw₈ :
  Eq.{v + 1} (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    0 0
⊢ Eq (α := homology T.obj₁ n ⟶ homology T.obj₃ n)
    (CategoryStruct.comp (Y := homology T.obj₂ n) (homologyMap T.mor₁ n) (homologyMap T.mor₂ n)) 0

Tactic:
rw [← cancel_epi ((DerivedCategory.homologyFunctorFactors _ _).hom.app _),
    ← DerivedCategory.homologyFunctorFactors_hom_naturality_assoc,
    ← DerivedCategory.homologyFunctorFactors_hom_naturality,
    ← Functor.map_comp_assoc, dsimp% comp_distTriang_mor_zero₁₂ _ hT, Functor.map_zero,
    Limits.zero_comp, Limits.comp_zero]

Premises used: CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, DerivedCategory.homologyFunctorFactors_hom_naturality, CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp_assoc, DerivedCategory.homologyFunctorFactors, CategoryTheory.Limits.zero_comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, DerivedCategory.homologyFunctorFactors_hom_naturality_assoc