-- 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' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
⊢ pageD X data r pq pq' hr ≫ pageD X data r pq' pq'' hr = 0
have pos : Eq (α := pageX X data r pq hr ⟶ pageX X data r pq'' hr)
  (CategoryStruct.comp (Y :=
      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)
      (Iso.hom
          (pageXIso X data r sorry pq (data.i₀ r pq sorry) (data.i₁ pq) (data.i₂ pq) (data.i₃ r pq sorry) sorry sorry sorry sorry (data.deg pq - 1)
            (data.deg pq) (data.deg pq + 1) sorry sorry sorry) :
        pageX X data r pq 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)
      (CategoryStruct.comp (Y :=
          X.E (j := data.i₃ r pq'' sorry) (k := data.i₀ r pq sorry) (homOfLE sorry : data.i₂ pq'' ⟶ data.i₃ r pq'' sorry)
            (homOfLE sorry : data.i₃ r pq'' sorry ⟶ 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 (j := data.i₃ r pq'' sorry) (k := data.i₀ r pq sorry) (homOfLE sorry : data.i₂ pq'' ⟶ data.i₃ r pq'' sorry)
                (homOfLE sorry : data.i₃ r pq'' sorry ⟶ 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)
          (Iso.inv
              (pageXIso X data r sorry pq' (data.i₂ pq'') (data.i₃ r pq'' sorry) (data.i₀ r pq sorry) (data.i₁ pq) sorry sorry sorry sorry
                (data.deg pq) (data.deg pq + 1) (data.deg pq + 2) sorry sorry sorry) :
            X.E (j := data.i₃ r pq'' sorry) (homOfLE sorry : data.i₂ pq'' ⟶ data.i₃ r pq'' sorry)
                (homOfLE sorry : data.i₃ r pq'' sorry ⟶ data.i₀ r pq sorry) (homOfLE sorry) (data.deg pq) (data.deg pq + 1)
                (data.deg pq + 2) sorry sorry ⟶
              pageX X data r pq' 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 ⟶
          pageX X data r pq' sorry) ≫
    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]