-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject (goal)
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
⊢ 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))
have 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 _ _ sorry _ (instPreadditive C (ComplexShape.up ℤ)) sorry _)
    (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 sorry sorry)
          (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 := sorry }
        (ComposableArrows.mk₂ f g)))
Tactic: obtain ⟨_, _, _, f, g, rfl⟩ := ComposableArrows.mk₂_surjective D
Cleared hypotheses: D