-- 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' : κ
hpq : (c r).Rel pq pq'
f₁ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq'
f₂ : data.i₁ pq' ⟶ data.i₀ r pq ⋯
f₃ : data.i₀ r pq ⋯ ⟶ data.i₁ pq
f₄ : data.i₁ pq ⟶ data.i₂ pq
f₅ : data.i₂ pq ⟶ data.i₃ r pq ⋯
hn₁ : data.deg pq - 1 + 1 = data.deg pq
hn₂ : data.deg pq + 1 = data.deg pq + 1
hn₃ : data.deg pq + 1 + 1 = data.deg pq + 2
rw :
  Eq (α := pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯)
    (CategoryStruct.comp (Y :=
        X.E (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
          (homOfLE ⋯ : data.i₁ 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 (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
              (homOfLE ⋯ : data.i₁ pq' ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
        (eqToHom ⋯ :
          X.E (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
              (homOfLE ⋯ : data.i₁ 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' ⋯) :
      pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯)
    (X.d f₁ f₂ f₃ f₄ f₅ (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) hn₁ hn₂ hn₃ ≫ eqToHom ⋯ :
      X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) hn₁ hn₂ ⟶
        pageX X data r pq' ⋯)
⊢ Eq (α := pageX X data r pq ⋯ ⟶ pageX X data r pq' ⋯)
    (if hpq : (c r).Rel pq pq' then
      CategoryStruct.comp (Y :=
        X.E (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
          (homOfLE ⋯ : data.i₁ 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 (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
              (homOfLE ⋯ : data.i₁ pq' ⟶ data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq ⋯ ⟶ data.i₁ pq) (data.deg pq)
              (data.deg pq + 1) (data.deg pq + 2) ⋯ ⋯)
        (eqToHom ⋯ :
          X.E (i := data.i₀ r pq' ⋯) (k := data.i₀ r pq ⋯) (homOfLE ⋯ : data.i₀ r pq' ⋯ ⟶ data.i₁ pq')
              (homOfLE ⋯ : data.i₁ 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' ⋯)
    else 0)
    (𝟙 (pageX X data r pq ⋯) ≫
      X.d f₁ f₂ f₃ f₄ f₅ (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) hn₁ hn₂ hn₃ ≫ eqToHom ⋯)

Tactic:
rw [dif_pos hpq, Category.id_comp]

Premises used: dif_pos, CategoryTheory.Category.id_comp