-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
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
⊢ 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₁)))
have 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₁)))
Tactic: rw [F.map_shiftFunctorComm_hom_app T.obj₁ 1 n]