∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} 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.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C} {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃}
  {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)},
  CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    ∀ {Q : A} (β : X₃ ⟶ ι.obj Q) [inst_7 : ι.Full] [inst_8 : CategoryTheory.Preadditive A] [ι.Faithful] {Z : A}
      (h : Q ⟶ Z),
      CategoryTheory.CategoryStruct.comp f₁
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂ β) h) =
        CategoryTheory.CategoryStruct.comp 0 h