-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 : EInt
hab : a ≤ b
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
rw :
  Eq (α :=
    (t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b).obj X ⟶
      (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))
    (CategoryStruct.comp (Y := (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)))
        (NatTrans.app (t.eTruncLT.map (φ.app 1)) ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) :
          (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ⟶
            (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)))
        (CategoryStruct.comp (Y := (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj X)))
            ((t.eTruncLT.obj b').map (NatTrans.app (t.eTruncGE.map (φ.app 0)) ((t.eTruncLT.obj b).obj X)) :
              (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ⟶
                (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj X)))
            ((t.eTruncLT.obj b').map
                  ((t.eTruncGE.obj a').map
                    (NatTrans.app (t.eTruncLT.map (φ.app 1)) X ≫
                      NatTrans.app (t.eTruncLTι ((mk₁ (homOfLE hab')).obj 1)) X)) ≫
                (t.eTruncLTGEIsoGELT a' b').hom.app X :
              (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj X)) ⟶
                (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X)) :
          (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ⟶
            (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X)) :
      (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ⟶
        (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))
    ((t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
        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.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ⟶
        (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))
⊢ Eq (α := (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj X) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))
    (CategoryStruct.comp (Y := (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj X))
        (NatTrans.app (t.eTruncLT.map (φ.app 1)) ((t.eTruncGE.obj a).obj X) :
          (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj X) ⟶ (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj X))
        ((t.eTruncLT.obj b').map (NatTrans.app (t.eTruncGE.map (φ.app 0)) X) ≫ (t.eTruncLTGEIsoGELT a' b').hom.app X :
          (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj X) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X)) :
      (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj X) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))
    ((t.eTruncLTGEIsoGELT a b).hom.app X ≫
        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.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj X) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))

Tactic:
rw [← cancel_epi ((t.eTruncLTGELTSelfToLTGE a b).app X), eTruncLTGELTSelfToLTGE_app,
    eTruncLTGEIsoGELT_hom_app_fac_assoc, NatTrans.naturality_assoc, ← Functor.map_comp_assoc,
    NatTrans.naturality, Functor.map_comp_assoc, ← t.eTruncLT_map_app_eTruncLTι_app (φ.app 1) X]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_app, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE_app, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac_assoc, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.NatTrans.naturality, OfNat.ofNat, CategoryTheory.cancel_epi, CategoryTheory.NatTrans.app, CategoryTheory.NatTrans.naturality_assoc