-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
D₁ D₂ : ComposableArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 2
φ : D₁ ⟶ D₂
obtain :
  ∀ (w w_1 w_2 : CochainComplex.{v_1, u_1, 0} C ℤ) (f : w ⟶ w_1) (g : w_1 ⟶ w_2) (φ : ComposableArrows.mk₂ f g ⟶ D₂),
    Eq (α :=
      Functor.obj
          (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 1 2 2 SpectralObject._proof_2
              SpectralObject._proof_4 ⋙
            composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
          (ComposableArrows.mk₂ f g) ⟶
        Functor.obj
          (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 2 SpectralObject._proof_6
              SpectralObject._proof_2 ⋙
            (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)) ⋙
              shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          D₂)
      (CategoryTheory.Functor.map
          (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 1 2 2 SpectralObject._proof_2
              SpectralObject._proof_4 ⋙
            composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
          φ ≫
        Pretriangulated.Triangle.mor₃
          (Functor.obj (Functor.mapTriangle (quotient C (ComplexShape.up ℤ)))
            (CochainComplex.mappingConeCompTriangle
              (D₂.map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
              (D₂.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))))
      (Pretriangulated.Triangle.mor₃
          (Functor.obj (Functor.mapTriangle (quotient C (ComplexShape.up ℤ)))
            (CochainComplex.mappingConeCompTriangle
              ((ComposableArrows.mk₂ f g).map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
              ((ComposableArrows.mk₂ f g).map' 1 2 spectralObjectMappingCone._proof_2
                spectralObjectMappingCone._proof_3))) ≫
        CategoryTheory.Functor.map
          (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 2 SpectralObject._proof_6
              SpectralObject._proof_2 ⋙
            (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)) ⋙
              shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          φ)
⊢ Eq (α :=
    Functor.obj
        (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 1 2 2 SpectralObject._proof_2
            SpectralObject._proof_4 ⋙
          composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
        D₁ ⟶
      Functor.obj
        (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 2 SpectralObject._proof_6
            SpectralObject._proof_2 ⋙
          (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)) ⋙
            shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        D₂)
    (CategoryTheory.Functor.map
        (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 1 2 2 SpectralObject._proof_2
            SpectralObject._proof_4 ⋙
          composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
        φ ≫
      Pretriangulated.Triangle.mor₃
        (Functor.obj (Functor.mapTriangle (quotient C (ComplexShape.up ℤ)))
          (CochainComplex.mappingConeCompTriangle
            (D₂.map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            (D₂.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))))
    (Pretriangulated.Triangle.mor₃
        (Functor.obj (Functor.mapTriangle (quotient C (ComplexShape.up ℤ)))
          (CochainComplex.mappingConeCompTriangle
            (D₁.map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            (D₁.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))) ≫
      CategoryTheory.Functor.map
        (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 2 SpectralObject._proof_6
            SpectralObject._proof_2 ⋙
          (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)) ⋙
            shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        φ)

Tactic:
obtain ⟨_, _, _, f, g, rfl⟩ := ComposableArrows.mk₂_surjective D₁

Premises used: rfl, CategoryTheory.ComposableArrows.mk₂_surjective