-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z₀ :
  A ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
z₂ : A₂ ⟶ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).X₁
hz₂ : π₂ ≫ z₁ = z₂ ≫ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).f
rw :
  ((π₂ ≫ π₁) ≫ z₀) ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ =
    ((z₂ ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀) ≫
        { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
            g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
            ShortComplex.{v_1, u_1} C }.f) ≫
      X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁
rw₁ :
  (π₂ ≫ π₁) ≫ z₀ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ =
    ((z₂ ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀) ≫
        { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
            g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
            ShortComplex.{v_1, u_1} C }.f) ≫
      X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁
rw₂ :
  π₂ ≫ π₁ ≫ z₀ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ =
    ((z₂ ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀) ≫
        { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
            g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
            ShortComplex.{v_1, u_1} C }.f) ≫
      X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁
rw₃ :
  π₂ ≫ π₁ ≫ z₀ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ =
    (z₂ ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀) ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
            g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
            ShortComplex.{v_1, u_1} C }.f ≫
        X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁
rw₄ :
  π₂ ≫ π₁ ≫ z₀ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ =
    z₂ ≫
      X.toCycles f₂ f₃ f₂₃ h₂₃ n₀ ≫
        { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
              g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
              ShortComplex.{v_1, u_1} C }.f ≫
          X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁
rw₅ :
  π₂ ≫ π₁ ≫ z₀ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ =
    z₂ ≫ X.δ f₁ f₂₃ n₀ n₁ ⋯ ≫ X.pOpcycles f₁ f₂ n₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁
rw₆ : π₂ ≫ π₁ ≫ z₀ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ = z₂ ≫ X.δ f₁ f₂₃ n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)
⊢ (π₂ ≫ π₁) ≫ z₀ =
    (z₂ ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀) ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.f
have rw₇ : π₂ ≫ π₁ ≫ z₀ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ = π₂ ≫ z₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)
Tactic: rw [← cancel_mono (X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁), assoc, assoc,
    assoc, assoc, toCycles_Ψ_assoc .., p_fromOpcycles, ← reassoc_of% dsimp% hz₂,
    reassoc_of% hz₁, p_fromOpcycles]