∀ {C : Type u_2} {A : Type u_4} [inst : CategoryTheory.Category.{u_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{u_3, u_4} A]
  {ι : CategoryTheory.Functor A C} [inst_7 : CategoryTheory.Preadditive A] [inst_8 : ι.Full] [inst_9 : ι.Faithful]
  [inst_10 : ι.Additive] {X₁ X₂ X₃ : A} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃)
  (f₃ : ι.obj X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁))
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles),
  ι.map
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Cofork.π
          (CategoryTheory.Limits.CokernelCofork.ofπ
            (CategoryTheory.Triangulated.AbelianSubcategory.πQ (ι.map f₂) (CategoryTheory.CategoryStruct.id (ι.obj X₃)))
            ⋯))
        (CategoryTheory.Iso.refl
            (CategoryTheory.Limits.CokernelCofork.ofπ
                (CategoryTheory.Triangulated.AbelianSubcategory.πQ (ι.map f₂)
                  (CategoryTheory.CategoryStruct.id (ι.obj X₃)))
                ⋯).pt).hom) =
    ι.map (CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.CokernelCofork.ofπ f₂ ⋯))