-- 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).next pq' = pq''
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' ⋯
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' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
    (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
        (Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
        (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯) :
      pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
    (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
          (Iso.hom (pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
          (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯ ≫
            Iso.inv (pageXIso X data r ⋯ pq'' (data.i₀ r pq'' ⋯) i₀' i₀ i₁ ⋯ ⋯ ⋯ ⋯ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯)) ≫
        Iso.hom (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) i₀' i₀ i₁ ⋯ ⋯ ⋯ ⋯ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯) :
      pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
pos₁ :
  Eq (α := pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
    (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
        (Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
        (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯) :
      pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
    (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
        (Iso.hom (pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
        ((X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯ ≫
            Iso.inv (pageXIso X data r ⋯ pq'' (data.i₀ r pq'' ⋯) i₀' i₀ i₁ ⋯ ⋯ ⋯ ⋯ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯)) ≫
          Iso.hom (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) i₀' i₀ i₁ ⋯ ⋯ ⋯ ⋯ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯)) :
      pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
pos₂ :
  Eq (α := pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
    (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
        (Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
        (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯) :
      pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
    (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
        (Iso.hom (pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
        (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯ ≫
          Iso.inv (pageXIso X data r ⋯ pq'' (data.i₀ r pq'' ⋯) i₀' i₀ i₁ ⋯ ⋯ ⋯ ⋯ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯) ≫
            Iso.hom (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) i₀' i₀ i₁ ⋯ ⋯ ⋯ ⋯ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯)) :
      pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
pos₃ :
  CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
      (Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
      (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯) =
    CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
      (Iso.hom (pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
      (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯ ≫
        𝟙 (X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯))
pos₄ pos₅ :
  Eq (α := pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
    (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
      (Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
      (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯))
    (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
      (Iso.hom (pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
      (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯))
⊢ Eq (α := pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
    (CategoryStruct.comp (Y := X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
        (Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
        (X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯) :
      pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)
    (pageD X data r pq' pq'' ⋯ ≫
        Iso.hom (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) i₀' i₀ i₁ ⋯ ⋯ ⋯ ⋯ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯) :
      pageX X data r pq' hr ⟶ X.E (i := data.i₀ r pq'' ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₁ n₂ (n₂ + 1) ⋯ ⋯)

Tactic:
rw [pageD_eq X data r hr pq' pq'' h
        (homOfLE (data.le₀₁' r hr pq'' rfl (by simpa [← data.i₀_prev r r' _ _ h])))
        (homOfLE (data.i₀_le' hrr' hr pq' hi₀' hi₀)) (homOfLE (data.le₀₁' r hr pq' hi₀ hi₁))
        (homOfLE (data.le₁₂' pq' hi₁ hi₂)) (homOfLE (data.le₂₃' r hr pq' hi₂ hi₃))
        rfl (by rw [hi₀', data.i₀_prev r r' _ _ h]) hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ (n₂ + 1) hn₁',
        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.Category.comp_id, HAdd.hAdd, CategoryTheory.homOfLE, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃', OfNat.ofNat, CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂', CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le', rfl