-- 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
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 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 (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 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) T.obj₃)
            a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂)))
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 b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
      (a + b).negOnePow
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
        Functor.map (CategoryTheory.shiftFunctor C a ⋙ CategoryTheory.shiftFunctor C b) T.mor₂) =
    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 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) T.obj₃)
            a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂)))
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 b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
      (a + b).negOnePow
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
        Functor.map (CategoryTheory.shiftFunctor C a ⋙ CategoryTheory.shiftFunctor C b) T.mor₂) =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
      b.negOnePow
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
          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) T.obj₃)
              a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂)) :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
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 b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
      (a + b).negOnePow
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
          Functor.map (CategoryTheory.shiftFunctor C b) (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂) :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a ⋙ CategoryTheory.shiftFunctor C b) 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 b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
      b.negOnePow
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
          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) T.obj₃)
              a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂)) :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
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 b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
      (a + b).negOnePow
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
          Functor.map (CategoryTheory.shiftFunctor C b) (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂) :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a ⋙ CategoryTheory.shiftFunctor C b) T.obj₃) =
    b.negOnePow •
      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 b)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
          a.negOnePow
          (Functor.map (CategoryTheory.shiftFunctor C b) (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂))
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 b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
      (a + b).negOnePow
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
          Functor.map (CategoryTheory.shiftFunctor C b) (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂) :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a ⋙ CategoryTheory.shiftFunctor C b) T.obj₃) =
    b.negOnePow •
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
        a.negOnePow
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
            Functor.map (CategoryTheory.shiftFunctor C b) (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂) :
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
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 b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
      (a + b).negOnePow
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
          Functor.map (CategoryTheory.shiftFunctor C b) (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂) :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a ⋙ CategoryTheory.shiftFunctor C b) 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 b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
      (b.negOnePow * a.negOnePow)
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
          Functor.map (CategoryTheory.shiftFunctor C b) (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂) :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) 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 + b)) T.obj₃)
        (a + b).negOnePow (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₂) ≫
      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 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) T.obj₃)
            a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂)))
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 b)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
    (a.negOnePow * b.negOnePow)
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₂ ≫
        Functor.map (CategoryTheory.shiftFunctor C b) (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a ⋙ CategoryTheory.shiftFunctor C b) 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 b)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
    (b.negOnePow * a.negOnePow)
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₂ ≫
        Functor.map (CategoryTheory.shiftFunctor C b) (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
Tactic: rw [Linear.units_smul_comp, NatTrans.naturality, Linear.comp_units_smul, Functor.comp_map,
          Functor.map_units_smul, Linear.comp_units_smul, smul_smul, Int.negOnePow_add, mul_comm]