-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
n : ℤ
T : Triangle.{v_1, u_1} C
rw :
  HSMul.hSMul (β :=
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₃) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₁)))
      n.negOnePow
      (F.map (map (shiftFunctor C n) T.mor₃) ≫
        CategoryStruct.comp (Y :=
          F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁)))
          (CategoryStruct.comp (Y :=
            (F ⋙ shiftFunctor D n).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
            (NatTrans.app (Iso.hom (commShiftIso F n)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
            (map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso F 1)) T.obj₁) ≫
              NatTrans.app (Iso.hom (shiftFunctorComm D 1 n)) (F.obj T.obj₁) ≫
                map (shiftFunctor D (A := ℤ) 1) (NatTrans.app (Iso.inv (commShiftIso F n)) T.obj₁) ≫
                  NatTrans.app (Iso.inv (commShiftIso F 1)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁)))
          (NatTrans.app (Iso.hom (commShiftIso F 1)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁) ≫
            map (shiftFunctor D (A := ℤ) 1) (NatTrans.app (Iso.hom (commShiftIso F n)) T.obj₁))) =
    HSMul.hSMul (β :=
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₃) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₁)))
      n.negOnePow
      (F.map (map (shiftFunctor C n) T.mor₃) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
            (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁)))
          (NatTrans.app (Iso.hom (commShiftIso F n)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
          (map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso F 1)) T.obj₁) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm D 1 n)) (F.obj T.obj₁)))
⊢ HSMul.hSMul (β :=
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₃) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₁)))
      n.negOnePow
      (F.map (map (shiftFunctor C n) T.mor₃) ≫
          F.map (NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) T.obj₁) ≫
            NatTrans.app (Iso.hom (commShiftIso F 1)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁) ≫
              map (shiftFunctor D (A := ℤ) 1) (NatTrans.app (Iso.hom (commShiftIso F n)) T.obj₁) :
        F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₃) ⟶
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₁))) =
    HSMul.hSMul (β :=
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₃) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₁)))
      n.negOnePow
      (F.map (map (shiftFunctor C n) T.mor₃) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
            (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁)))
          (NatTrans.app (Iso.hom (commShiftIso F n)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
          (map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso F 1)) T.obj₁) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm D 1 n)) (F.obj T.obj₁)))

Tactic:
rw [F.map_shiftFunctorComm_hom_app T.obj₁ 1 n]

Premises used: CategoryTheory.Functor.map_shiftFunctorComm_hom_app, CategoryTheory.Pretriangulated.Triangle.obj₁, OfNat.ofNat