∀ {C : Type u_4} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{u_1, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] [inst_4 : CategoryTheory.Limits.HasZeroObject C]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_7 : CategoryTheory.Pretriangulated C] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) (F : CategoryTheory.Functor C D)
  [inst_8 : F.CommShift ℤ],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pretriangulated.Triangle.mk (F.map h.m₁) (F.map h.m₃)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃).mor₃)
              ((CategoryTheory.Functor.commShiftIso F 1).hom.app
                (CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
            ((CategoryTheory.shiftFunctor D 1).map
              (F.map (CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂).mor₂)))).mor₁
      (CategoryTheory.Iso.refl
          (CategoryTheory.Pretriangulated.Triangle.mk (F.map h.m₁) (F.map h.m₃)
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.CategoryStruct.comp
                  (F.map (CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃).mor₃)
                  ((CategoryTheory.Functor.commShiftIso F 1).hom.app
                    (CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
                ((CategoryTheory.shiftFunctor D 1).map
                  (F.map (CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂).mor₂)))).obj₂).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          (CategoryTheory.Pretriangulated.Triangle.mk (F.map h.m₁) (F.map h.m₃)
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.CategoryStruct.comp
                  (F.map (CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃).mor₃)
                  ((CategoryTheory.Functor.commShiftIso F 1).hom.app
                    (CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
                ((CategoryTheory.shiftFunctor D 1).map
                  (F.map (CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂).mor₂)))).obj₁).hom
      (F.mapTriangle.obj
          (CategoryTheory.Pretriangulated.Triangle.mk h.m₁ h.m₃
            (CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂)))).mor₁