-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
a_1 : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a_1 = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a_1 ≫ T₂.invRotate.mor₂
ha₂ :
  Eq (α :=
    T₁.obj₂ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₂.obj₃))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃))
        (T₁.mor₂ ≫ NatTrans.app (Iso.inv (Equivalence.counitIso (shiftEquiv C (A := ℤ) 1))) T₁.3 :
          T₁.obj₂ ⟶
            Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃))
        (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) c) :
          Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃) ⟶
            Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₂.obj₃)) :
      T₁.obj₂ ⟶
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₂.obj₃))
    (a ≫ T₂.mor₂ ≫ NatTrans.app (Iso.inv (Equivalence.counitIso (shiftEquiv C (A := ℤ) 1))) T₂.3 :
      T₁.obj₂ ⟶
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₂.obj₃))
rw :
  Eq (α :=
    T₁.obj₂ ⟶
      Functor.obj.{v, v, u, u}
        (Equivalence.inverse (shiftEquiv C (A := ℤ) 1) ⋙ Equivalence.functor (shiftEquiv C (A := ℤ) 1)) T₂.obj₃)
    (T₁.mor₂ ≫ c ≫ NatTrans.app (Iso.inv (Equivalence.counitIso (shiftEquiv C (A := ℤ) 1))) T₂.obj₃)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃))
      (T₁.mor₂ ≫ NatTrans.app (Iso.inv (Equivalence.counitIso (shiftEquiv C (A := ℤ) 1))) T₁.3 :
        T₁.obj₂ ⟶
          Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) c) :
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃) ⟶
          Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₂.obj₃)))
⊢ T₁.mor₂ ≫ c = a ≫ T₂.mor₂

Tactic:
rw [← cancel_mono ((shiftEquiv C (1 : ℤ)).counitIso.inv.app T₂.obj₃), assoc, assoc, ← ha₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Pretriangulated.Triangle.obj₃, CategoryTheory.cancel_mono, CategoryTheory.shiftEquiv, OfNat.ofNat, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, CategoryTheory.Equivalence.counitIso