∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂)
  (h :
    ∃ c,
      CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
        CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) =
          CategoryTheory.CategoryStruct.comp c T₂.mor₃),
  CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) =
    CategoryTheory.CategoryStruct.comp h.choose T₂.mor₃