-- 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
⊢ (F.map
          (HSMul.hSMul (β :=
            obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.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₁))
            n.negOnePow
            (map (shiftFunctor C n) T.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) T.obj₁ :
              obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.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₁))) ≫
        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₁) =
    NatTrans.app (Iso.hom (commShiftIso F n)) T.obj₃ ≫
      HSMul.hSMul (β :=
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj 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
        (map (shiftFunctor D n) (F.map T.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) T.obj₁) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm D 1 n)) (F.obj T.obj₁) :
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj 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₁)))
have simp : 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: simp only [map_units_smul, map_comp, Linear.units_smul_comp, assoc,
        Linear.comp_units_smul, ← F.commShiftIso_hom_naturality_assoc]