-- 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 pq' pq'' : κ
hpq : (c r).prev pq' = pq
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ i₃' : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
obtain :
  ∀ (hn₂ : n₁ + 1 = n₁ + 1),
    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' pq pq' pq'').homology)
          (((X.spectralSequence data).page r ⋯).homologyIsoSc' pq pq' pq'' hpq hpq')
          (Iso.trans (Y :=
            ShortComplex.LeftHomologyData.H (S := ((X.spectralSequence data).page r hr).sc' pq pq' pq'')
              (ShortComplex.HomologyData.left
                (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁
                  hi₂ hi₃ hi₃' (n₁ - 1) n₁ (n₁ + 1) hn₁' ⋯ ⋯)))
            (ShortComplex.LeftHomologyData.homologyIso
              (ShortComplex.HomologyData.left
                (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁
                  hi₂ hi₃ hi₃' (n₁ - 1) n₁ (n₁ + 1) hn₁' ⋯ ⋯)))
            (Iso.symm
              (X.spectralSequencePageXIso data r' ⋯ pq' i₀' i₁ i₂ i₃' hi₀' hi₁ hi₂ hi₃' (n₁ - 1) n₁ (n₁ + 1) hn₁' ⋯
                ⋯))) :
        ((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' pq pq' pq'').homology)
        (((X.spectralSequence data).page r ⋯).homologyIsoSc' pq pq' pq'' hpq hpq')
        (Iso.trans (Y :=
          ShortComplex.LeftHomologyData.H (S := ((X.spectralSequence data).page r hr).sc' pq pq' pq'')
            (ShortComplex.HomologyData.left
              (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁
                hi₂ hi₃ hi₃' (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯)))
          (ShortComplex.LeftHomologyData.homologyIso
            (ShortComplex.HomologyData.left
              (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁
                hi₂ hi₃ hi₃' (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯)))
          (Iso.symm
            (X.spectralSequencePageXIso data r' ⋯ pq' i₀' i₁ i₂ i₃' hi₀' hi₁ hi₂ hi₃' (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯))) :
      ((X.spectralSequence data).page r ⋯).homology pq' ≅ ((X.spectralSequence data).page r' ⋯).X pq')

Tactic:
obtain rfl : n₂ = n₁ + 1 := by lia

Premises used: rfl