∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ u₁₂_1 : X₁ ⟶ X₂} (e_u₁₂ : u₁₂ = u₁₂_1) {u₂₃ u₂₃_1 : X₂ ⟶ X₃} (e_u₂₃ : u₂₃ = u₂₃_1)
  {u₁₃ u₁₃_1 : X₁ ⟶ X₃} (e_u₁₃ : u₁₃ = u₁₃_1) (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃)
  {v₁₂ v₁₂_1 : X₂ ⟶ Z₁₂} (e_v₁₂ : v₁₂ = v₁₂_1) {w₁₂ w₁₂_1 : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (e_w₁₂ : w₁₂ = w₁₂_1)
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ v₂₃_1 : X₃ ⟶ Z₂₃} (e_v₂₃ : v₂₃ = v₂₃_1) {w₂₃ w₂₃_1 : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  (e_w₂₃ : w₂₃ = w₂₃_1)
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ v₁₃_1 : X₃ ⟶ Z₁₃} (e_v₁₃ : v₁₃ = v₁₃_1) {w₁₃ w₁₃_1 : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (e_w₁₃ : w₁₃ = w₁₃_1)
  (h₁₃ :
    CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃ = CategoryTheory.Triangulated.Octahedron ⋯ ⋯ ⋯ ⋯