-- Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
Goal:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι
X : SpectralObject.{u_1, u_2, v_1, u_2} C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
pos :
  Eq (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y :=
        X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
          (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
        (Iso.hom
            (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯
              (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⋯) :
          pageX X data r pq ⋯ ⟶
            X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
              (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
        (CategoryStruct.comp (Y :=
            X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
              (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
            (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
                (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ :
              X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
                  (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
                X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                  (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
            (Iso.inv
                (pageXIso X data r ⋯ pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯) :
              X.E (j := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                  (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯) (data.deg pq) (data.deg pq + 1)
                  (data.deg pq + 2) ⋯ ⋯ ⟶
                pageX X data r pq' ⋯) :
          X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
              (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
            pageX X data r pq' ⋯) ≫
      pageD X data r pq' pq'' hr)
    0
pos₁ :
  Eq (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y := pageX X data r pq' hr)
      (CategoryStruct.comp (Y :=
        X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
          (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
        (Iso.hom
            (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯
              (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⋯) :
          pageX X data r pq ⋯ ⟶
            X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
              (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
        (CategoryStruct.comp (Y :=
            X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
              (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
            (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
                (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ :
              X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
                  (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
                X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                  (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
            (Iso.inv
                (pageXIso X data r ⋯ pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯) :
              X.E (j := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                  (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯) (data.deg pq) (data.deg pq + 1)
                  (data.deg pq + 2) ⋯ ⋯ ⟶
                pageX X data r pq' ⋯) :
          X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
              (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
            pageX X data r pq' ⋯))
      (CategoryStruct.comp (Y :=
        X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
          (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
          (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
        (Iso.hom
            (pageXIso X data r ⋯ pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯
              (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯) :
          pageX X data r pq' ⋯ ⟶
            X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
              (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
        (CategoryStruct.comp (Y :=
            X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
              (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
              (data.deg pq + 2 + 1) ⋯ ⋯)
            (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq) (data.deg pq + 1)
                (data.deg pq + 2) (data.deg pq + 2 + 1) ⋯ ⋯ ⋯ :
              X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                  (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⟶
                X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                  (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                  (data.deg pq + 2 + 1) ⋯ ⋯)
            (Iso.inv
                (pageXIso X data r ⋯ pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯ ⋯ ⋯ ⋯
                  (data.deg pq + 1) (data.deg pq + 2) (data.deg pq + 2 + 1) ⋯ ⋯ ⋯) :
              X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                  (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                  (data.deg pq + 2 + 1) ⋯ ⋯ ⟶
                pageX X data r pq'' ⋯) :
          X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
              (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⟶
            pageX X data r pq'' ⋯)))
    0
pos₂ :
  Eq (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y :=
      X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
        (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
      (Iso.hom
          (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (data.deg pq - 1)
            (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
            (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
      (CategoryStruct.comp (Y := pageX X data r pq' hr)
          (CategoryStruct.comp (Y :=
            X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
              (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
            (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
                (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ :
              X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
                  (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
                X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                  (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
            (Iso.inv
                (pageXIso X data r ⋯ pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯) :
              X.E (j := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                  (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯) (data.deg pq) (data.deg pq + 1)
                  (data.deg pq + 2) ⋯ ⋯ ⟶
                pageX X data r pq' ⋯))
          (CategoryStruct.comp (Y :=
            X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
              (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
            (Iso.hom
                (pageXIso X data r ⋯ pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯) :
              pageX X data r pq' ⋯ ⟶
                X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                  (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
            (CategoryStruct.comp (Y :=
                X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                  (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                  (data.deg pq + 2 + 1) ⋯ ⋯)
                (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq) (data.deg pq + 1)
                    (data.deg pq + 2) (data.deg pq + 2 + 1) ⋯ ⋯ ⋯ :
                  X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                      (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                      (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⟶
                    X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                      (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                      (data.deg pq + 2 + 1) ⋯ ⋯)
                (Iso.inv
                    (pageXIso X data r ⋯ pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯ ⋯ ⋯
                      ⋯ (data.deg pq + 1) (data.deg pq + 2) (data.deg pq + 2 + 1) ⋯ ⋯ ⋯) :
                  X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                      (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                      (data.deg pq + 2 + 1) ⋯ ⋯ ⟶
                    pageX X data r pq'' ⋯) :
              X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                  (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⟶
                pageX X data r pq'' ⋯)) :
        X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
            (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
          pageX X data r pq'' hr))
    0
pos₃ :
  Eq (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y :=
      X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
        (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
      (Iso.hom
          (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (data.deg pq - 1)
            (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
            (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
      (CategoryStruct.comp (Y :=
          X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
            (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
          (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ :
            X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
                (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
              X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
                (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
          (CategoryStruct.comp (Y := pageX X data r pq' hr)
              (Iso.inv
                (pageXIso X data r ⋯ pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯))
              (CategoryStruct.comp (Y :=
                X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                  (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                  (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
                (Iso.hom
                    (pageXIso X data r ⋯ pq' (data.i₂ pq'') (data.i₃ r pq'' ⋯) (data.i₀ r pq ⋯) (data.i₁ pq) ⋯ ⋯ ⋯ ⋯
                      (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯) :
                  pageX X data r pq' ⋯ ⟶
                    X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                      (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                      (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
                (CategoryStruct.comp (Y :=
                    X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                      (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                      (data.deg pq + 2 + 1) ⋯ ⋯)
                    (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq) (data.deg pq + 1)
                        (data.deg pq + 2) (data.deg pq + 2 + 1) ⋯ ⋯ ⋯ :
                      X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                          (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                          (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⟶
                        X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯)
                          (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'') (homOfLE ⋯)
                          (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                          (data.deg pq + 2 + 1) ⋯ ⋯)
                    (Iso.inv
                        (pageXIso X data r ⋯ pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯
                          ⋯ ⋯ ⋯ (data.deg pq + 1) (data.deg pq + 2) (data.deg pq + 2 + 1) ⋯ ⋯ ⋯) :
                      X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                          (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                          (data.deg pq + 2 + 1) ⋯ ⋯ ⟶
                        pageX X data r pq'' ⋯) :
                  X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                      (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                      (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⟶
                    pageX X data r pq'' ⋯)) :
            X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
                (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⟶
              pageX X data r pq'' hr) :
        X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
            (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
          pageX X data r pq'' hr))
    0
pos₄ :
  Eq (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y :=
      X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
        (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
      (Iso.hom
          (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (data.deg pq - 1)
            (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
            (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
      (CategoryStruct.comp (Y :=
          X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
            (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
          (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⋯ :
            X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
                (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
              X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
                (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
          (CategoryStruct.comp (Y :=
              X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                (data.deg pq + 2 + 1) ⋯ ⋯)
              (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq) (data.deg pq + 1)
                  (data.deg pq + 2) (data.deg pq + 2 + 1) ⋯ ⋯ ⋯ :
                X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                    (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq)
                    (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⟶
                  X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                    (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                    (data.deg pq + 2 + 1) ⋯ ⋯)
              (Iso.inv
                  (pageXIso X data r ⋯ pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯ ⋯ ⋯ ⋯
                    (data.deg pq + 1) (data.deg pq + 2) (data.deg pq + 2 + 1) ⋯ ⋯ ⋯) :
                X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                    (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                    (data.deg pq + 2 + 1) ⋯ ⋯ ⟶
                  pageX X data r pq'' ⋯) :
            X.E (j := data.i₃ r pq'' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯)
                (homOfLE ⋯ : data.i₃ r pq'' ⋯ ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
                (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯ ⟶
              pageX X data r pq'' ⋯) :
        X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
            (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
          pageX X data r pq'' hr))
    0
pos₅ :
  Eq (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y :=
      X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
        (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
      (Iso.hom
          (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (data.deg pq - 1)
            (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
            (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
      (CategoryStruct.comp (Y :=
          X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'') (homOfLE ⋯)
            (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2) (data.deg pq + 2 + 1) ⋯ ⋯)
          (0 :
            X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
                (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
              X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                (data.deg pq + 2 + 1) ⋯ ⋯)
          (Iso.inv
              (pageXIso X data r ⋯ pq'' (data.i₀ r pq'' ⋯) (data.i₁ pq'') (data.i₂ pq'') (data.i₃ r pq'' ⋯) ⋯ ⋯ ⋯ ⋯
                (data.deg pq + 1) (data.deg pq + 2) (data.deg pq + 2 + 1) ⋯ ⋯ ⋯) :
            X.E (i := data.i₀ r pq'' ⋯) (l := data.i₃ r pq'' ⋯) (homOfLE ⋯ : data.i₀ r pq'' ⋯ ⟶ data.i₁ pq'')
                (homOfLE ⋯) (homOfLE ⋯ : data.i₂ pq'' ⟶ data.i₃ r pq'' ⋯) (data.deg pq + 1) (data.deg pq + 2)
                (data.deg pq + 2 + 1) ⋯ ⋯ ⟶
              pageX X data r pq'' ⋯) :
        X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
            (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
          pageX X data r pq'' hr))
    0
pos₆ :
  Eq (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
    (CategoryStruct.comp (Y :=
      X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
        (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
      (Iso.hom
          (pageXIso X data r ⋯ pq (data.i₀ r pq ⋯) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (data.deg pq - 1)
            (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
            (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯)
      (0 :
        X.E (i := data.i₀ r pq ⋯) (l := data.i₃ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (homOfLE ⋯)
            (homOfLE ⋯ : data.i₂ pq ⟶ data.i₃ r pq ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) ⋯ ⋯ ⟶
          pageX X data r pq'' hr))
    0
pos₇ pos₈ : Eq.{v_1 + 1} (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr) 0 0
⊢ pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0

Tactic:
rw [pageD_eq X data r hr pq pq' hpq (homOfLE (data.le₂₃ r pq''))
          (homOfLE (data.le₁₂' pq' (data.hc₁₃ r pq' pq'' hpq').symm
          (data.hc₀₂ r pq pq' hpq))) (homOfLE (data.le₀₁ r pq)) (homOfLE (data.le₁₂ pq))
          (homOfLE (data.le₂₃ r pq))
          (data.hc₀₂ r pq' pq'' hpq').symm (data.hc₁₃ r pq' pq'' hpq').symm rfl rfl rfl rfl
          (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) rfl,
        pageD_eq X data r hr pq' pq'' hpq' (homOfLE (data.le₀₁ r pq''))
          (homOfLE (data.le₁₂ pq'')) (homOfLE (data.le₂₃ r pq''))
          (homOfLE (data.le₁₂' pq' (data.hc₁₃ r pq' pq'' hpq').symm (data.hc₀₂ r pq pq' hpq)))
          (homOfLE (data.le₀₁ r pq)) rfl rfl
          (data.hc₀₂ r pq' pq'' hpq').symm (data.hc₁₃ r pq' pq'' hpq').symm
          (data.hc₀₂ r pq pq' hpq) (data.hc₁₃ r pq pq' hpq)
          _ _ (data.deg pq + 2) _ (data.hc r pq pq' hpq) rfl (by lia) rfl,
        Category.assoc, Category.assoc, Iso.inv_hom_id_assoc,
        d_d_assoc .., zero_comp, comp_zero]

Premises used: CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃, CategoryTheory.Category.assoc, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂, HSub.hSub, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂, CategoryTheory.Limits.comp_zero, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₁₃, HAdd.hAdd, CategoryTheory.homOfLE, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq, CategoryTheory.Abelian.SpectralObject.d_d_assoc, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg, CategoryTheory.Limits.zero_comp, OfNat.ofNat, Eq.symm, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂', rfl, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc