-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (goal)
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
⊢ 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 ⋯)
have rw : Eq (α := pageX X data r pq sorry ⟶ pageX X data r pq' sorry)
  (CategoryStruct.comp (Y :=
      X.E (i := data.i₀ r pq' sorry) (k := data.i₀ r pq sorry) (homOfLE sorry : data.i₀ r pq' sorry ⟶ data.i₁ pq')
        (homOfLE sorry : data.i₁ pq' ⟶ data.i₀ r pq sorry) (homOfLE sorry : data.i₀ r pq sorry ⟶ data.i₁ pq) (data.deg pq)
        (data.deg pq + 1) (data.deg pq + 2) sorry sorry)
      (X.d (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1)
          (data.deg pq + 2) sorry sorry sorry :
        X.E (i := data.i₀ r pq sorry) (l := data.i₃ r pq sorry) (homOfLE sorry : data.i₀ r pq sorry ⟶ data.i₁ pq) (homOfLE sorry)
            (homOfLE sorry : data.i₂ pq ⟶ data.i₃ r pq sorry) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) sorry sorry ⟶
          X.E (i := data.i₀ r pq' sorry) (k := data.i₀ r pq sorry) (homOfLE sorry : data.i₀ r pq' sorry ⟶ data.i₁ pq')
            (homOfLE sorry : data.i₁ pq' ⟶ data.i₀ r pq sorry) (homOfLE sorry : data.i₀ r pq sorry ⟶ data.i₁ pq) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) sorry sorry)
      (eqToHom sorry :
        X.E (i := data.i₀ r pq' sorry) (k := data.i₀ r pq sorry) (homOfLE sorry : data.i₀ r pq' sorry ⟶ data.i₁ pq')
            (homOfLE sorry : data.i₁ pq' ⟶ data.i₀ r pq sorry) (homOfLE sorry : data.i₀ r pq sorry ⟶ data.i₁ pq) (data.deg pq)
            (data.deg pq + 1) (data.deg pq + 2) sorry sorry ⟶
          pageX X data r pq' sorry) :
    pageX X data r pq sorry ⟶ pageX X data r pq' sorry)
  (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 sorry :
    X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (data.deg pq - 1) (data.deg pq) (data.deg pq + 1) hn₁ hn₂ ⟶
      pageX X data r pq' sorry)
Tactic: rw [dif_pos hpq, Category.id_comp]