-- 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
⊢ (mk
          (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₁ ⟶
              Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₂)
            n.negOnePow (Functor.map (CategoryTheory.shiftFunctor C n) X.mor₁))
          (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₂ ⟶
              Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃)
            n.negOnePow (Functor.map (CategoryTheory.shiftFunctor C n) X.mor₂))
          (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃ ⟶
              Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n ⋙ CategoryTheory.shiftFunctor C (A := ℤ) 1)
                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 n ⋙ CategoryTheory.shiftFunctor C (A := ℤ) 1)
                  X.obj₁))).mor₃ ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) (Functor.map (CategoryTheory.shiftFunctor C n) f.hom₁) =
    Functor.map (CategoryTheory.shiftFunctor C n) f.hom₃ ≫
      (mk
          (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁ ⟶
              Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₂)
            n.negOnePow (Functor.map (CategoryTheory.shiftFunctor C n) Y.mor₁))
          (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₂ ⟶
              Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₃)
            n.negOnePow (Functor.map (CategoryTheory.shiftFunctor C n) Y.mor₂))
          (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₃ ⟶
              Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n ⋙ CategoryTheory.shiftFunctor C (A := ℤ) 1)
                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 n ⋙ CategoryTheory.shiftFunctor C (A := ℤ) 1)
                  Y.obj₁))).mor₃
have dsimp : 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₁))
Tactic: dsimp