-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.mk.inj : ∀ {C : Type u_1} {ι : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} ι} {inst_2 : CategoryTheory.Limits.HasZeroObject C}
  {inst_3 : CategoryTheory.HasShift C ℤ} {inst_4 : CategoryTheory.Preadditive C}
  {inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_6 : CategoryTheory.Pretriangulated C}
  {ω₁ : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C}
  {δ' :
    (CategoryTheory.ComposableArrows.functorArrows ι 1 2 2 CategoryTheory.Triangulated.SpectralObject._proof_2
            CategoryTheory.Triangulated.SpectralObject._proof_4).comp
        ω₁ ⟶
      (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Triangulated.SpectralObject._proof_6
            CategoryTheory.Triangulated.SpectralObject._proof_2).comp
        (ω₁.comp (CategoryTheory.shiftFunctor C 1))}
  {distinguished' :
    ∀ (D : CategoryTheory.ComposableArrows ι 2),
      CategoryTheory.Pretriangulated.Triangle.mk
          (ω₁.map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                  CategoryTheory.Triangulated.SpectralObject._proof_6
                  CategoryTheory.Triangulated.SpectralObject._proof_8
                  CategoryTheory.Triangulated.SpectralObject._proof_10
                  CategoryTheory.Triangulated.SpectralObject._proof_2
                  CategoryTheory.Triangulated.SpectralObject._proof_4).app
              D))
          (ω₁.map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                  CategoryTheory.Triangulated.SpectralObject._proof_8
                  CategoryTheory.Triangulated.SpectralObject._proof_2
                  CategoryTheory.Triangulated.SpectralObject._proof_6
                  CategoryTheory.Triangulated.SpectralObject._proof_4
                  CategoryTheory.Triangulated.SpectralObject._proof_4).app
              D))
          (δ'.app D) ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles}
  {ω₁_1 : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C}
  {δ'_1 :
    (CategoryTheory.ComposableArrows.functorArrows ι 1 2 2 CategoryTheory.Triangulated.SpectralObject._proof_2
            CategoryTheory.Triangulated.SpectralObject._proof_4).comp
        ω₁_1 ⟶
      (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Triangulated.SpectralObject._proof_6
            CategoryTheory.Triangulated.SpectralObject._proof_2).comp
        (ω₁_1.comp (CategoryTheory.shiftFunctor C 1))}
  {distinguished'_1 :
    ∀ (D : CategoryTheory.ComposableArrows ι 2),
      CategoryTheory.Pretriangulated.Triangle.mk
          (ω₁_1.map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                  CategoryTheory.Triangulated.SpectralObject._proof_6
                  CategoryTheory.Triangulated.SpectralObject._proof_8
                  CategoryTheory.Triangulated.SpectralObject._proof_10
                  CategoryTheory.Triangulated.SpectralObject._proof_2
                  CategoryTheory.Triangulated.SpectralObject._proof_4).app
              D))
          (ω₁_1.map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                  CategoryTheory.Triangulated.SpectralObject._proof_8
                  CategoryTheory.Triangulated.SpectralObject._proof_2
                  CategoryTheory.Triangulated.SpectralObject._proof_6
                  CategoryTheory.Triangulated.SpectralObject._proof_4
                  CategoryTheory.Triangulated.SpectralObject._proof_4).app
              D))
          (δ'_1.app D) ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles},
  { ω₁ := ω₁, δ' := δ', distinguished' := distinguished' } =
      { ω₁ := ω₁_1, δ' := δ'_1, distinguished' := distinguished'_1 } →
    ω₁ = ω₁_1 ∧ δ' ≍ δ'_1