-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.mk.inj : ∀ {ι : 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