{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] →
              (le ge : ℤ → CategoryTheory.ObjectProperty C) →
                autoParam (∀ (n : ℤ), (le n).IsClosedUnderIsomorphisms)
                    CategoryTheory.Triangulated.TStructure.le_isClosedUnderIsomorphisms._autoParam →
                  autoParam (∀ (n : ℤ), (ge n).IsClosedUnderIsomorphisms)
                      CategoryTheory.Triangulated.TStructure.ge_isClosedUnderIsomorphisms._autoParam →
                    (∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), le n X → le n' ((CategoryTheory.shiftFunctor C a).obj X)) →
                      (∀ (n a n' : ℤ),
                          a + n' = n → ∀ (X : C), ge n X → ge n' ((CategoryTheory.shiftFunctor C a).obj X)) →
                        (∀ ⦃X Y : C⦄ (f : X ⟶ Y), le 0 X → ge 1 Y → f = 0) →
                          le 0 ≤ le 1 →
                            ge 1 ≤ ge 0 →
                              (∀ (A : C),
                                  ∃ X Y,
                                    ∃ (_ : le 0 X) (_ : ge 1 Y),
                                      ∃ f g h,
                                        CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
                                          CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                CategoryTheory.Triangulated.TStructure C