-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
      (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)))
    ((CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) (triangle φ).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso (G.mapHomologicalComplex (ComplexShape.up ℤ)) 1)) K) ≫
        CategoryTheory.Functor.map
          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
          (𝟙 (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
          (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)))
    (CategoryStruct.comp (Y :=
        mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        (Iso.hom (mapHomologicalComplexIso φ G) :
          Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
            (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
            (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
              (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
        (Triangle.mor₃
            (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
              (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) :
          Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
            (Triangle.obj₃
              (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
                (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
            (Functor.obj
              (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
              (Triangle.obj₁
                (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
                  (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))))) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
          (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)))

Tactic:
simp only [CategoryTheory.Functor.map_id, comp_id, map_δ]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CochainComplex.mappingCone.map_δ