-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.mk.injEq : ∀ {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)