-- 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 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) ⋯ ⋯)
⊢ 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) ⋯ ⋯)
have pos₃ : CategoryStruct.comp (Y := X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry)
    (Iso.hom (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' sorry sorry))
    (X.d (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ (n₂ + 1) sorry sorry sorry) =
  CategoryStruct.comp (Y := X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ sorry sorry)
    (Iso.hom (pageXIso X data r sorry pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' sorry sorry))
    (X.d (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₀ n₁ n₂ (n₂ + 1) sorry sorry sorry ≫
      𝟙 (X.E (homOfLE sorry) (homOfLE sorry) (homOfLE sorry) n₁ n₂ (n₂ + 1) sorry sorry))
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]