-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
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
⊢ Eq (α :=
    (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
    (CategoryStruct.comp (Y := (t.eTruncGE.obj b').obj ((t.eTruncLT.obj c).obj x))
          (NatTrans.app (t.eTruncGE.map (φ.app 1)) ((t.eTruncLT.obj c).obj x))
          ((t.eTruncGE.obj b').map (NatTrans.app (t.eTruncLT.map (φ.app 2)) x)) ≫
        (t.ω₁δ a' b' c' hab' hbc').app x :
      (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
          ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
    ((t.ω₁δ a b c hab hbc).app x ≫
        Functor.map (shiftFunctor C (A := ℤ) 1)
          (CategoryStruct.comp (Y := (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj x))
            (NatTrans.app (t.eTruncGE.map (φ.app 0)) ((t.eTruncLT.obj b).obj x))
            ((t.eTruncGE.obj a').map (NatTrans.app (t.eTruncLT.map (φ.app 1)) x))) :
      (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
          ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
have w : Eq (α :=
  (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
  ((t.eTruncGEδLT.app b).app ((t.eTruncLT.obj c).obj x) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (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.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.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
  ((t.eTruncGEδLT.app b).app ((t.eTruncLT.obj c).obj x) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        ((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.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.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
Tactic: simp only [ω₁δ_app, ← Functor.map_comp, NatTrans.naturality_assoc, Functor.comp_map,
    Category.assoc, ← Functor.map_comp_assoc, NatTrans.naturality_app_assoc,
    Functor.whiskeringRight_obj_map, Functor.whiskerRight_app, NatTrans.naturality]