-- 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
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)
        φ)
have 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)
        φ)
Tactic: obtain ⟨_, _, _, f', g', rfl⟩ := ComposableArrows.mk₂_surjective D₂
Cleared hypotheses: D₂, φ