awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (hypothesis)
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 : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n : ℤ
hg : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ g))
⊢ IsIso (X.fromOpcycles f g fg h n)
have this : Epi (X.fromOpcycles f g fg h n)
Tactic: have : Epi (X.fromOpcycles f g fg h n) :=
    (X.kernelSequenceOpcycles_exact f g fg h n).epi_f (hg.eq_of_tgt _ _)
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw : (X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) ≫ X.iCycles f₁ f₂ n₁ =
  X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
Tactic: rw [← cancel_mono (X.iCycles f₁ f₂ n₁), Category.assoc,
    toCycles_i, δToCycles_iCycles,
    ← X.δ_naturality f₁₂ f₃ f₂ f₃ (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) (𝟙 _) n₀ n₁,
    Functor.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₁
rw :
  (X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
⊢ X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw₁ : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.iCycles f₁ f₂ n₁ =
  X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
Tactic: rw [← cancel_mono (X.iCycles f₁ f₂ n₁), Category.assoc,
    toCycles_i, δToCycles_iCycles,
    ← X.δ_naturality f₁₂ f₃ f₂ f₃ (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) (𝟙 _) n₀ n₁,
    Functor.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₁
rw :
  (X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₁ :
  X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
⊢ X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw₂ : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
Tactic: rw [← cancel_mono (X.iCycles f₁ f₂ n₁), Category.assoc,
    toCycles_i, δToCycles_iCycles,
    ← X.δ_naturality f₁₂ f₃ f₂ f₃ (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) (𝟙 _) n₀ n₁,
    Functor.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₁
rw :
  (X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₁ :
  X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₂ :
  X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
⊢ X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw₃ : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δ f₂ f₃ n₀ n₁ hn₁
Tactic: rw [← cancel_mono (X.iCycles f₁ f₂ n₁), Category.assoc,
    toCycles_i, δToCycles_iCycles,
    ← X.δ_naturality f₁₂ f₃ f₂ f₃ (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) (𝟙 _) n₀ n₁,
    Functor.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₁
rw :
  (X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₁ :
  X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₂ :
  X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₃ : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δ f₂ f₃ n₀ n₁ hn₁
⊢ X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw₄ : (X.H n₀).map (𝟙 (mk₁ f₃)) ≫ X.δ f₂ f₃ n₀ n₁ sorry = X.δ f₂ f₃ n₀ n₁ hn₁
Tactic: rw [← cancel_mono (X.iCycles f₁ f₂ n₁), Category.assoc,
    toCycles_i, δToCycles_iCycles,
    ← X.δ_naturality f₁₂ f₃ f₂ f₃ (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) (𝟙 _) n₀ n₁,
    Functor.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₁
rw :
  (X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₁ :
  X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₂ :
  X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₃ : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δ f₂ f₃ n₀ n₁ hn₁
rw₄ : (X.H n₀).map (𝟙 (mk₁ f₃)) ≫ X.δ f₂ f₃ n₀ n₁ ⋯ = X.δ f₂ f₃ n₀ n₁ hn₁
⊢ X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw₅ : 𝟙 ((X.H n₀).obj (mk₁ f₃)) ≫ X.δ f₂ f₃ n₀ n₁ sorry = X.δ f₂ f₃ n₀ n₁ hn₁
Tactic: rw [← cancel_mono (X.iCycles f₁ f₂ n₁), Category.assoc,
    toCycles_i, δToCycles_iCycles,
    ← X.δ_naturality f₁₂ f₃ f₂ f₃ (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) (𝟙 _) n₀ n₁,
    Functor.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₁
rw :
  (X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₁ :
  X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₂ :
  X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₃ : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δ f₂ f₃ n₀ n₁ hn₁
rw₄ : (X.H n₀).map (𝟙 (mk₁ f₃)) ≫ X.δ f₂ f₃ n₀ n₁ ⋯ = X.δ f₂ f₃ n₀ n₁ hn₁
rw₅ : 𝟙 ((X.H n₀).obj (mk₁ f₃)) ≫ X.δ f₂ f₃ n₀ n₁ ⋯ = X.δ f₂ f₃ n₀ n₁ hn₁
⊢ X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw₆ : X.δ f₂ f₃ n₀ n₁ sorry = X.δ f₂ f₃ n₀ n₁ hn₁
Tactic: rw [← cancel_mono (X.iCycles f₁ f₂ n₁), Category.assoc,
    toCycles_i, δToCycles_iCycles,
    ← X.δ_naturality f₁₂ f₃ f₂ f₃ (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) (𝟙 _) n₀ n₁,
    Functor.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw : X.pOpcycles f₂ f₃ n₀ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
  X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
Tactic: rw [← cancel_epi (X.pOpcycles f₂ f₃ n₀),
    p_fromOpcycles_assoc, pOpcycles_δFromOpcycles,
    X.δ_naturality f₁ f₂ f₁ f₂₃ (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) n₀ n₁,
    Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₁
rw :
  X.pOpcycles f₂ f₃ n₀ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
    X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
⊢ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw₁ : (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
  X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
Tactic: rw [← cancel_epi (X.pOpcycles f₂ f₃ n₀),
    p_fromOpcycles_assoc, pOpcycles_δFromOpcycles,
    X.δ_naturality f₁ f₂ f₁ f₂₃ (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) n₀ n₁,
    Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₁
rw :
  X.pOpcycles f₂ f₃ n₀ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
    X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
rw₁ :
  (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
    X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
⊢ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw₂ : (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δ f₁ f₂ n₀ n₁ hn₁
Tactic: rw [← cancel_epi (X.pOpcycles f₂ f₃ n₀),
    p_fromOpcycles_assoc, pOpcycles_δFromOpcycles,
    X.δ_naturality f₁ f₂ f₁ f₂₃ (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) n₀ n₁,
    Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₁
rw :
  X.pOpcycles f₂ f₃ n₀ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
    X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
rw₁ :
  (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
    X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
rw₂ : (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δ f₁ f₂ n₀ n₁ hn₁
⊢ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw₃ : X.δ f₁ f₂ n₀ n₁ sorry ≫ (X.H n₁).map (𝟙 (mk₁ f₁)) = X.δ f₁ f₂ n₀ n₁ hn₁
Tactic: rw [← cancel_epi (X.pOpcycles f₂ f₃ n₀),
    p_fromOpcycles_assoc, pOpcycles_δFromOpcycles,
    X.δ_naturality f₁ f₂ f₁ f₂₃ (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) n₀ n₁,
    Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₁
rw :
  X.pOpcycles f₂ f₃ n₀ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
    X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
rw₁ :
  (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
    X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
rw₂ : (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δ f₁ f₂ n₀ n₁ hn₁
rw₃ : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ (X.H n₁).map (𝟙 (mk₁ f₁)) = X.δ f₁ f₂ n₀ n₁ hn₁
⊢ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw₄ : X.δ f₁ f₂ n₀ n₁ sorry ≫ 𝟙 ((X.H n₁).obj (mk₁ f₁)) = X.δ f₁ f₂ n₀ n₁ hn₁
Tactic: rw [← cancel_epi (X.pOpcycles f₂ f₃ n₀),
    p_fromOpcycles_assoc, pOpcycles_δFromOpcycles,
    X.δ_naturality f₁ f₂ f₁ f₂₃ (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) n₀ n₁,
    Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Cycles (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₁
rw :
  X.pOpcycles f₂ f₃ n₀ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
    X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
rw₁ :
  (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
    X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
rw₂ : (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δ f₁ f₂ n₀ n₁ hn₁
rw₃ : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ (X.H n₁).map (𝟙 (mk₁ f₁)) = X.δ f₁ f₂ n₀ n₁ hn₁
rw₄ : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ 𝟙 ((X.H n₁).obj (mk₁ f₁)) = X.δ f₁ f₂ n₀ n₁ hn₁
⊢ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
have rw₅ : X.δ f₁ f₂ n₀ n₁ sorry = X.δ f₁ f₂ n₀ n₁ hn₁
Tactic: rw [← cancel_epi (X.pOpcycles f₂ f₃ n₀),
    p_fromOpcycles_assoc, pOpcycles_δFromOpcycles,
    X.δ_naturality f₁ f₂ f₁ f₂₃ (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) n₀ n₁,
    Functor.map_id, Category.comp_id]
-- 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₃₄
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₃ ≫ f₄) ⋯) ≫
      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
have rw : X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫
    (X.H n₂).map (𝟙 (mk₁ (f₁ ≫ f₂))) ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) sorry n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
  0
Tactic: rw [X.δ_naturality_assoc (f₁ ≫ f₂) f₃ (f₁ ≫ f₂) (f₃ ≫ f₄)
        (𝟙 _) (twoδ₂Toδ₁ f₃ f₄ _ rfl) n₁ n₂ rfl hn₂, Functor.map_id, id_comp,
        δ_toCycles_assoc .., δToCycles_πE ..]
-- 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₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫
      (X.H n₂).map (𝟙 (mk₁ (f₁ ≫ f₂))) ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0
⊢ (X.H n₁).map (twoδ₂Toδ₁ f₃ f₄ (f₃ ≫ f₄) ⋯) ≫
      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
have rw₁ : X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫
    𝟙 ((X.H n₂).obj (mk₁ (f₁ ≫ f₂))) ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) sorry n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
  0
Tactic: rw [X.δ_naturality_assoc (f₁ ≫ f₂) f₃ (f₁ ≫ f₂) (f₃ ≫ f₄)
        (𝟙 _) (twoδ₂Toδ₁ f₃ f₄ _ rfl) n₁ n₂ rfl hn₂, Functor.map_id, id_comp,
        δ_toCycles_assoc .., δToCycles_πE ..]
-- 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₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫
      (X.H n₂).map (𝟙 (mk₁ (f₁ ≫ f₂))) ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0
rw₁ :
  X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫
      𝟙 ((X.H n₂).obj (mk₁ (f₁ ≫ f₂))) ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0
⊢ (X.H n₁).map (twoδ₂Toδ₁ f₃ f₄ (f₃ ≫ f₄) ⋯) ≫
      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
have rw₂ : X.δ (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 [X.δ_naturality_assoc (f₁ ≫ f₂) f₃ (f₁ ≫ f₂) (f₃ ≫ f₄)
        (𝟙 _) (twoδ₂Toδ₁ f₃ f₄ _ rfl) n₁ n₂ rfl hn₂, Functor.map_id, id_comp,
        δ_toCycles_assoc .., δToCycles_πE ..]
-- 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₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫
      (X.H n₂).map (𝟙 (mk₁ (f₁ ≫ f₂))) ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0
rw₁ :
  X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫
      𝟙 ((X.H n₂).obj (mk₁ (f₁ ≫ f₂))) ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0
rw₂ : X.δ (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.H n₁).map (twoδ₂Toδ₁ f₃ f₄ (f₃ ≫ f₄) ⋯) ≫
      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
have rw₃ : X.δToCycles f₁ f₂ f₃ n₁ n₂ sorry ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ = 0
Tactic: rw [X.δ_naturality_assoc (f₁ ≫ f₂) f₃ (f₁ ≫ f₂) (f₃ ≫ f₄)
        (𝟙 _) (twoδ₂Toδ₁ f₃ f₄ _ rfl) n₁ n₂ rfl hn₂, Functor.map_id, id_comp,
        δ_toCycles_assoc .., δToCycles_πE ..]
-- 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₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫
      (X.H n₂).map (𝟙 (mk₁ (f₁ ≫ f₂))) ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0
rw₁ :
  X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫
      𝟙 ((X.H n₂).obj (mk₁ (f₁ ≫ f₂))) ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0
rw₂ : X.δ (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₃ : X.δToCycles f₁ f₂ f₃ n₁ n₂ ⋯ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ = 0
⊢ (X.H n₁).map (twoδ₂Toδ₁ f₃ f₄ (f₃ ≫ f₄) ⋯) ≫
      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
have rw₄ : Eq.{v_1 + 1} (α := (X.H n₁).obj (mk₁ f₃) ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) 0 0
Tactic: rw [X.δ_naturality_assoc (f₁ ≫ f₂) f₃ (f₁ ≫ f₂) (f₃ ≫ f₄)
        (𝟙 _) (twoδ₂Toδ₁ f₃ f₄ _ rfl) n₁ n₂ rfl hn₂, Functor.map_id, id_comp,
        δ_toCycles_assoc .., δToCycles_πE ..]
-- 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₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.δ (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
have rw : Eq (α := (X.H n₀).obj (mk₁ 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 [δ_δ_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₅ : ι
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₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  Eq (α := (X.H n₀).obj (mk₁ 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.δ (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
have rw₁ : Eq.{v_1 + 1} (α := (X.H n₀).obj (mk₁ f₅) ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) 0 0
Tactic: rw [δ_δ_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₅ : ι
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₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.toCycles f₃ f₄ f₃₄ h₃₄ 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.δ f₁₂ f₃₄ n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃
have subst : 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.δ (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₃
Tactic: subst h₁₂ h₃₄
Cleared hypotheses: f₁₂, h₁₂, f₃₄, h₃₄