-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- When two diagrams are isomorphic, an octahedron for one gives an octahedron for the other.  -/
CategoryTheory.Triangulated.Octahedron.ofIso : {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₁₂ : 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) →
                                          {X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C} →
                                            (u₁₂' : X₁' ⟶ X₂') →
                                              (u₂₃' : X₂' ⟶ X₃') →
                                                (u₁₃' : X₁' ⟶ X₃') →
                                                  (comm' : CategoryTheory.CategoryStruct.comp u₁₂' u₂₃' = u₁₃') →
                                                    (e₁ : X₁ ≅ X₁') →
                                                      (e₂ : X₂ ≅ X₂') →
                                                        (e₃ : X₃ ≅ X₃') →
                                                          CategoryTheory.CategoryStruct.comp u₁₂ e₂.hom =
                                                              CategoryTheory.CategoryStruct.comp e₁.hom u₁₂' →
                                                            CategoryTheory.CategoryStruct.comp u₂₃ e₃.hom =
                                                                CategoryTheory.CategoryStruct.comp e₂.hom 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) →
                                                                                CategoryTheory.Triangulated.Octahedron
                                                                                    comm' h₁₂' h₂₃' h₁₃' →
                                                                                  CategoryTheory.Triangulated.Octahedron
                                                                                    comm h₁₂ h₂₃ h₁₃