-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
T : Triangle.{v, u} C
⊢ (Functor.obj (shiftFunctor C (a + b)) T).mor₃ ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₁)) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₃) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₃
have dsimp : HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₁))
      (a + b).negOnePow
      (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorComm C 1 (a + b))) T.obj₁ :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₁)) ≫
    Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₁) =
  NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₃ ≫
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃) ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
      b.negOnePow
      (Functor.map (CategoryTheory.shiftFunctor C b)
            (HSMul.hSMul (β :=
              Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃ ⟶
                Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
                  (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁))
              a.negOnePow
              (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₃ ≫
                  NatTrans.app (Iso.hom (shiftFunctorComm C 1 a)) T.obj₁ :
                Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃ ⟶
                  Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
                    (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁))) ≫
          NatTrans.app (Iso.hom (shiftFunctorComm C 1 b))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁) :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃) ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
Tactic: dsimp