-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.mk : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (H : ℤ → CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C) →
            (δ' :
                (n₀ n₁ : ℤ) →
                  n₀ + 1 = n₁ →
                    ((CategoryTheory.ComposableArrows.functorArrows ι 1 2 2
                            CategoryTheory.Abelian.SpectralObject._proof_2
                            CategoryTheory.Abelian.SpectralObject._proof_4).comp
                        (H n₀) ⟶
                      (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2
                            CategoryTheory.Abelian.SpectralObject._proof_6
                            CategoryTheory.Abelian.SpectralObject._proof_2).comp
                        (H n₁))) →
              (∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : CategoryTheory.ComposableArrows ι 2),
                  (CategoryTheory.ComposableArrows.mk₂ ((δ' n₀ n₁ h).app D)
                      ((H n₁).map
                        ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                              CategoryTheory.Abelian.SpectralObject._proof_6
                              CategoryTheory.Abelian.SpectralObject._proof_8
                              CategoryTheory.Abelian.SpectralObject._proof_10
                              CategoryTheory.Abelian.SpectralObject._proof_2
                              CategoryTheory.Abelian.SpectralObject._proof_4).app
                          D))).Exact) →
                (∀ (n : ℤ) (D : CategoryTheory.ComposableArrows ι 2),
                    (CategoryTheory.ComposableArrows.mk₂
                        ((H n).map
                          ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                                CategoryTheory.Abelian.SpectralObject._proof_6
                                CategoryTheory.Abelian.SpectralObject._proof_8
                                CategoryTheory.Abelian.SpectralObject._proof_10
                                CategoryTheory.Abelian.SpectralObject._proof_2
                                CategoryTheory.Abelian.SpectralObject._proof_4).app
                            D))
                        ((H n).map
                          ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                                CategoryTheory.Abelian.SpectralObject._proof_8
                                CategoryTheory.Abelian.SpectralObject._proof_2
                                CategoryTheory.Abelian.SpectralObject._proof_6
                                CategoryTheory.Abelian.SpectralObject._proof_4
                                CategoryTheory.Abelian.SpectralObject._proof_4).app
                            D))).Exact) →
                  (∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : CategoryTheory.ComposableArrows ι 2),
                      (CategoryTheory.ComposableArrows.mk₂
                          ((H n₀).map
                            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                                  CategoryTheory.Abelian.SpectralObject._proof_8
                                  CategoryTheory.Abelian.SpectralObject._proof_2
                                  CategoryTheory.Abelian.SpectralObject._proof_6
                                  CategoryTheory.Abelian.SpectralObject._proof_4
                                  CategoryTheory.Abelian.SpectralObject._proof_4).app
                              D))
                          ((δ' n₀ n₁ h).app D)).Exact) →
                    CategoryTheory.Abelian.SpectralObject C ι