-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.mk.injEq : ∀ {ι : 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 → ι)
  (le₀₁ :
    ∀ (r : ℤ) (pq : κ) (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_5),
      i₀ r pq ⋯ ≤ i₁ pq)
  (le₁₂ : ∀ (pq : κ), i₁ pq ≤ i₂ pq)
  (le₂₃ :
    ∀ (r : ℤ) (pq : κ) (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_9),
      i₂ pq ≤ i₃ r pq ⋯)
  (hc :
    ∀ (r : ℤ) (pq pq' : κ),
      (c r).Rel pq pq' →
        autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_14 →
          deg pq + 1 = deg pq')
  (hc₀₂ :
    ∀ (r : ℤ) (pq pq' : κ),
      (c r).Rel pq pq' →
        ∀ (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_16),
          i₀ r pq ⋯ = i₂ pq')
  (hc₁₃ :
    ∀ (r : ℤ) (pq pq' : κ),
      (c r).Rel pq pq' →
        ∀ (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_20),
          i₁ pq = i₃ r pq' ⋯)
  (antitone_i₀ :
    ∀ (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 ⋯)
  (monotone_i₃ :
    ∀ (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 ⋯)
  (i₀_prev :
    ∀ (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')
  (i₃_next :
    ∀ (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)
  (deg_1 : κ → ℤ)
  (i₀_1 : (r : ℤ) → κ → autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_1 → ι)
  (i₁_1 i₂_1 : κ → ι)
  (i₃_1 : (r : ℤ) → κ → autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_3 → ι)
  (le₀₁_1 :
    ∀ (r : ℤ) (pq : κ) (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_5),
      i₀_1 r pq ⋯ ≤ i₁_1 pq)
  (le₁₂_1 : ∀ (pq : κ), i₁_1 pq ≤ i₂_1 pq)
  (le₂₃_1 :
    ∀ (r : ℤ) (pq : κ) (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_9),
      i₂_1 pq ≤ i₃_1 r pq ⋯)
  (hc_1 :
    ∀ (r : ℤ) (pq pq' : κ),
      (c r).Rel pq pq' →
        autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_14 →
          deg_1 pq + 1 = deg_1 pq')
  (hc₀₂_1 :
    ∀ (r : ℤ) (pq pq' : κ),
      (c r).Rel pq pq' →
        ∀ (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_16),
          i₀_1 r pq ⋯ = i₂_1 pq')
  (hc₁₃_1 :
    ∀ (r : ℤ) (pq pq' : κ),
      (c r).Rel pq pq' →
        ∀ (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_20),
          i₁_1 pq = i₃_1 r pq' ⋯)
  (antitone_i₀_1 :
    ∀ (r r' : ℤ) (pq : κ)
      (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_24)
      (hrr' : autoParam (r ≤ r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_26),
      i₀_1 r' pq ⋯ ≤ i₀_1 r pq ⋯)
  (monotone_i₃_1 :
    ∀ (r r' : ℤ) (pq : κ)
      (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_32)
      (hrr' : autoParam (r ≤ r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_34),
      i₃_1 r pq ⋯ ≤ i₃_1 r' pq ⋯)
  (i₀_prev_1 :
    ∀ (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₀_1 r' pq ⋯ = i₁_1 pq')
  (i₃_next_1 :
    ∀ (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₃_1 r' pq' ⋯ = i₂_1 pq),
  ({ deg := deg, i₀ := i₀, i₁ := i₁, i₂ := i₂, i₃ := i₃, le₀₁ := le₀₁, le₁₂ := le₁₂, le₂₃ := le₂₃, hc := hc,
        hc₀₂ := hc₀₂, hc₁₃ := hc₁₃, antitone_i₀ := antitone_i₀, monotone_i₃ := monotone_i₃, i₀_prev := i₀_prev,
        i₃_next := i₃_next } =
      { deg := deg_1, i₀ := i₀_1, i₁ := i₁_1, i₂ := i₂_1, i₃ := i₃_1, le₀₁ := le₀₁_1, le₁₂ := le₁₂_1, le₂₃ := le₂₃_1,
        hc := hc_1, hc₀₂ := hc₀₂_1, hc₁₃ := hc₁₃_1, antitone_i₀ := antitone_i₀_1, monotone_i₃ := monotone_i₃_1,
        i₀_prev := i₀_prev_1, i₃_next := i₃_next_1 }) =
    (deg = deg_1 ∧ i₀ = i₀_1 ∧ i₁ = i₁_1 ∧ i₂ = i₂_1 ∧ i₃ = i₃_1)