-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.mk : {ι : Type u_2} →
  {κ : Type u_3} →
    [inst : Preorder ι] →
      {c : ℤ → ComplexShape κ} →
        {r₀ : ℤ} →
          (deg : κ → ℤ) →
            (i₀ :
                (r : ℤ) →
                  κ → autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_1 → ι) →
              (i₁ i₂ : κ → ι) →
                (i₃ :
                    (r : ℤ) →
                      κ →
                        autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_3 → ι) →
                  (∀ (r : ℤ) (pq : κ)
                      (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_5),
                      i₀ r pq ⋯ ≤ i₁ pq) →
                    (∀ (pq : κ), i₁ pq ≤ i₂ pq) →
                      (∀ (r : ℤ) (pq : κ)
                          (hr :
                            autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_9),
                          i₂ pq ≤ i₃ r pq ⋯) →
                        (∀ (r : ℤ) (pq pq' : κ),
                            (c r).Rel pq pq' →
                              autoParam (r₀ ≤ r)
                                  CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_14 →
                                deg pq + 1 = deg pq') →
                          (∀ (r : ℤ) (pq pq' : κ),
                              (c r).Rel pq pq' →
                                ∀
                                  (hr :
                                    autoParam (r₀ ≤ r)
                                      CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_16),
                                  i₀ r pq ⋯ = i₂ pq') →
                            (∀ (r : ℤ) (pq pq' : κ),
                                (c r).Rel pq pq' →
                                  ∀
                                    (hr :
                                      autoParam (r₀ ≤ r)
                                        CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_20),
                                    i₁ pq = i₃ r pq' ⋯) →
                              (∀ (r r' : ℤ) (pq : κ)
                                  (hr :
                                    autoParam (r₀ ≤ r)
                                      CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_24)
                                  (hrr' :
                                    autoParam (r ≤ r')
                                      CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_26),
                                  i₀ r' pq ⋯ ≤ i₀ r pq ⋯) →
                                (∀ (r r' : ℤ) (pq : κ)
                                    (hr :
                                      autoParam (r₀ ≤ r)
                                        CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_32)
                                    (hrr' :
                                      autoParam (r ≤ r')
                                        CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_34),
                                    i₃ r pq ⋯ ≤ i₃ r' pq ⋯) →
                                  (∀ (r r' : ℤ) (pq pq' : κ),
                                      (c r).Rel pq pq' →
                                        ∀
                                          (hrr' :
                                            autoParam (r + 1 = r')
                                              CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_41)
                                          (hr :
                                            autoParam (r₀ ≤ r)
                                              CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_43),
                                          i₀ r' pq ⋯ = i₁ pq') →
                                    (∀ (r r' : ℤ) (pq pq' : κ),
                                        (c r).Rel pq pq' →
                                          ∀
                                            (hrr' :
                                              autoParam (r + 1 = r')
                                                CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_47)
                                            (hr :
                                              autoParam (r₀ ≤ r)
                                                CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_49),
                                            i₃ r' pq' ⋯ = i₂ pq) →
                                      CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