-- 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
obtain :
  ∀ (w w_1 w_2 : CochainComplex.{v_1, u_1, 0} C ℤ) (f : w ⟶ w_1) (g : w_1 ⟶ w_2),
    Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _)
      (Pretriangulated.Triangle.mk (X :=
        Functor.obj (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
          (Functor.obj (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 2 ⋯ ⋯)
            (ComposableArrows.mk₂ f g)))
        (CategoryTheory.Functor.map (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
          (NatTrans.app
            (ComposableArrows.mapFunctorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 0 2 2 SpectralObject._proof_6
              SpectralObject._proof_8 SpectralObject._proof_10 SpectralObject._proof_2 SpectralObject._proof_4)
            (ComposableArrows.mk₂ f g)))
        (CategoryTheory.Functor.map (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
          (NatTrans.app
            (ComposableArrows.mapFunctorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 2 1 2 2 SpectralObject._proof_8
              SpectralObject._proof_2 SpectralObject._proof_6 SpectralObject._proof_4 SpectralObject._proof_4)
            (ComposableArrows.mk₂ f g)))
        (NatTrans.app
          {
            app := fun (D : ComposableArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 2) ↦
              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))),
            naturality := ⋯ }
          (ComposableArrows.mk₂ f g)))
⊢ Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _)
    (Pretriangulated.Triangle.mk (X :=
      Functor.obj (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
        (Functor.obj (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 2 ⋯ ⋯) D))
      (CategoryTheory.Functor.map (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
        (NatTrans.app
          (ComposableArrows.mapFunctorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 0 2 2 SpectralObject._proof_6
            SpectralObject._proof_8 SpectralObject._proof_10 SpectralObject._proof_2 SpectralObject._proof_4)
          D))
      (CategoryTheory.Functor.map (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
        (NatTrans.app
          (ComposableArrows.mapFunctorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 2 1 2 2 SpectralObject._proof_8
            SpectralObject._proof_2 SpectralObject._proof_6 SpectralObject._proof_4 SpectralObject._proof_4)
          D))
      (NatTrans.app
        {
          app := fun (D : ComposableArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 2) ↦
            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))),
          naturality := ⋯ }
        D))

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

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