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₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ 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.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₂ =
    X.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.fromOpcycles f₄ f₅ f₄₅ h₄₅ n₁ ≫ X.δ f₂₃ f₄₅ n₁ n₂ hn₂
have rw : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) ≫ X.δ f₂₃ f₄ n₁ n₂ sorry =
  X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) sorry ≫ twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃)
Tactic: rw [← cancel_epi (X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₃ f₄ f₃₄ h₃₄ n₁),
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_ιE_assoc .., p_fromOpcycles, toCycles_i_assoc, fromOpcyles_δ ..,
    πE_ιE_assoc .., pOpcycles_δFromOpcycles, toCycles_i_assoc, ← Functor.map_comp, Eq.comm]
-- 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₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) ≫ X.δ f₂₃ f₄ n₁ n₂ ⋯ =
    X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯ ≫ twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃)
have hαβ : autoParam
  (Eq (α := (mk₁ (f₁ ≫ f₂)).obj 1 ⟶ (mk₁ f₂₃).obj 1) ((twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) sorry ≫ twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃).app 1)
    ((twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄).app 0))
  δ_naturality._auto_1
Tactic: apply δ_naturality
-- 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₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₆ : i₅ ⟶ i₆
f₇ : i₆ ⟶ i₇
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
⊢ X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ = 0
have rw : 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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
  X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
