-- 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.mappingCone f'))
    (CategoryStruct.comp (Y := CochainComplex.mappingCone g')
        (map g g' (φ.app 1) (φ.app 2) ⋯ : CochainComplex.mappingCone g ⟶ CochainComplex.mappingCone g')
        ((triangle g').mor₃ ≫
            CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (inr f') :
          CochainComplex.mappingCone g' ⟶
            Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (CochainComplex.mappingCone f')) :
      CochainComplex.mappingCone g ⟶
        Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (CochainComplex.mappingCone f'))
    (CategoryStruct.comp (Y :=
        Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (CochainComplex.mappingCone f))
        ((triangle g).mor₃ ≫
            CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (inr f) :
          CochainComplex.mappingCone g ⟶
            Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (CochainComplex.mappingCone f))
        (CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
            (map f f' (φ.app 0) (φ.app 1) ⋯) :
          Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (CochainComplex.mappingCone f) ⟶
            Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (CochainComplex.mappingCone f')) :
      CochainComplex.mappingCone g ⟶
        Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (CochainComplex.mappingCone f'))
⊢ 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) ⋯) :
          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) ⋯)) :
      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')))
have simp : 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 ℤ))
        (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          (CochainComplex.mappingCone f')))
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
        (CategoryStruct.comp (Y := CochainComplex.mappingCone g')
          (map g g' (φ.app 1) (φ.app 2) sorry : CochainComplex.mappingCone g ⟶ CochainComplex.mappingCone g')
          ((triangle g').mor₃ ≫
              CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (inr f') :
            CochainComplex.mappingCone g' ⟶
              Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
                (CochainComplex.mappingCone 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')))
  (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)))
      (CategoryStruct.comp (Y :=
        Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone f)))
        (NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1))
            (CochainComplex.mappingCone f) :
          Functor.obj
              (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1 ⋙
                quotient C (ComplexShape.up ℤ))
              (CochainComplex.mappingCone f) ⟶
            Functor.obj
              (quotient C (ComplexShape.up ℤ) ⋙
                shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 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 (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
              (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone f)) ⟶
            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')))
Tactic: simp only [Category.assoc, ← Functor.map_comp_assoc]