∀ {C : Type u_2} {ι : Type u_4} {inst : CategoryTheory.Category.{u_1, u_2} C}
  {inst_1 : CategoryTheory.Category.{u_3, u_4} ι} {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}
  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (motive : X.Hom Y → Prop) (h : X.Hom Y),
  (∀ (hom : X.ω₁ ⟶ Y.ω₁)
      (comm :
        autoParam
          (∀ {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
            CategoryTheory.CategoryStruct.comp (X.δ f g)
                ((CategoryTheory.shiftFunctor C 1).map (hom.app (CategoryTheory.ComposableArrows.mk₁ f))) =
              CategoryTheory.CategoryStruct.comp (hom.app (CategoryTheory.ComposableArrows.mk₁ g)) (Y.δ f g))
          CategoryTheory.Triangulated.SpectralObject.Hom.comm._autoParam),
      motive { hom := hom, comm := comm }) →
    motive h