awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso (X := (mk₁ f).obj 0) (φ.app 0) ∧ IsIso (X := (mk₁ f).obj 1) (φ.app 1)
have left : IsIso (X := (mk₁ f).obj 0) (φ.app 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
left : IsIso (X := (mk₁ f).obj 0) (φ.app 0)
⊢ IsIso (X := (mk₁ f).obj 0) (φ.app 0) ∧ IsIso (X := (mk₁ f).obj 1) (φ.app 1)
have right : IsIso (X := (mk₁ f).obj 1) (φ.app 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso (X := (mk₁ f).obj 0) (φ.app 0)
have left : IsIso (𝟙 i₀ ≫ f)
Tactic: dsimp [φ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso (X := (mk₁ f).obj 1) (φ.app 1)
have right : IsIso (inv f ≫ 𝟙 i₀)
Tactic: dsimp [φ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsZero.{u_4, u_1} ((X.H n).obj (mk₁ f))
have this : IsIso φ
Tactic: have : IsIso φ := by
    rw [isIso_iff₁]
    constructor <;> dsimp [φ] <;> infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
⊢ IsZero.{u_4, u_1} ((X.H n).obj (mk₁ f))
have rw : Eq.{u_4 + 1} (α := (X.H n).obj (mk₁ f) ⟶ (X.H n).obj (mk₁ f)) (𝟙 ((X.H n).obj (mk₁ f))) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
⊢ Eq.{u_4 + 1} (α := (X.H n).obj (mk₁ f) ⟶ (X.H n).obj (mk₁ f)) (𝟙 ((X.H n).obj (mk₁ f))) 0
have rw : 𝟙 ((X.H n).obj (mk₁ f)) ≫ (X.H n).map φ = 0 ≫ (X.H n).map φ
Tactic: rw [← cancel_mono ((X.H n).map φ), Category.id_comp, zero_comp,
    ← X.zero₂ f (inv f) (𝟙 _) (by simp), ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
rw : 𝟙 ((X.H n).obj (mk₁ f)) ≫ (X.H n).map φ = 0 ≫ (X.H n).map φ
⊢ Eq.{u_4 + 1} (α := (X.H n).obj (mk₁ f) ⟶ (X.H n).obj (mk₁ f)) (𝟙 ((X.H n).obj (mk₁ f))) 0
have rw₁ : (X.H n).map φ = 0 ≫ (X.H n).map φ
Tactic: rw [← cancel_mono ((X.H n).map φ), Category.id_comp, zero_comp,
    ← X.zero₂ f (inv f) (𝟙 _) (by simp), ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
rw : 𝟙 ((X.H n).obj (mk₁ f)) ≫ (X.H n).map φ = 0 ≫ (X.H n).map φ
rw₁ : (X.H n).map φ = 0 ≫ (X.H n).map φ
⊢ Eq.{u_4 + 1} (α := (X.H n).obj (mk₁ f) ⟶ (X.H n).obj (mk₁ f)) (𝟙 ((X.H n).obj (mk₁ f))) 0
have rw₂ : (X.H n).map φ = 0
Tactic: rw [← cancel_mono ((X.H n).map φ), Category.id_comp, zero_comp,
    ← X.zero₂ f (inv f) (𝟙 _) (by simp), ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
rw : 𝟙 ((X.H n).obj (mk₁ f)) ≫ (X.H n).map φ = 0 ≫ (X.H n).map φ
rw₁ : (X.H n).map φ = 0 ≫ (X.H n).map φ
rw₂ : (X.H n).map φ = 0
⊢ Eq.{u_4 + 1} (α := (X.H n).obj (mk₁ f) ⟶ (X.H n).obj (mk₁ f)) (𝟙 ((X.H n).obj (mk₁ f))) 0
have rw₃ : (X.H n).map φ = (X.H n).map (twoδ₂Toδ₁ f (inv f) (𝟙 i₀) sorry) ≫ (X.H n).map (twoδ₁Toδ₀ f (inv f) (𝟙 i₀) sorry)
Tactic: rw [← cancel_mono ((X.H n).map φ), Category.id_comp, zero_comp,
    ← X.zero₂ f (inv f) (𝟙 _) (by simp), ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} ι
inst_2 : Abelian.{u_4, u_1} C
X : SpectralObject.{u_1, u_2, u_4, u_3} C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst_3 : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
rw : 𝟙 ((X.H n).obj (mk₁ f)) ≫ (X.H n).map φ = 0 ≫ (X.H n).map φ
rw₁ : (X.H n).map φ = 0 ≫ (X.H n).map φ
rw₂ : (X.H n).map φ = 0
rw₃ : (X.H n).map φ = (X.H n).map (twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯) ≫ (X.H n).map (twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯)
⊢ Eq.{u_4 + 1} (α := (X.H n).obj (mk₁ f) ⟶ (X.H n).obj (mk₁ f)) (𝟙 ((X.H n).obj (mk₁ f))) 0
have rw₄ : (X.H n).map φ = (X.H n).map (twoδ₂Toδ₁ f (inv f) (𝟙 i₀) sorry ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) sorry)
Tactic: rw [← cancel_mono ((X.H n).map φ), Category.id_comp, zero_comp,
    ← X.zero₂ f (inv f) (𝟙 _) (by simp), ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι
f : i₀ ⟶ i₁
g : i₁ ⟶ i₂
fg : i₀ ⟶ i₂
hfg : f ≫ g = fg
h₁ : IsZero.{u_3, u_1} ((X.H n₀).obj (mk₁ f))
h₂ : IsZero.{u_3, u_1} ((X.H n₁).obj (mk₁ f))
⊢ IsIso ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
have this : Mono ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
Tactic: have := X.mono_H_map_twoδ₁Toδ₀ n₀ f g fg hfg h₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Basic (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} ι
inst_2 : Abelian.{u_3, u_1} C
X : SpectralObject.{u_1, u_2, u_3, u_4} C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι
f : i₀ ⟶ i₁
g : i₁ ⟶ i₂
fg : i₀ ⟶ i₂
hfg : f ≫ g = fg
h₁ : IsZero.{u_3, u_1} ((X.H n₀).obj (mk₁ f))
h₂ : IsZero.{u_3, u_1} ((X.H n₁).obj (mk₁ f))
this : Mono ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
⊢ IsIso ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
have this₁ : Epi ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
Tactic: have := X.epi_H_map_twoδ₁Toδ₀ n₀ n₁ hn₁ f g fg hfg h₂
-- 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 : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
h : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ f))
⊢ IsZero.{v_1, u_1} (X.opcycles f g n)
have rw : X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n) = X.pOpcycles f g n ≫ 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi (X.pOpcycles ..)]
-- 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 : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
h : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ g))
⊢ IsZero.{v_1, u_1} (X.cycles f g n)
have rw : 𝟙 (X.cycles f g n) ≫ X.iCycles f g n = 0 ≫ X.iCycles f g n
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_mono (X.iCycles ..)]
-- 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 : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.iCycles f g n₀ ≫ X.δ f g n₀ n₁ hn₁ = 0
have subst : X.iCycles f g n₀ ≫ X.δ f g n₀ (n₀ + 1) sorry = 0
Tactic: subst hn₁
Cleared hypotheses: n₁, hn₁
-- 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 : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f g n₀ n₁ hn₁ ≫ X.pOpcycles f g n₁ = 0
have obtain : ∀ (hn₁ : n₁ - 1 + 1 = n₁), X.δ f g (n₁ - 1) n₁ hn₁ ≫ X.pOpcycles f g n₁ = 0
Tactic: obtain rfl : n₀ = n₁ - 1 := by lia
Cleared hypotheses: n₀, hn₁
-- 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 : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ Mono (X.kernelSequenceCycles f g n₀ n₁ hn₁).f
have dsimp : Mono (X.iCycles f g n₀)
Tactic: dsimp
-- 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 : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ Epi (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).g
have dsimp : Epi (X.pOpcycles f g n₁)
Tactic: dsimp
-- 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 : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.kernelSequenceCycles f g n₀ n₁ hn₁).Exact
have subst : (X.kernelSequenceCycles f g n₀ (n₀ + 1) sorry).Exact
Tactic: subst hn₁
Cleared hypotheses: n₁, hn₁
-- 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 : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).Exact
have obtain : ∀ (hn₁ : n₁ - 1 + 1 = n₁), (X.cokernelSequenceOpcycles f g (n₁ - 1) n₁ hn₁).Exact
Tactic: obtain rfl : n₀ = n₁ - 1 := by lia
Cleared hypotheses: n₀, hn₁
-- 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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
x : (X.H n₁).obj (mk₁ f) ⟶ A
hx : X.δ f g n₀ n₁ hn₁ ≫ x = 0
⊢ X.δ f g (n₁ - 1) n₁ ⋯ ≫ x = 0
have hn₂ : n₁ - 1 + 1 = n₁
Tactic: obtain rfl : n₀ = n₁ -1 := by lia
Cleared hypotheses: n₀, hn₁, hx
-- 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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ (X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯)) ≫ X.δ f' g' n (n + 1) ⋯ = 0
have rw : X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) sorry) ≫ X.δ f' g' n (n + 1) sorry = 0
Tactic: rw [Category.assoc, X.δ_naturality f g f' g'
        (homMk₁ (α.app 0) (α.app 1) (naturality' α 0 1))
          (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2)) n (n + 1),
        iCycles_δ_assoc _ _ _ _ _, zero_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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
rw : X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯) ≫ X.δ f' g' n (n + 1) ⋯ = 0
⊢ (X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯)) ≫ X.δ f' g' n (n + 1) ⋯ = 0
have rw₁ : Eq (α := X.cycles f g n ⟶ (X.H (n + 1)).obj (mk₁ f'))
  (X.iCycles f g n ≫ X.δ f g n (n + 1) sorry ≫ (X.H (n + 1)).map (homMk₁ (α.app 0) (α.app 1) sorry)) 0
Tactic: rw [Category.assoc, X.δ_naturality f g f' g'
        (homMk₁ (α.app 0) (α.app 1) (naturality' α 0 1))
          (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2)) n (n + 1),
        iCycles_δ_assoc _ _ _ _ _, zero_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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
rw : X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯) ≫ X.δ f' g' n (n + 1) ⋯ = 0
rw₁ :
  Eq (α := X.cycles f g n ⟶ (X.H (n + 1)).obj (mk₁ f'))
    (X.iCycles f g n ≫ X.δ f g n (n + 1) ⋯ ≫ (X.H (n + 1)).map (homMk₁ (α.app 0) (α.app 1) ⋯)) 0
⊢ (X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯)) ≫ X.δ f' g' n (n + 1) ⋯ = 0
have rw₂ : Eq (α := X.cycles f g n ⟶ (X.H (n + 1)).obj (mk₁ f'))
  (CategoryStruct.comp (Y := (X.H (n + 1)).obj (mk₁ f)) 0 ((X.H (n + 1)).map (homMk₁ (α.app 0) (α.app 1) sorry))) 0
Tactic: rw [Category.assoc, X.δ_naturality f g f' g'
        (homMk₁ (α.app 0) (α.app 1) (naturality' α 0 1))
          (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2)) n (n + 1),
        iCycles_δ_assoc _ _ _ _ _, zero_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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
rw : X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯) ≫ X.δ f' g' n (n + 1) ⋯ = 0
rw₁ :
  Eq (α := X.cycles f g n ⟶ (X.H (n + 1)).obj (mk₁ f'))
    (X.iCycles f g n ≫ X.δ f g n (n + 1) ⋯ ≫ (X.H (n + 1)).map (homMk₁ (α.app 0) (α.app 1) ⋯)) 0
rw₂ :
  Eq (α := X.cycles f g n ⟶ (X.H (n + 1)).obj (mk₁ f'))
    (CategoryStruct.comp (Y := (X.H (n + 1)).obj (mk₁ f)) 0 ((X.H (n + 1)).map (homMk₁ (α.app 0) (α.app 1) ⋯))) 0
⊢ (X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯)) ≫ X.δ f' g' n (n + 1) ⋯ = 0
have rw₃ : Eq.{v_1 + 1} (α := X.cycles f g n ⟶ (X.H (n + 1)).obj (mk₁ f')) 0 0
Tactic: rw [Category.assoc, X.δ_naturality f g f' g'
        (homMk₁ (α.app 0) (α.app 1) (naturality' α 0 1))
          (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2)) n (n + 1),
        iCycles_δ_assoc _ _ _ _ _, zero_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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ g ⟶ mk₁ g'
n : ℤ
hβ : β = homMk₁ (α.app 1) (α.app 2) ⋯
⊢ X.cyclesMap f g f' g' α n ≫ X.iCycles f' g' n = X.iCycles f g n ≫ (X.H n).map β
have subst : X.cyclesMap f g f' g' α n ≫ X.iCycles f' g' n = X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) sorry)
Tactic: subst hβ
Cleared hypotheses: β, hβ
-- 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 : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
⊢ X.cyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.cycles f g n)
have rw : X.cyclesMap f g f g (𝟙 (mk₂ f g)) n ≫ X.iCycles f g n = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
Tactic: rw [← cancel_mono (X.iCycles f g n), X.cyclesMap_i f g f g (𝟙 _) (𝟙 _) n,
    Functor.map_id, Category.comp_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 : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
rw : X.cyclesMap f g f g (𝟙 (mk₂ f g)) n ≫ X.iCycles f g n = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
⊢ X.cyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.cycles f g n)
have rw₁ : X.iCycles f g n ≫ (X.H n).map (𝟙 (mk₁ g)) = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
Tactic: rw [← cancel_mono (X.iCycles f g n), X.cyclesMap_i f g f g (𝟙 _) (𝟙 _) n,
    Functor.map_id, Category.comp_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 : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
rw : X.cyclesMap f g f g (𝟙 (mk₂ f g)) n ≫ X.iCycles f g n = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
rw₁ : X.iCycles f g n ≫ (X.H n).map (𝟙 (mk₁ g)) = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
⊢ X.cyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.cycles f g n)
have rw₂ : X.iCycles f g n ≫ 𝟙 ((X.H n).obj (mk₁ g)) = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
Tactic: rw [← cancel_mono (X.iCycles f g n), X.cyclesMap_i f g f g (𝟙 _) (𝟙 _) n,
    Functor.map_id, Category.comp_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 : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
rw : X.cyclesMap f g f g (𝟙 (mk₂ f g)) n ≫ X.iCycles f g n = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
rw₁ : X.iCycles f g n ≫ (X.H n).map (𝟙 (mk₁ g)) = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
rw₂ : X.iCycles f g n ≫ 𝟙 ((X.H n).obj (mk₁ g)) = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
⊢ X.cyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.cycles f g n)
have rw₃ : X.iCycles f g n = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
Tactic: rw [← cancel_mono (X.iCycles f g n), X.cyclesMap_i f g f g (𝟙 _) (𝟙 _) n,
    Functor.map_id, Category.comp_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 : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
rw : X.cyclesMap f g f g (𝟙 (mk₂ f g)) n ≫ X.iCycles f g n = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
rw₁ : X.iCycles f g n ≫ (X.H n).map (𝟙 (mk₁ g)) = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
rw₂ : X.iCycles f g n ≫ 𝟙 ((X.H n).obj (mk₁ g)) = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
rw₃ : X.iCycles f g n = 𝟙 (X.cycles f g n) ≫ X.iCycles f g n
⊢ X.cyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.cycles f g n)
have rw₄ : X.iCycles f g n = X.iCycles f g n
Tactic: rw [← cancel_mono (X.iCycles f g n), X.cyclesMap_i f g f g (𝟙 _) (𝟙 _) n,
    Functor.map_id, Category.comp_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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
α'' : mk₂ f g ⟶ mk₂ f'' g''
n : ℤ
h : α ≫ α' = α''
⊢ X.cyclesMap f g f' g' α n ≫ X.cyclesMap f' g' f'' g'' α' n = X.cyclesMap f g f'' g'' α'' n
have subst : X.cyclesMap f g f' g' α n ≫ X.cyclesMap f' g' f'' g'' α' n = X.cyclesMap f g f'' g'' (α ≫ α') n
Tactic: subst h
Cleared hypotheses: α'', h
-- 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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
n : ℤ
⊢ X.cyclesMap f g f' g' α n ≫ X.cyclesMap f' g' f'' g'' α' n = X.cyclesMap f g f'' g'' (α ≫ α') n
have rw : X.iCycles f g n ≫
    (X.H n).map (CategoryStruct.comp (Y := mk₁ g') (homMk₁ (α.app 1) (α.app 2) sorry) (homMk₁ (α'.app 1) (α'.app 2) sorry)) =
  X.cyclesMap f g f'' g'' (α ≫ α') n ≫ X.iCycles f'' g'' n
Tactic: rw [← cancel_mono (X.iCycles f'' g'' n), Category.assoc,
    X.cyclesMap_i f' g' f'' g'' α' _ n rfl,
    X.cyclesMap_i_assoc f g f' g' α _ n rfl,
    ← Functor.map_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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ X.δ f g (n - 1) n ⋯ ≫ (X.H n).map (homMk₁ (α.app 0) (α.app 1) ⋯) ≫ X.pOpcycles f' g' n = 0
have rw : Eq (α := (X.H (n - 1)).obj (mk₁ g) ⟶ X.opcycles f' g' n)
  ((X.H (n - 1)).map (homMk₁ (α.app 1) (α.app 2) sorry) ≫ X.δ f' g' (n - 1) n sorry ≫ X.pOpcycles f' g' n) 0
Tactic: rw [← X.δ_naturality_assoc f g f' g'
        (homMk₁ (α.app 0) (α.app 1) (naturality' α 0 1))
        (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2)) _ _,
        δ_pOpcycles _ _ _ _ _, comp_zero]