-- 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
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 :
  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) ⋯ ≫ (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) ⋯) :
      (CochainComplex.mappingConeCompTriangle f g).obj₃ ⟶
        Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (CochainComplex.mappingCone f'))
⊢ 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 dsimp : Eq (α :=
  Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone g) ⟶
    Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone f')))
  (CategoryStruct.comp (Y := Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone g'))
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (map g g' (φ.app 1) (φ.app 2) sorry) :
        Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone g) ⟶
          Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone g'))
      (CategoryStruct.comp (Y :=
          Functor.obj (quotient C (ComplexShape.up ℤ))
            (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
              (CochainComplex.mappingCone f')))
          (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
            ((triangle g').mor₃ ≫
              CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (inr f')))
          (NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1))
            (CochainComplex.mappingCone f')) :
        Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone g') ⟶
          Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone f'))) :
    Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone g) ⟶
      Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone f')))
  (CategoryStruct.comp (Y :=
        Functor.obj (quotient C (ComplexShape.up ℤ))
          (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            (CochainComplex.mappingCone f)))
        (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
          ((triangle g).mor₃ ≫
            CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (inr f)))
        (NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1))
          (CochainComplex.mappingCone f)) ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (map f f' (φ.app 0) (φ.app 1) sorry)) :
    Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone g) ⟶
      Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone f')))
Tactic: dsimp [ComposableArrows.Precomp.map] at eq ⊢