Tactic: rw [← cancel_epi (X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁), comp_zero, comp_zero,
    X.toCycles_πE_d_assoc f₃ f₄ f₅ f₆ f₇ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    X.toCycles_πE_d f₁ f₂ f₃ f₄ f₅ _ rfl _ rfl n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄,
    δ_δ_assoc .., zero_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₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₆ : i₅ ⟶ i₆
f₇ : i₆ ⟶ i₇
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
rw :
  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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
⊢ X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ = 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
  X.toCycles f₅ f₆ (f₅ ≫ f₆) sorry n₁ ≫ X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
Tactic: rw [← cancel_epi (X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁), comp_zero, comp_zero,
    X.toCycles_πE_d_assoc f₃ f₄ f₅ f₆ f₇ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    X.toCycles_πE_d f₁ f₂ f₃ f₄ f₅ _ rfl _ rfl n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄,
    δ_δ_assoc .., zero_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₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₆ : i₅ ⟶ i₆
f₇ : i₆ ⟶ i₇
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
rw :
  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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
⊢ X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ = 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
  X.toCycles f₅ f₆ (f₅ ≫ f₆) sorry n₁ ≫ 0
Tactic: rw [← cancel_epi (X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁), comp_zero, comp_zero,
    X.toCycles_πE_d_assoc f₃ f₄ f₅ f₆ f₇ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    X.toCycles_πE_d f₁ f₂ f₃ f₄ f₅ _ rfl _ rfl n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄,
    δ_δ_assoc .., zero_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₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₆ : i₅ ⟶ i₆
f₇ : i₆ ⟶ i₇
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
rw :
  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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ 0
⊢ X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ = 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
  0
Tactic: rw [← cancel_epi (X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁), comp_zero, comp_zero,
    X.toCycles_πE_d_assoc f₃ f₄ f₅ f₆ f₇ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    X.toCycles_πE_d f₁ f₂ f₃ f₄ f₅ _ rfl _ rfl n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄,
    δ_δ_assoc .., zero_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₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₆ : i₅ ⟶ i₆
f₇ : i₆ ⟶ i₇
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
rw :
  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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    0
⊢ X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ = 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
  0
Tactic: rw [← cancel_epi (X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁), comp_zero, comp_zero,
    X.toCycles_πE_d_assoc f₃ f₄ f₅ f₆ f₇ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    X.toCycles_πE_d f₁ f₂ f₃ f₄ f₅ _ rfl _ rfl n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄,
    δ_δ_assoc .., zero_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₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₆ : i₅ ⟶ i₆
f₇ : i₆ ⟶ i₇
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
rw :
  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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    0
⊢ X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ = 0
have rw₅ : X.δ (f₃ ≫ f₄) (f₅ ≫ f₆) n₁ n₂ hn₂ ≫
    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₄ =
  0
Tactic: rw [← cancel_epi (X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁), comp_zero, comp_zero,
    X.toCycles_πE_d_assoc f₃ f₄ f₅ f₆ f₇ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    X.toCycles_πE_d f₁ f₂ f₃ f₄ f₅ _ rfl _ rfl n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄,
    δ_δ_assoc .., zero_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₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₆ : i₅ ⟶ i₆
f₇ : i₆ ⟶ i₇
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
rw :
  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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    0
rw₅ :
  X.δ (f₃ ≫ f₄) (f₅ ≫ f₆) n₁ n₂ hn₂ ≫
      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₄ =
    0
⊢ X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ = 0
have rw₆ : Eq (α := (X.H n₁).obj (mk₁ (f₅ ≫ f₆)) ⟶ X.E f₁ f₂ f₃ n₂ n₃ n₄ hn₃ hn₄)
  (0 ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) sorry n₃ ≫ X.πE f₁ f₂ f₃ n₂ n₃ n₄ hn₃ hn₄) 0
Tactic: rw [← cancel_epi (X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁), comp_zero, comp_zero,
    X.toCycles_πE_d_assoc f₃ f₄ f₅ f₆ f₇ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    X.toCycles_πE_d f₁ f₂ f₃ f₄ f₅ _ rfl _ rfl n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄,
    δ_δ_assoc .., zero_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₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₆ : i₅ ⟶ i₆
f₇ : i₆ ⟶ i₇
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
rw :
  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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ 0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    0
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.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    0
rw₅ :
  X.δ (f₃ ≫ f₄) (f₅ ≫ f₆) n₁ n₂ hn₂ ≫
      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₄ =
    0
rw₆ :
  Eq (α := (X.H n₁).obj (mk₁ (f₅ ≫ f₆)) ⟶ X.E f₁ f₂ f₃ n₂ n₃ n₄ hn₃ hn₄)
    (0 ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₃ ≫ X.πE f₁ f₂ f₃ n₂ n₃ n₄ hn₃ hn₄) 0
⊢ X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ = 0
have rw₇ : Eq.{v_1 + 1} (α := (X.H n₁).obj (mk₁ (f₅ ≫ f₆)) ⟶ X.E f₁ f₂ f₃ n₂ n₃ n₄ hn₃ hn₄) 0 0
Tactic: rw [← cancel_epi (X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁), comp_zero, comp_zero,
    X.toCycles_πE_d_assoc f₃ f₄ f₅ f₆ f₇ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    X.toCycles_πE_d f₁ f₂ f₃ f₄ f₅ _ rfl _ rfl n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄,
    δ_δ_assoc .., zero_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 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₁
⊢ (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ (f₂ ≫ f₃) ⋯) ≫ X.δ f₁ (f₂ ≫ f₃) n₀ n₁ hn₁ ≫ X.pOpcycles f₁ f₂ n₁ = 0
have rw : X.δ f₁ f₂ n₀ n₁ sorry ≫ (X.H n₁).map (𝟙 (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂ n₁ = 0
Tactic: rw [X.δ_naturality_assoc f₁ f₂ f₁ (f₂ ≫ f₃) (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ _ rfl) _ _ rfl,
        Functor.map_id, id_comp, δ_pOpcycles ..]
-- 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₁
rw : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ (X.H n₁).map (𝟙 (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂ n₁ = 0
⊢ (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ (f₂ ≫ f₃) ⋯) ≫ X.δ f₁ (f₂ ≫ f₃) n₀ n₁ hn₁ ≫ X.pOpcycles f₁ f₂ n₁ = 0
have rw₁ : X.δ f₁ f₂ n₀ n₁ sorry ≫ 𝟙 ((X.H n₁).obj (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂ n₁ = 0
Tactic: rw [X.δ_naturality_assoc f₁ f₂ f₁ (f₂ ≫ f₃) (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ _ rfl) _ _ rfl,
        Functor.map_id, id_comp, δ_pOpcycles ..]
-- 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₁
rw : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ (X.H n₁).map (𝟙 (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂ n₁ = 0
rw₁ : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ 𝟙 ((X.H n₁).obj (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂ n₁ = 0
⊢ (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ (f₂ ≫ f₃) ⋯) ≫ X.δ f₁ (f₂ ≫ f₃) n₀ n₁ hn₁ ≫ X.pOpcycles f₁ f₂ n₁ = 0
have rw₂ : X.δ f₁ f₂ n₀ n₁ sorry ≫ X.pOpcycles f₁ f₂ n₁ = 0
Tactic: rw [X.δ_naturality_assoc f₁ f₂ f₁ (f₂ ≫ f₃) (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ _ rfl) _ _ rfl,
        Functor.map_id, id_comp, δ_pOpcycles ..]
-- 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₁
rw : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ (X.H n₁).map (𝟙 (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂ n₁ = 0
rw₁ : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ 𝟙 ((X.H n₁).obj (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂ n₁ = 0
rw₂ : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ X.pOpcycles f₁ f₂ n₁ = 0
⊢ (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ (f₂ ≫ f₃) ⋯) ≫ X.δ f₁ (f₂ ≫ f₃) n₀ n₁ hn₁ ≫ X.pOpcycles f₁ f₂ n₁ = 0
have rw₃ : Eq.{v_1 + 1} (α := (X.H n₀).obj (mk₁ f₂) ⟶ X.opcycles f₁ f₂ n₁) 0 0
Tactic: rw [X.δ_naturality_assoc f₁ f₂ f₁ (f₂ ≫ f₃) (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ _ rfl) _ _ rfl,
        Functor.map_id, id_comp, δ_pOpcycles ..]
-- 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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = X.δ f₁ f₂₃ n₀ n₁ hn₁ ≫ X.pOpcycles f₁ f₂ n₁
have subst : X.toCycles f₂ f₃ (f₂ ≫ f₃) sorry n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = X.δ f₁ (f₂ ≫ f₃) n₀ n₁ hn₁ ≫ X.pOpcycles f₁ f₂ n₁
Tactic: subst h₂₃
Cleared hypotheses: f₂₃, h₂₃
-- 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₁₂
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ = X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁
have rw : X.δ f₁ (f₂ ≫ f₃) n₀ n₁ sorry ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) =
  (X.H n₀).map (twoδ₁Toδ₀ f₂ f₃ (f₂ ≫ f₃) sorry) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁
Tactic: rw [← cancel_epi (X.toCycles f₂ f₃ _ rfl n₀),
    toCycles_Ψ_assoc .., p_fromOpcycles, toCycles_i_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 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₁
⊢ f₁₂ ≫ f₃ = f₁ ≫ f₂ ≫ f₃
have rw : f₁₂ ≫ f₃ = f₁₂ ≫ f₃
Tactic: rw [reassoc_of% h₁₂]
-- 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₁
⊢ f₁ ≫ f₂₃ = f₁ ≫ f₂ ≫ f₃
have rw : f₁ ≫ f₂₃ = f₁ ≫ f₂₃
Tactic: rw [h₂₃]
-- 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₁
⊢ X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = 0
have rw : Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
  (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) sorry n₀ ≫
    X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
  (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) sorry n₀ ≫ 0)
Tactic: rw [← cancel_epi (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) n₀), comp_zero,
    X.toCycles_cyclesMap_assoc f₁₂ f₃ f₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) f₂₃ h₂₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂)
    (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃])) n₀ rfl rfl,
    toCycles_Ψ .., zero₃_assoc .., zero_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 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₁
rw :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫ 0)
⊢ X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = 0
have rw₁ : Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
  (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) sorry n₀ ≫
    X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
  0
Tactic: rw [← cancel_epi (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) n₀), comp_zero,
    X.toCycles_cyclesMap_assoc f₁₂ f₃ f₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) f₂₃ h₂₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂)
    (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃])) n₀ rfl rfl,
    toCycles_Ψ .., zero₃_assoc .., zero_comp]