∀ {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)
  (le_isClosedUnderIsomorphisms :
    autoParam (∀ (n : ℤ), (le n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.le_isClosedUnderIsomorphisms._autoParam)
  (ge_isClosedUnderIsomorphisms :
    autoParam (∀ (n : ℤ), (ge n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.ge_isClosedUnderIsomorphisms._autoParam)
  (le_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), le n X → le n' ((CategoryTheory.shiftFunctor C a).obj X))
  (ge_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), ge n X → ge n' ((CategoryTheory.shiftFunctor C a).obj X))
  (zero' : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), le 0 X → ge 1 Y → f = 0) (le_zero_le : le 0 ≤ le 1) (ge_one_le : ge 1 ≤ ge 0)
  (exists_triangle_zero_one :
    ∀ (A : C),
      ∃ X Y,
        ∃ (_ : le 0 X) (_ : ge 1 Y),
          ∃ f g h,
            CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (le_1 ge_1 : ℤ → CategoryTheory.ObjectProperty C)
  (le_isClosedUnderIsomorphisms_1 :
    autoParam (∀ (n : ℤ), (le_1 n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.le_isClosedUnderIsomorphisms._autoParam)
  (ge_isClosedUnderIsomorphisms_1 :
    autoParam (∀ (n : ℤ), (ge_1 n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.ge_isClosedUnderIsomorphisms._autoParam)
  (le_shift_1 : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), le_1 n X → le_1 n' ((CategoryTheory.shiftFunctor C a).obj X))
  (ge_shift_1 : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), ge_1 n X → ge_1 n' ((CategoryTheory.shiftFunctor C a).obj X))
  (zero'_1 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), le_1 0 X → ge_1 1 Y → f = 0) (le_zero_le_1 : le_1 0 ≤ le_1 1)
  (ge_one_le_1 : ge_1 1 ≤ ge_1 0)
  (exists_triangle_zero_one_1 :
    ∀ (A : C),
      ∃ X Y,
        ∃ (_ : le_1 0 X) (_ : ge_1 1 Y),
          ∃ f g h,
            CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  ({ le := le, ge := ge, le_isClosedUnderIsomorphisms := le_isClosedUnderIsomorphisms,
        ge_isClosedUnderIsomorphisms := ge_isClosedUnderIsomorphisms, le_shift := le_shift, ge_shift := ge_shift,
        zero' := zero', le_zero_le := le_zero_le, ge_one_le := ge_one_le,
        exists_triangle_zero_one := exists_triangle_zero_one } =
      { le := le_1, ge := ge_1, le_isClosedUnderIsomorphisms := le_isClosedUnderIsomorphisms_1,
        ge_isClosedUnderIsomorphisms := ge_isClosedUnderIsomorphisms_1, le_shift := le_shift_1, ge_shift := ge_shift_1,
        zero' := zero'_1, le_zero_le := le_zero_le_1, ge_one_le := ge_one_le_1,
        exists_triangle_zero_one := exists_triangle_zero_one_1 }) =
    (le = le_1 ∧ ge = ge_1)