-- 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₀
inst_3 : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' : κ
hn₁ : data.deg pq' - 1 + 1 = data.deg pq'
hn₂ : data.deg pq' + 1 = data.deg pq' + 1
w :
  Eq (α := ((X.spectralSequence data).page r ⋯).homology pq' ⟶ ((X.spectralSequence data).page r' ⋯).X pq')
    (Iso.hom ((X.spectralSequence data).iso r r' pq' ⋯ ⋯) :
      ((X.spectralSequence data).page r ⋯).homology pq' ⟶ ((X.spectralSequence data).page r' ⋯).X pq')
    (Iso.hom
        (Iso.trans (Y := (((X.spectralSequence data).page r ⋯).sc' ((c r).prev pq') pq' ((c r).next pq')).homology)
          (((X.spectralSequence data).page r ⋯).homologyIsoSc' ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯)
          (Iso.trans (Y :=
            ShortComplex.LeftHomologyData.H (S :=
              ((X.spectralSequence data).page r hr).sc' ((c r).prev pq') pq' ((c r).next pq'))
              (ShortComplex.HomologyData.left
                (X.spectralSequenceHomologyData data r r' hrr' hr ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯
                  (data.i₀ r' pq' ⋯) (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₂ pq') (data.i₃ r pq' ⋯) (data.i₃ r' pq' ⋯)
                  ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯)))
            (ShortComplex.LeftHomologyData.homologyIso
              (ShortComplex.HomologyData.left
                (X.spectralSequenceHomologyData data r r' hrr' hr ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯
                  (data.i₀ r' pq' ⋯) (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₂ pq') (data.i₃ r pq' ⋯) (data.i₃ r' pq' ⋯)
                  ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯)))
            (Iso.symm
              (X.spectralSequencePageXIso 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) ⋯ ⋯ ⋯)))) :
      ((X.spectralSequence data).page r ⋯).homology pq' ⟶ ((X.spectralSequence data).page r' ⋯).X pq')
⊢ Eq (α := ((X.spectralSequence data).page r ⋯).homology pq' ≅ ((X.spectralSequence data).page r' ⋯).X pq')
    ((X.spectralSequence data).iso r r' pq' ⋯ ⋯ :
      ((X.spectralSequence data).page r ⋯).homology pq' ≅ ((X.spectralSequence data).page r' ⋯).X pq')
    (Iso.trans (Y := (((X.spectralSequence data).page r ⋯).sc' ((c r).prev pq') pq' ((c r).next pq')).homology)
        (((X.spectralSequence data).page r ⋯).homologyIsoSc' ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯)
        (Iso.trans (Y :=
          ShortComplex.LeftHomologyData.H (S :=
            ((X.spectralSequence data).page r hr).sc' ((c r).prev pq') pq' ((c r).next pq'))
            (ShortComplex.HomologyData.left
              (X.spectralSequenceHomologyData data r r' hrr' hr ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯
                (data.i₀ r' pq' ⋯) (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₂ pq') (data.i₃ r pq' ⋯) (data.i₃ r' pq' ⋯) ⋯
                ⋯ ⋯ ⋯ ⋯ ⋯ (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯)))
          (ShortComplex.LeftHomologyData.homologyIso
            (ShortComplex.HomologyData.left
              (X.spectralSequenceHomologyData data r r' hrr' hr ((c r).prev pq') pq' ((c r).next pq') ⋯ ⋯
                (data.i₀ r' pq' ⋯) (data.i₀ r pq' ⋯) (data.i₁ pq') (data.i₂ pq') (data.i₃ r pq' ⋯) (data.i₃ r' pq' ⋯) ⋯
                ⋯ ⋯ ⋯ ⋯ ⋯ (data.deg pq' - 1) (data.deg pq') (data.deg pq' + 1) ⋯ ⋯ ⋯)))
          (Iso.symm
            (X.spectralSequencePageXIso 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) ⋯ ⋯ ⋯))) :
      ((X.spectralSequence data).page r ⋯).homology pq' ≅ ((X.spectralSequence data).page r' ⋯).X pq')

Tactic:
ext