awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
⊢ (π₂ ≫ π₁) ≫ 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.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 := sorry : ShortComplex.{v_1, u_1} C }.f ≫
      X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁
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]
-- 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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
have rw : X.toCycles f₃ f₄ (f₃ ≫ f₄) sorry n₁ ≫
    X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
  X.toCycles f₃ f₄ (f₃ ≫ f₄) sorry n₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
Tactic: rw [← cancel_epi (X.toCycles f₃ f₄ _ rfl n₁), toCycles_Ψ ..,
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_ιE .., toCycles_i_assoc, ← X.δ_naturality_assoc (f₁ ≫ f₂) (f₃ ≫ f₄) f₂ (f₃ ≫ f₄)
      (twoδ₁Toδ₀ f₁ f₂ _ rfl) (𝟙 _) n₁ n₂ rfl hn₂, Functor.map_id, id_comp]
-- 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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
⊢ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
have rw₁ : X.toCycles f₃ f₄ (f₃ ≫ f₄) sorry n₁ ≫
    X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
  X.δ f₂ (f₃ ≫ f₄) n₁ n₂ sorry ≫ X.pOpcycles f₂ f₃ n₂
Tactic: rw [← cancel_epi (X.toCycles f₃ f₄ _ rfl n₁), toCycles_Ψ ..,
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_ιE .., toCycles_i_assoc, ← X.δ_naturality_assoc (f₁ ≫ f₂) (f₃ ≫ f₄) f₂ (f₃ ≫ f₄)
      (twoδ₁Toδ₀ f₁ f₂ _ rfl) (𝟙 _) n₁ n₂ rfl hn₂, Functor.map_id, id_comp]
-- 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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
rw₁ :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
⊢ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
have rw₂ : X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫
    X.toCycles f₁ f₂ (f₁ ≫ f₂) sorry n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
  X.δ f₂ (f₃ ≫ f₄) n₁ n₂ sorry ≫ X.pOpcycles f₂ f₃ n₂
Tactic: rw [← cancel_epi (X.toCycles f₃ f₄ _ rfl n₁), toCycles_Ψ ..,
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_ιE .., toCycles_i_assoc, ← X.δ_naturality_assoc (f₁ ≫ f₂) (f₃ ≫ f₄) f₂ (f₃ ≫ f₄)
      (twoδ₁Toδ₀ f₁ f₂ _ rfl) (𝟙 _) n₁ n₂ rfl hn₂, Functor.map_id, id_comp]
-- 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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
rw₁ :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₂ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫
      X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
⊢ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
have rw₃ : X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) sorry n₂ ≫ X.iCycles f₁ f₂ n₂ ≫ X.pOpcycles f₂ f₃ n₂ =
  X.δ f₂ (f₃ ≫ f₄) n₁ n₂ sorry ≫ X.pOpcycles f₂ f₃ n₂
Tactic: rw [← cancel_epi (X.toCycles f₃ f₄ _ rfl n₁), toCycles_Ψ ..,
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_ιE .., toCycles_i_assoc, ← X.δ_naturality_assoc (f₁ ≫ f₂) (f₃ ≫ f₄) f₂ (f₃ ≫ f₄)
      (twoδ₁Toδ₀ f₁ f₂ _ rfl) (𝟙 _) n₁ n₂ rfl hn₂, Functor.map_id, id_comp]
-- 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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
rw₁ :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₂ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫
      X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₃ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.iCycles f₁ f₂ n₂ ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
⊢ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
have rw₄ : X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) sorry) ≫ X.pOpcycles f₂ f₃ n₂ =
  X.δ f₂ (f₃ ≫ f₄) n₁ n₂ sorry ≫ X.pOpcycles f₂ f₃ n₂
Tactic: rw [← cancel_epi (X.toCycles f₃ f₄ _ rfl n₁), toCycles_Ψ ..,
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_ιE .., toCycles_i_assoc, ← X.δ_naturality_assoc (f₁ ≫ f₂) (f₃ ≫ f₄) f₂ (f₃ ≫ f₄)
      (twoδ₁Toδ₀ f₁ f₂ _ rfl) (𝟙 _) n₁ n₂ rfl hn₂, Functor.map_id, id_comp]
-- 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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
rw₁ :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₂ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫
      X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₃ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.iCycles f₁ f₂ n₂ ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₄ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯) ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
