-- 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 r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
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₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst_3 : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
pos :
  Eq (α := pageX X data r pq ⋯ ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (CategoryStruct.comp (Y :=
      X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (Iso.hom (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯ :
        X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯ ⟶
          X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯))
    (CategoryStruct.comp (Y :=
        X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
        (Iso.hom (pageXIso X data r ⋯ pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) :
          pageX X data r pq ⋯ ⟶
            X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
        (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
            (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯)
            (Iso.inv (pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ hi₀ hi₁ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ⋯)) :
          X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯ ⟶
            pageX X data r pq' ⋯) ≫
      Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
pos₁ :
  Eq (α := pageX X data r pq ⋯ ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (CategoryStruct.comp (Y :=
      X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (Iso.hom (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯ :
        X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯ ⟶
          X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯))
    (CategoryStruct.comp (Y :=
      X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (Iso.hom (pageXIso X data r ⋯ pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
            (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯)
            (Iso.inv (pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ hi₀ hi₁ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ⋯)) ≫
          Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯) :
        X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯ ⟶
          X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯))
pos₂ :
  Eq (α := pageX X data r pq ⋯ ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (CategoryStruct.comp (Y :=
      X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (Iso.hom (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯ :
        X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯ ⟶
          X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯))
    (CategoryStruct.comp (Y :=
      X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (Iso.hom (pageXIso X data r ⋯ pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
          (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯)
          (Iso.inv (pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ hi₀ hi₁ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ⋯) ≫
            Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯)) :
        X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯ ⟶
          X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯))
pos₃ :
  CategoryStruct.comp (Y :=
      X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (Iso.hom (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯ :
        X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯ ⟶
          X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯) =
    Iso.hom (pageXIso X data r ⋯ pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) ≫
      X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯ ≫
        𝟙 (X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
pos₄ pos₅ :
  Eq (α := pageX X data r pq ⋯ ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (CategoryStruct.comp (Y :=
      X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (Iso.hom (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯ :
        X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯ ⟶
          X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯))
    (CategoryStruct.comp (Y :=
      X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (Iso.hom (pageXIso X data r ⋯ pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯ :
        X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯ ⟶
          X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯))
⊢ Eq (α := pageX X data r pq ⋯ ⟶ X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
    (CategoryStruct.comp (Y :=
      X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (Iso.hom (pageXIso X data r hr pq i₂ i₃ i₃' (data.i₃ r pq ⋯) ⋯ ⋯ ⋯ ⋯ (n₀ - 1) n₀ n₁ ⋯ ⋯ ⋯) :
        pageX X data r pq ⋯ ⟶
          X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯)
      (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯ :
        X.E (l := data.i₃ r pq ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯ : i₃' ⟶ data.i₃ r pq ⋯) (n₀ - 1) n₀ n₁ ⋯ ⋯ ⟶
          X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯))
    (pageD X data r pq pq' ⋯ ≫ Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))

Tactic:
rw [pageD_eq X data r hr pq pq' h
          (homOfLE (data.le₀₁' r hr pq' hi₀ hi₁)) (homOfLE (data.le₁₂' pq' hi₁ hi₂))
          (homOfLE (data.le₂₃' r hr pq' hi₂ hi₃)) (homOfLE (data.le₃₃' hrr' hr pq' hi₃ hi₃'))
          (homOfLE (data.le₂₃' r hr pq (by rw [hi₃', data.i₃_next r r' pq pq' h]) rfl))
          hi₀ hi₁ (hi₂.trans (data.hc₀₂ r pq pq' h).symm)
          (hi₃.trans (data.hc₁₃ r pq pq' h).symm) (hi₃'.trans (data.i₃_next r r' pq pq' h)) rfl
          (n₀ - 1) n₀ n₁ n₂ (by have := data.hc r _ _ h; lia),
        Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁', CategoryTheory.Iso.inv_hom_id, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃_next, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂, HSub.hSub, CategoryTheory.Category.comp_id, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₁₃, CategoryTheory.homOfLE, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃', CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₃₃', OfNat.ofNat, Eq.symm, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂', rfl, Eq.trans