-- 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₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
a :
  ∀ (A' : C) (π : A' ⟶ A),
    Epi π →
      ∀ (x' : A' ⟶ (mappingCone S.f).X n₀) (w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0)
        (hx' :
          π ≫ x =
            HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫
              HomologicalComplex.homologyπ (mappingCone S.f) n₀),
        Eq (α :=
          Functor.obj (Functor.obj yoneda (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁))
            (Opposite.op A))
          (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (CategoryTheory.Functor.map yoneda
                  (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₁))
                (Opposite.op A)))
            x)
          (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (CategoryTheory.Functor.map yoneda
                  (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
                    hS.δ n₀ n₁ h ≫ 𝟙 (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁)))
                (Opposite.op A)))
            x)
⊢ Eq (α :=
    Functor.obj (Functor.obj yoneda (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁))
      (Opposite.op A))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (CategoryTheory.Functor.map yoneda
            (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₁))
          (Opposite.op A)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (CategoryTheory.Functor.map yoneda
            (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
              hS.δ n₀ n₁ h ≫ 𝟙 (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁)))
          (Opposite.op A)))
      x)

Tactic:
obtain ⟨A', π, _, x', w, hx'⟩ :=
    (mappingCone S.f).eq_liftCycles_homologyπ_up_to_refinements x n₁ (by simpa using h)

Premises used: HomologicalComplex.eq_liftCycles_homologyπ_up_to_refinements, CochainComplex.mappingCone, CategoryTheory.ShortComplex.f