-- 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
⊢ 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) ⋯)) T.obj₁) =
    NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) 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₁)))
have rw : 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 b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) 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.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (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 (a + b)) 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 * a.negOnePow)
    (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₃ ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁) ≫
        Functor.map (CategoryTheory.shiftFunctor C b) (NatTrans.app (Iso.hom (shiftFunctorComm C 1 a)) T.obj₁) ≫
          NatTrans.app (Iso.hom (shiftFunctorComm C 1 b))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁))
Tactic: rw [Linear.units_smul_comp, Linear.comp_units_smul, Functor.map_units_smul,
          Linear.units_smul_comp, Linear.comp_units_smul, smul_smul, assoc, Functor.map_comp, assoc,
          ← dsimp% (CategoryTheory.shiftFunctorAdd' C a b (a + b) rfl).hom.naturality_assoc]