-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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 : EInt
hab : a ≤ b
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
⊢ 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))
have 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))
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]