awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  Eq (α := (X.H (n - 1)).obj (mk₁ g) ⟶ X.opcycles f' g' n)
    ((X.H (n - 1)).map (homMk₁ (α.app 1) (α.app 2) ⋯) ≫ X.δ f' g' (n - 1) n ⋯ ≫ X.pOpcycles f' g' n) 0
⊢ 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)
  (CategoryStruct.comp (Y := (X.H (n - 1)).obj (mk₁ g')) ((X.H (n - 1)).map (homMk₁ (α.app 1) (α.app 2) sorry)) 0) 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]
-- 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 :
  Eq (α := (X.H (n - 1)).obj (mk₁ g) ⟶ X.opcycles f' g' n)
    ((X.H (n - 1)).map (homMk₁ (α.app 1) (α.app 2) ⋯) ≫ X.δ f' g' (n - 1) n ⋯ ≫ X.pOpcycles f' g' n) 0
rw₁ :
  Eq (α := (X.H (n - 1)).obj (mk₁ g) ⟶ X.opcycles f' g' n)
    (CategoryStruct.comp (Y := (X.H (n - 1)).obj (mk₁ g')) ((X.H (n - 1)).map (homMk₁ (α.app 1) (α.app 2) ⋯)) 0) 0
⊢ X.δ f g (n - 1) n ⋯ ≫ (X.H n).map (homMk₁ (α.app 0) (α.app 1) ⋯) ≫ X.pOpcycles f' g' n = 0
have rw₂ : Eq.{v_1 + 1} (α := (X.H (n - 1)).obj (mk₁ g) ⟶ X.opcycles f' g' n) 0 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]
-- 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₁ f ⟶ mk₁ f'
n : ℤ
hβ : β = homMk₁ (α.app 0) (α.app 1) ⋯
⊢ X.pOpcycles f g n ≫ X.opcyclesMap f g f' g' α n = (X.H n).map β ≫ X.pOpcycles f' g' n
have subst : X.pOpcycles f g n ≫ X.opcyclesMap f g f' g' α n = (X.H n).map (homMk₁ (α.app 0) (α.app 1) sorry) ≫ X.pOpcycles 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
n : ℤ
⊢ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.opcycles f g n)
have rw : X.pOpcycles f g n ≫ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
Tactic: rw [← cancel_epi (X.pOpcycles f g n),
    X.p_opcyclesMap f g f g (𝟙 _) (𝟙 _),
    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.pOpcycles f g n ≫ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
⊢ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.opcycles f g n)
have rw₁ : (X.H n).map (𝟙 (mk₁ f)) ≫ X.pOpcycles f g n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
Tactic: rw [← cancel_epi (X.pOpcycles f g n),
    X.p_opcyclesMap f g f g (𝟙 _) (𝟙 _),
    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.pOpcycles f g n ≫ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
rw₁ : (X.H n).map (𝟙 (mk₁ f)) ≫ X.pOpcycles f g n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
⊢ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.opcycles f g n)
have rw₂ : 𝟙 ((X.H n).obj (mk₁ f)) ≫ X.pOpcycles f g n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
Tactic: rw [← cancel_epi (X.pOpcycles f g n),
    X.p_opcyclesMap f g f g (𝟙 _) (𝟙 _),
    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.pOpcycles f g n ≫ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
rw₁ : (X.H n).map (𝟙 (mk₁ f)) ≫ X.pOpcycles f g n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
rw₂ : 𝟙 ((X.H n).obj (mk₁ f)) ≫ X.pOpcycles f g n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
⊢ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.opcycles f g n)
have rw₃ : 𝟙 ((X.H n).obj (mk₁ f)) ≫ X.pOpcycles f g n = X.pOpcycles f g n
Tactic: rw [← cancel_epi (X.pOpcycles f g n),
    X.p_opcyclesMap f g f g (𝟙 _) (𝟙 _),
    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.pOpcycles f g n ≫ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
rw₁ : (X.H n).map (𝟙 (mk₁ f)) ≫ X.pOpcycles f g n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
rw₂ : 𝟙 ((X.H n).obj (mk₁ f)) ≫ X.pOpcycles f g n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
rw₃ : 𝟙 ((X.H n).obj (mk₁ f)) ≫ X.pOpcycles f g n = X.pOpcycles f g n
⊢ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.opcycles f g n)
have rw₄ : X.pOpcycles f g n = X.pOpcycles f g n
Tactic: rw [← cancel_epi (X.pOpcycles f g n),
    X.p_opcyclesMap f g f g (𝟙 _) (𝟙 _),
    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.opcyclesMap f g f' g' α n ≫ X.opcyclesMap f' g' f'' g'' α' n = X.opcyclesMap f g f'' g'' α'' n
have subst : X.opcyclesMap f g f' g' α n ≫ X.opcyclesMap f' g' f'' g'' α' n = X.opcyclesMap 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.opcyclesMap f g f' g' α n ≫ X.opcyclesMap f' g' f'' g'' α' n = X.opcyclesMap f g f'' g'' (α ≫ α') n
have rw : (X.H n).map (CategoryStruct.comp (Y := mk₁ f') (homMk₁ (α.app 0) (α.app 1) sorry) (homMk₁ (α'.app 0) (α'.app 1) sorry)) ≫
    X.pOpcycles f'' g'' n =
  X.pOpcycles f g n ≫ X.opcyclesMap f g f'' g'' (α ≫ α') n
Tactic: rw [← cancel_epi (X.pOpcycles f g n),
    X.p_opcyclesMap_assoc f g f' g' α _,
    X.p_opcyclesMap f' g' f'' g'' α' _,
    ← Functor.map_comp_assoc]
-- 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ X.toCycles f g fg h n ≫ X.cyclesMap f g f' g' α n = (X.H n).map β ≫ X.toCycles f' g' fg' h' n
have rw : (X.H n).map (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) sorry) = (X.H n).map (β ≫ twoδ₁Toδ₀ f' g' fg' h')
Tactic: rw [← cancel_mono (X.iCycles f' g' n), Category.assoc, Category.assoc, toCycles_i,
    X.cyclesMap_i f g f' g' α (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2)) n rfl,
    toCycles_i_assoc, ← Functor.map_comp, ← 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ (X.H n).map (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯) = (X.H n).map (β ≫ twoδ₁Toδ₀ f' g' fg' h')
have e_a : twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) sorry = β ≫ twoδ₁Toδ₀ f' g' fg' h'
Tactic: congr 1
-- 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯ = β ≫ twoδ₁Toδ₀ f' g' fg' h'
have e_a : app' (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) sorry) 0 homMk₁._proof_4 =
  app' (β ≫ twoδ₁Toδ₀ f' g' fg' h') 0 homMk₁._proof_4
Tactic: ext
-- 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
e_a :
  app' (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯) 0 homMk₁._proof_4 =
    app' (β ≫ twoδ₁Toδ₀ f' g' fg' h') 0 homMk₁._proof_4
⊢ twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯ = β ≫ twoδ₁Toδ₀ f' g' fg' h'
have e_a₁ : app' (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) sorry) 1 homMk₁._proof_5 =
  app' (β ≫ twoδ₁Toδ₀ f' g' fg' h') 1 homMk₁._proof_5
Tactic: ext
-- 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ app' (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯) 0 homMk₁._proof_4 =
    app' (β ≫ twoδ₁Toδ₀ f' g' fg' h') 0 homMk₁._proof_4
have e_a : Eq (α := i ⟶ j') (f ≫ α.app 1) (β.app 0 ≫ f')
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
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ Eq (α := i ⟶ j') (f ≫ α.app 1) (β.app 0 ≫ f')
have e_a : Eq (α := i ⟶ j') (f ≫ α.app 1) (α.app 0 ≫ f')
Tactic: rw [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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ app' (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯) 1 homMk₁._proof_5 =
    app' (β ≫ twoδ₁Toδ₀ f' g' fg' h') 1 homMk₁._proof_5
have e_a : Eq.{v_2 + 1} (α := k ⟶ k') (𝟙 k ≫ α.app 2) (β.app 1 ≫ 𝟙 k')
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
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ Eq.{v_2 + 1} (α := k ⟶ k') (𝟙 k ≫ α.app 2) (β.app 1 ≫ 𝟙 k')
have e_a : Eq.{v_2 + 1} (α := k ⟶ k') (𝟙 k ≫ α.app 2) (α.app 2 ≫ 𝟙 k')
Tactic: rw [hβ₁, 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
e_a : Eq.{v_2 + 1} (α := k ⟶ k') (𝟙 k ≫ α.app 2) (α.app 2 ≫ 𝟙 k')
⊢ Eq.{v_2 + 1} (α := k ⟶ k') (𝟙 k ≫ α.app 2) (β.app 1 ≫ 𝟙 k')
have e_a₁ : Eq.{v_2 + 1} (α := k ⟶ k') (𝟙 k ≫ α.app 2) (α.app 2)
Tactic: rw [hβ₁, 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
e_a : Eq.{v_2 + 1} (α := k ⟶ k') (𝟙 k ≫ α.app 2) (α.app 2 ≫ 𝟙 k')
e_a₁ : Eq.{v_2 + 1} (α := k ⟶ k') (𝟙 k ≫ α.app 2) (α.app 2)
⊢ Eq.{v_2 + 1} (α := k ⟶ k') (𝟙 k ≫ α.app 2) (β.app 1 ≫ 𝟙 k')
have e_a₂ : Eq (α := k ⟶ k') (α.app 2 : (mk₂ f g).obj 2 ⟶ (mk₂ f' g').obj 2) (α.app 2)
Tactic: rw [hβ₁, 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ X.opcyclesMap f g f' g' α n ≫ X.fromOpcycles f' g' fg' h' n = X.fromOpcycles f g fg h n ≫ (X.H n).map β
have rw : (X.H n).map (homMk₁ (α.app 0) (α.app 1) sorry ≫ twoδ₂Toδ₁ f' g' fg' h') = (X.H n).map (twoδ₂Toδ₁ f g fg h ≫ β)
Tactic: rw [← cancel_epi (X.pOpcycles f g n), p_fromOpcycles_assoc,
    X.p_opcyclesMap_assoc f g f' g' α (homMk₁ (α.app 0) (α.app 1)
      (naturality' α 0 1)) n rfl,
    p_fromOpcycles, ← Functor.map_comp, ← 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ (X.H n).map (homMk₁ (α.app 0) (α.app 1) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h') = (X.H n).map (twoδ₂Toδ₁ f g fg h ≫ β)
have e_a : homMk₁ (α.app 0) (α.app 1) sorry ≫ twoδ₂Toδ₁ f' g' fg' h' = twoδ₂Toδ₁ f g fg h ≫ β
Tactic: congr 1
-- 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ homMk₁ (α.app 0) (α.app 1) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h' = twoδ₂Toδ₁ f g fg h ≫ β
have e_a : app' (homMk₁ (α.app 0) (α.app 1) sorry ≫ twoδ₂Toδ₁ f' g' fg' h') 0 homMk₁._proof_4 =
  app' (twoδ₂Toδ₁ f g fg h ≫ β) 0 homMk₁._proof_4
Tactic: ext
-- 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
e_a :
  app' (homMk₁ (α.app 0) (α.app 1) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h') 0 homMk₁._proof_4 =
    app' (twoδ₂Toδ₁ f g fg h ≫ β) 0 homMk₁._proof_4
⊢ homMk₁ (α.app 0) (α.app 1) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h' = twoδ₂Toδ₁ f g fg h ≫ β
have e_a₁ : app' (homMk₁ (α.app 0) (α.app 1) sorry ≫ twoδ₂Toδ₁ f' g' fg' h') 1 homMk₁._proof_5 =
  app' (twoδ₂Toδ₁ f g fg h ≫ β) 1 homMk₁._proof_5
Tactic: ext
-- 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'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ app' (homMk₁ (α.app 0) (α.app 1) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h') 1 homMk₁._proof_5 =
    app' (twoδ₂Toδ₁ f g fg h ≫ β) 1 homMk₁._proof_5
have e_a : Eq (α := j ⟶ k') (α.app 1 ≫ g' : j ⟶ k') (g ≫ β.app 1 : j ⟶ k')
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
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : Eq (α := (mk₁ fg).obj 0 ⟶ (mk₁ fg').obj 0) (β.app 0) (α.app 0)
hβ₁ : Eq (α := (mk₁ fg).obj 1 ⟶ (mk₁ fg').obj 1) (β.app 1) (α.app 2)
⊢ Eq (α := j ⟶ k') (α.app 1 ≫ g' : j ⟶ k') (g ≫ β.app 1 : j ⟶ k')
have e_a : Eq (α := j ⟶ k') (α.app 1 ≫ g' : j ⟶ k') (g ≫ α.app 2 : j ⟶ k')
Tactic: rw [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''
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
n : ℤ
⊢ Epi (X.cokernelSequenceCycles f g fg h n).g
have dsimp : Epi (X.toCycles f g fg h 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
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
n : ℤ
⊢ Mono (X.kernelSequenceOpcycles f g fg h n).f
have dsimp : Mono (X.fromOpcycles f g fg h 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
fg : i ⟶ k
h : f ≫ g = fg
n : ℤ
⊢ (X.cokernelSequenceCycles f g fg h n).Exact
have hS : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceCycles f g fg h n).g sorry)
Tactic: apply ShortComplex.exact_of_g_is_cokernel
-- 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
fg : i ⟶ k
h : f ≫ g = fg
n : ℤ
⊢ (X.kernelSequenceOpcycles f g fg h n).Exact
have hS : IsLimit (KernelFork.ofι (X.kernelSequenceOpcycles f g fg h n).f sorry)
Tactic: apply ShortComplex.exact_of_f_is_kernel
-- 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 : ℤ
hf : IsZero.{v_1, u_1} ((X.H n).obj (mk₁ f))
⊢ IsIso (X.toCycles f g fg h n)
have this : Mono (X.toCycles f g fg h n)
Tactic: have : Mono (X.toCycles f g fg h n) :=
    (X.cokernelSequenceCycles_exact f g fg h n).mono_g (hf.eq_of_src _ _)