-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
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)
⊢ 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
have 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)
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]