-- 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₂ : ComposableArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 2
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₂
obtain :
  ∀ (w_3 w_4 w_5 : CochainComplex.{v_1, u_1, 0} C ℤ) (f' : w_3 ⟶ w_4) (g' : w_4 ⟶ w_5)
    (φ : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g'),
    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)
          (ComposableArrows.mk₂ f' g'))
      (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
              ((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))))
      (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 ℤ))
        (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)
        φ)

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

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