-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
rw :
  Eq (α :=
    Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f) ⟶
      Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁)
    (NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f) ≫
      Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
          (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
          n₀ n₁ h ≫
        NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₁)) S.X₁)
    (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
      hS.δ n₀ n₁ h ≫ 𝟙 (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁))
⊢ Eq (α :=
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₀) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₁) (Functor.obj (quotient C (up ℤ)) S.X₁))
    (Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
        (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
          (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
          (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
            NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
        n₀ n₁ h :
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₀)
          (Triangle.obj₃
            (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁)
              (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
              (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
              (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
                NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))) ⟶
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₁)
          (Triangle.obj₁
            (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁)
              (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
              (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
              (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
                NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))))
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f) ≫
      HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
        hS.δ n₀ n₁ h ≫ NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₁)) S.X₁)

Tactic:
rw [← cancel_mono ((homologyFunctorFactors C (up ℤ) n₁).hom.app _),
    assoc, assoc, assoc, Iso.inv_hom_id_app,
    ← cancel_epi ((homologyFunctorFactors C (up ℤ) n₀).inv.app _), Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Category.assoc, HomotopyCategory.homologyFunctorFactors, Int, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, ComplexShape.up