-- 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)
n : ℤ
X Y : Triangle.{v, u} C
f : X ⟶ Y
rw :
  HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
      n.negOnePow
      ((Functor.map (CategoryTheory.shiftFunctor C n) X.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) X.obj₁) ≫
          Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.map (CategoryTheory.shiftFunctor C n) f.hom₁) :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁)) =
    Functor.map (CategoryTheory.shiftFunctor C n) f.hom₃ ≫
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
        n.negOnePow
        (Functor.map (CategoryTheory.shiftFunctor C n) Y.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) Y.obj₁ :
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₃ ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
rw₁ :
  HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
      n.negOnePow
      ((Functor.map (CategoryTheory.shiftFunctor C n) X.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) X.obj₁) ≫
          Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.map (CategoryTheory.shiftFunctor C n) f.hom₁) :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁)) =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
      n.negOnePow
      (Functor.map (CategoryTheory.shiftFunctor C n) f.hom₃ ≫
          Functor.map (CategoryTheory.shiftFunctor C n) Y.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) Y.obj₁ :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
rw₂ :
  HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
      n.negOnePow
      ((Functor.map (CategoryTheory.shiftFunctor C n) X.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) X.obj₁) ≫
          Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.map (CategoryTheory.shiftFunctor C n) f.hom₁) :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁)) =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
      n.negOnePow
      (Functor.map (CategoryTheory.shiftFunctor C n) (f.hom₃ ≫ Y.mor₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) Y.obj₁ :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
⊢ HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₁))
        n.negOnePow
        (Functor.map (CategoryTheory.shiftFunctor C n) X.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) X.obj₁ :
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₁)) ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) (Functor.map (CategoryTheory.shiftFunctor C n) f.hom₁) =
    Functor.map (CategoryTheory.shiftFunctor C n) f.hom₃ ≫
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
        n.negOnePow
        (Functor.map (CategoryTheory.shiftFunctor C n) Y.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) Y.obj₁ :
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₃ ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
have rw₃ : HSMul.hSMul (β :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
    n.negOnePow
    ((Functor.map (CategoryTheory.shiftFunctor C n) X.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) X.obj₁) ≫
        Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) (Functor.map (CategoryTheory.shiftFunctor C n) f.hom₁) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁)) =
  HSMul.hSMul (β :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
    n.negOnePow
    (Functor.map (CategoryTheory.shiftFunctor C n)
          (X.mor₃ ≫ Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) f.hom₁) ≫
        NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) Y.obj₁ :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁))
Tactic: rw [Linear.units_smul_comp, Linear.comp_units_smul, ← Functor.map_comp_assoc, ← f.comm₃,
          Functor.map_comp, assoc, assoc, dsimp% (shiftFunctorComm C 1 n).hom.naturality]