-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject (hypothesis)
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
w w_1 w_2 : CochainComplex.{v_1, u_1, 0} C ℤ
f : w ⟶ w_1
g : w_1 ⟶ w_2
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)
        φ)
have eq : Eq (α :=
  CochainComplex.mappingCone g ⟶
    Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
      (CochainComplex.mappingConeCompTriangle f' g').obj₁)
  (map g g' (φ.app 1) (φ.app 2) sorry ≫ (CochainComplex.mappingConeCompTriangle f' g').mor₃ :
    CochainComplex.mappingCone g ⟶
      Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
        (CochainComplex.mappingConeCompTriangle f' g').obj₁)
  ((CochainComplex.mappingConeCompTriangle f g).mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
        (map f f' (φ.app 0) (φ.app 1) sorry) :
    (CochainComplex.mappingConeCompTriangle f g).obj₃ ⟶
      Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (CochainComplex.mappingCone f'))
Tactic: have eq := CochainComplex.mappingConeCompTriangle_mor₃_naturality f g f' g' φ