∀ {C : Type u_4} {A : Type u_2} [inst : CategoryTheory.Category.{u_3, u_4} 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_1, u_2} A]
  {ι : CategoryTheory.Functor A C}
  (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) {X₁ X₂ : A}
  {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {K Q : A} {α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q}
  {γ : ι.obj Q ⟶ (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj (ι.obj K))}
  (hT' : CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  [inst_7 : ι.Full] [inst_8 : CategoryTheory.Preadditive A] [inst_9 : ι.Faithful] {W' : A} (x₁ : W' ⟶ X₁)
  (hx₁ : CategoryTheory.CategoryStruct.comp x₁ f₁ = 0) (m : W' ⟶ K),
  CategoryTheory.CategoryStruct.comp m (CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃ α) = x₁ → m = ⋯.choose