-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
a' b' c' : EInt
hab' : a' ≤ b'
hbc' : b' ≤ c'
φ : mk₂ (homOfLE hab) (homOfLE hbc) ⟶ mk₂ (homOfLE hab') (homOfLE hbc')
x : C
h₁ :
  ∀ (X : C),
    Eq (α :=
      (t.eTruncLT.obj ((mk₁ (homOfLE hab)).obj 1)).obj ((t.eTruncGE.obj a).obj X) ⟶
        (t.eTruncLT.obj b' ⋙ t.eTruncGE.obj a').obj X)
      (CategoryStruct.comp (Y := (t.eTruncLT.obj ((mk₁ (homOfLE hab')).obj 1)).obj ((t.eTruncGE.obj a).obj X))
        (NatTrans.app (t.eTruncLT.map (NatTrans.app (homMk₁ (φ.app 0) (φ.app 1) ⋯) 1)) ((t.eTruncGE.obj a).obj X))
        ((t.eTruncLT.obj b').map (NatTrans.app (t.eTruncGE.map (NatTrans.app (homMk₁ (φ.app 0) (φ.app 1) ⋯) 0)) X) ≫
          (t.eTruncLTGEIsoGELT a' b').hom.app X))
      ((t.eTruncLTGEIsoGELT a b).hom.app X ≫
        CategoryStruct.comp (Y := (t.eTruncGE.obj ((mk₁ (homOfLE hab')).obj 0)).obj ((t.eTruncLT.obj b).obj X))
          (NatTrans.app (t.eTruncGE.map (NatTrans.app (homMk₁ (φ.app 0) (φ.app 1) ⋯) 0)) ((t.eTruncLT.obj b).obj X) :
            (t.eTruncGE.obj ((mk₁ (homOfLE hab)).obj 0)).obj ((t.eTruncLT.obj b).obj X) ⟶
              (t.eTruncGE.obj ((mk₁ (homOfLE hab')).obj 0)).obj ((t.eTruncLT.obj b).obj X))
          ((t.eTruncGE.obj a').map (NatTrans.app (t.eTruncLT.map (NatTrans.app (homMk₁ (φ.app 0) (φ.app 1) ⋯) 1)) X) :
            (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj X) ⟶
              (t.eTruncGE.obj a').obj ((t.eTruncLT.obj ((mk₁ (homOfLE hab')).obj 1)).obj X)))
w :
  Eq (α := (t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x))
    (CategoryStruct.comp (Y := (t.eTruncLT.obj b').obj ((t.eTruncLT.obj c).obj x))
        (NatTrans.app (t.eTruncLT.map (φ.app 1)) ((t.eTruncLT.obj c).obj x) :
          (t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶ (t.eTruncLT.obj b').obj ((t.eTruncLT.obj c).obj x))
        ((t.eTruncLT.obj b').map (NatTrans.app (t.eTruncLT.map (φ.app 2)) x) ≫
            (t.eTruncLT.obj b').map ((t.eTruncGEπ a').app ((t.eTruncLT.obj c').obj x)) ≫
              (t.eTruncLT.obj b').map ((t.eTruncGE.obj a').map ((t.eTruncLTι c').app x)) ≫
                (t.eTruncLTGEIsoGELT a' b').hom.app x :
          (t.eTruncLT.obj b').obj ((t.eTruncLT.obj c).obj x) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)) :
      (t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x))
    ((t.eTruncLT.obj b).map ((t.eTruncGEπ a).app ((t.eTruncLT.obj c).obj x)) ≫
        CategoryStruct.comp (Y := (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj x)))
          (NatTrans.app (t.eTruncLT.map (φ.app 1)) ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj x)) :
            (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj x)) ⟶
              (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj x)))
          (CategoryStruct.comp (Y := (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj c).obj x)))
              ((t.eTruncLT.obj b').map (NatTrans.app (t.eTruncGE.map (φ.app 0)) ((t.eTruncLT.obj c).obj x)) :
                (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj x)) ⟶
                  (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj c).obj x)))
              ((t.eTruncLT.obj b').map
                    ((t.eTruncGE.obj a').map
                      (NatTrans.app (t.eTruncLT.map (φ.app 2)) x ≫
                        NatTrans.app (t.eTruncLTι ((mk₂ (homOfLE hab') (homOfLE hbc')).obj 2)) x)) ≫
                  (t.eTruncLTGEIsoGELT a' b').hom.app x :
                (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj c).obj x)) ⟶
                  (t.eTruncLT.obj b' ⋙ t.eTruncGE.obj a').obj x) :
            (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj x)) ⟶
              (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)) :
      (t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x))
⊢ Eq (α := (t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x))
    (CategoryStruct.comp (Y := (t.eTruncLT.obj b').obj ((t.eTruncLT.obj c).obj x))
        (NatTrans.app (t.eTruncLT.map (φ.app 1)) ((t.eTruncLT.obj c).obj x) :
          (t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶ (t.eTruncLT.obj b').obj ((t.eTruncLT.obj c).obj x))
        ((t.eTruncLT.obj b').map (NatTrans.app (t.eTruncLT.map (φ.app 2)) x) ≫
            (t.eTruncLT.obj b').map ((t.eTruncGEπ a').app ((t.eTruncLT.obj c').obj x)) ≫
              (t.eTruncLTGEIsoGELT a' b').hom.app ((t.eTruncLT.obj c').obj x) ≫
                (t.eTruncGE.obj a').map ((t.eTruncLT.obj b').map ((t.eTruncLTι c').app x)) :
          (t.eTruncLT.obj b').obj ((t.eTruncLT.obj c).obj x) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)) :
      (t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x))
    ((t.eTruncLT.obj b).map ((t.eTruncGEπ a).app ((t.eTruncLT.obj c).obj x)) ≫
        (t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj x) ≫
          CategoryStruct.comp (Y := (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x)))
            (NatTrans.app (t.eTruncGE.map (φ.app 0)) ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x)) :
              (t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x)) ⟶
                (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x)))
            ((t.eTruncGE.obj a').map (NatTrans.app (t.eTruncLT.map (φ.app 1)) ((t.eTruncLT.obj c).obj x)) ≫
                (t.eTruncGE.obj a').map ((t.eTruncLT.obj b').map ((t.eTruncLTι c).app x)) :
              (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x)) ⟶
                (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)) :
      (t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x))

Tactic:
rw [← reassoc_of% dsimp% h₁, ← eTruncLTGEIsoGELT_hom_naturality,
    ← eTruncLTGEIsoGELT_hom_naturality, ← t.eTruncLT_map_app_eTruncLTι_app (φ.app 2)]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_app, OfNat.ofNat, CategoryTheory.NatTrans.app, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality