-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
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'))
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) ⋯ : 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) ⋯)) :
            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')))
⊢ 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')))

Tactic:
simp only [Category.assoc, ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp_assoc