⊢ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
have rw₅ : (X.H n₁).map (𝟙 (mk₁ (f₃ ≫ f₄))) ≫ X.δ f₂ (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.pOpcycles f₂ f₃ n₂ =
  X.δ f₂ (f₃ ≫ f₄) n₁ n₂ sorry ≫ X.pOpcycles f₂ f₃ n₂
Tactic: rw [← cancel_epi (X.toCycles f₃ f₄ _ rfl n₁), toCycles_Ψ ..,
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_ιE .., toCycles_i_assoc, ← X.δ_naturality_assoc (f₁ ≫ f₂) (f₃ ≫ f₄) f₂ (f₃ ≫ f₄)
      (twoδ₁Toδ₀ f₁ f₂ _ rfl) (𝟙 _) n₁ n₂ rfl hn₂, Functor.map_id, id_comp]
-- 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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
rw₁ :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₂ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫
      X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₃ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.iCycles f₁ f₂ n₂ ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₄ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯) ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₅ :
  (X.H n₁).map (𝟙 (mk₁ (f₃ ≫ f₄))) ≫ X.δ f₂ (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
⊢ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
have rw₆ : 𝟙 ((X.H n₁).obj (mk₁ (f₃ ≫ f₄))) ≫ X.δ f₂ (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.pOpcycles f₂ f₃ n₂ =
  X.δ f₂ (f₃ ≫ f₄) n₁ n₂ sorry ≫ X.pOpcycles f₂ f₃ n₂
Tactic: rw [← cancel_epi (X.toCycles f₃ f₄ _ rfl n₁), toCycles_Ψ ..,
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_ιE .., toCycles_i_assoc, ← X.δ_naturality_assoc (f₁ ≫ f₂) (f₃ ≫ f₄) f₂ (f₃ ≫ f₄)
      (twoδ₁Toδ₀ f₁ f₂ _ rfl) (𝟙 _) n₁ n₂ rfl hn₂, Functor.map_id, id_comp]
-- 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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
rw₁ :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₂ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫
      X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₃ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.iCycles f₁ f₂ n₂ ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₄ :
  X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯) ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₅ :
  (X.H n₁).map (𝟙 (mk₁ (f₃ ≫ f₄))) ≫ X.δ f₂ (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
rw₆ :
  𝟙 ((X.H n₁).obj (mk₁ (f₃ ≫ f₄))) ≫ X.δ f₂ (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.pOpcycles f₂ f₃ n₂ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
⊢ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂
have rw₇ : X.δ f₂ (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.pOpcycles f₂ f₃ n₂ = X.δ f₂ (f₃ ≫ f₄) n₁ n₂ sorry ≫ X.pOpcycles f₂ f₃ n₂
Tactic: rw [← cancel_epi (X.toCycles f₃ f₄ _ rfl n₁), toCycles_Ψ ..,
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_ιE .., toCycles_i_assoc, ← X.δ_naturality_assoc (f₁ ≫ f₂) (f₃ ≫ f₄) f₂ (f₃ ≫ f₄)
      (twoδ₁Toδ₀ f₁ f₂ _ rfl) (𝟙 _) n₁ n₂ rfl hn₂, Functor.map_id, id_comp]
-- 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₀ i₁ : ι
f₁ : i₀ ⟶ i₁
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.πE (𝟙 i₀) f₁ (𝟙 i₁) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₁ n₀ n₁ n₂ hn₁ hn₂).hom = (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom
have obtain : ∀ (hn₁ : n₁ - 1 + 1 = n₁),
  X.πE (𝟙 i₀) f₁ (𝟙 i₁) (n₁ - 1) n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₁ (n₁ - 1) n₁ n₂ hn₁ hn₂).hom =
    (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom
Tactic: obtain rfl : n₀ = n₁ - 1 := by lia
Cleared hypotheses: n₀, hn₁
-- 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₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
have rw : X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
    X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
  X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
Tactic: rw [← cancel_epi (X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles (𝟙 i₁) f₂ f₂ (by simp) n₁),
    X.toCycles_πE_d_assoc (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) f₁ (by simp) _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_EIsoH_hom .., πE_EIsoH_hom_assoc .., cyclesIsoH_inv_hom_id ..,
    comp_id, cyclesIsoH_inv_hom_id_assoc ..]
-- 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₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
⊢ X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
have rw₁ : X.toCycles (𝟙 i₁) f₂ f₂ sorry n₁ ≫
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
  X.toCycles (𝟙 i₁) f₂ f₂ sorry n₁ ≫
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
Tactic: rw [← cancel_epi (X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles (𝟙 i₁) f₂ f₂ (by simp) n₁),
    X.toCycles_πE_d_assoc (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) f₁ (by simp) _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_EIsoH_hom .., πE_EIsoH_hom_assoc .., cyclesIsoH_inv_hom_id ..,
    comp_id, cyclesIsoH_inv_hom_id_assoc ..]
-- 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₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₁ :
  X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
        X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
⊢ X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
have rw₂ : X.δ f₁ f₂ n₁ n₂ hn₂ ≫
    X.toCycles (𝟙 i₀) f₁ f₁ sorry n₂ ≫ X.πE (𝟙 i₀) f₁ (𝟙 i₁) n₁ n₂ n₃ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
  X.toCycles (𝟙 i₁) f₂ f₂ sorry n₁ ≫
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
Tactic: rw [← cancel_epi (X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles (𝟙 i₁) f₂ f₂ (by simp) n₁),
    X.toCycles_πE_d_assoc (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) f₁ (by simp) _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_EIsoH_hom .., πE_EIsoH_hom_assoc .., cyclesIsoH_inv_hom_id ..,
    comp_id, cyclesIsoH_inv_hom_id_assoc ..]
-- 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₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₁ :
  X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
        X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₂ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫
      X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ X.πE (𝟙 i₀) f₁ (𝟙 i₁) n₁ n₂ n₃ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
⊢ X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
have rw₃ : X.δ f₁ f₂ n₁ n₂ hn₂ ≫ X.toCycles (𝟙 i₀) f₁ f₁ sorry n₂ ≫ (X.cyclesIsoH f₁ n₂ n₃ sorry).hom =
  X.toCycles (𝟙 i₁) f₂ f₂ sorry n₁ ≫
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
Tactic: rw [← cancel_epi (X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles (𝟙 i₁) f₂ f₂ (by simp) n₁),
    X.toCycles_πE_d_assoc (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) f₁ (by simp) _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_EIsoH_hom .., πE_EIsoH_hom_assoc .., cyclesIsoH_inv_hom_id ..,
    comp_id, cyclesIsoH_inv_hom_id_assoc ..]