-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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₃))
⊢ T₁.mor₂ ≫ c = a ≫ T₂.mor₂
have 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₃)))
Tactic: rw [← cancel_mono ((shiftEquiv C (1 : ℤ)).counitIso.inv.app T₂.obj₃), assoc, assoc, ← ha₂]