awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 (α := i ⟶ j') (f ≫ α.app 1) (β.app 0 ≫ f')
⊢ 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

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 (α := i ⟶ j') (f ≫ α.app 1) (α.app 0 ≫ f')
⊢ Eq (α := i ⟶ j') (f ≫ α.app 1) (β.app 0 ≫ f')

Tactic:
rw [hβ₀]
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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')

Tactic:
naturality' α 0 1

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, Fin.ofNat, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.naturality', OfNat.ofNat, CategoryTheory.ComposableArrows.Precomp.map
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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')

Tactic:
exact naturality' α 0 1

Premises used: CategoryTheory.ComposableArrows.naturality', OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 1 ≫ 𝟙 k')
⊢ 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

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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)
e_a₂ e_a₃ : Eq (α := k ⟶ k') (α.app 2 : (mk₂ f g).obj 2 ⟶ (mk₂ f' g').obj 2) (α.app 2)
⊢ Eq.{v_2 + 1} (α := k ⟶ k') (𝟙 k ≫ α.app 2) (β.app 1 ≫ 𝟙 k')

Tactic:
rw [hβ₁, Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 : ℤ
⊢ X.δ f g (n - 1) n ⋯ ≫ (X.H n).map (twoδ₂Toδ₁ f g fg h) = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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.fromOpcycles f g fg h n)

Tactic:
(ShortComplex.exact_iff_mono_cokernel_desc _).1 (X.exact₁ f g fg h (n - 1) n)

Premises used: HSub.hSub, CategoryTheory.Abelian.SpectralObject.fromOpcycles, CategoryTheory.Abelian.SpectralObject.opcycles, CategoryTheory.ShortComplex.exact_iff_mono_cokernel_desc, Iff.mp, CategoryTheory.Abelian.SpectralObject.δ, OfNat.ofNat, CategoryTheory.Abelian.SpectralObject.exact₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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.pOpcycles f g n ≫ X.fromOpcycles f g fg h n = (X.H n).map (twoδ₂Toδ₁ f g fg h)

Tactic:
cokernel.π_desc ..

Premises used: CategoryTheory.Abelian.SpectralObject.fromOpcycles, CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Abelian.SpectralObject.opcycles, CategoryTheory.Abelian.SpectralObject.pOpcycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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)
rw : (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 ≫ β)
⊢ 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 β

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]

Premises used: CategoryTheory.Abelian.SpectralObject.p_fromOpcycles_assoc, CategoryTheory.ComposableArrows.naturality', CategoryTheory.Abelian.SpectralObject.p_opcyclesMap_assoc, CategoryTheory.Abelian.SpectralObject.p_fromOpcycles, CategoryTheory.ComposableArrows.homMk₁, CategoryTheory.Functor.map_comp, OfNat.ofNat, CategoryTheory.cancel_epi, CategoryTheory.NatTrans.app, rfl, CategoryTheory.Abelian.SpectralObject.pOpcycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 : homMk₁ (α.app 0) (α.app 1) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h' = twoδ₂Toδ₁ f g fg h ≫ β
⊢ (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 ≫ β)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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
e_a₁ :
  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
⊢ homMk₁ (α.app 0) (α.app 1) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h' = twoδ₂Toδ₁ f g fg h ≫ β

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 (α := j ⟶ k') (α.app 1 ≫ g' : j ⟶ k') (g ≫ β.app 1 : j ⟶ k')
⊢ 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

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 (α := j ⟶ k') (α.app 1 ≫ g' : j ⟶ k') (g ≫ α.app 2 : j ⟶ k')
⊢ Eq (α := j ⟶ k') (α.app 1 ≫ g' : j ⟶ k') (g ≫ β.app 1 : j ⟶ k')

Tactic:
rw [hβ₁]
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 2 : j ⟶ k')

Tactic:
(naturality' α 1 2).symm

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, Fin.ofNat, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.naturality', CategoryTheory.ComposableArrows.Mk₁.map, OfNat.ofNat, Eq.symm, CategoryTheory.ComposableArrows.Precomp.map
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 2 : j ⟶ k')

Tactic:
exact (naturality' α 1 2).symm

Premises used: CategoryTheory.ComposableArrows.naturality', OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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.H n).map (twoδ₂Toδ₁ f g fg h) ≫ X.toCycles f g fg h n = 0

Tactic:
simp [← cancel_mono (X.iCycles f g n)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Abelian.SpectralObject.iCycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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.fromOpcycles f g fg h n ≫ (X.H n).map (twoδ₁Toδ₀ f g fg h) = 0

Tactic:
simp [← cancel_epi (X.pOpcycles f g n)]

Premises used: CategoryTheory.cancel_epi, CategoryTheory.Abelian.SpectralObject.pOpcycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 : ℤ
dsimp : Epi (X.toCycles f g fg h n)
⊢ Epi (X.cokernelSequenceCycles f g fg h n).g

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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.toCycles f g fg h n)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 : ℤ
dsimp : Mono (X.fromOpcycles f g fg h n)
⊢ Mono (X.kernelSequenceOpcycles f g fg h n).f

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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.fromOpcycles f g fg h n)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 : ℤ
hS : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceCycles f g fg h n).g ⋯)
⊢ (X.cokernelSequenceCycles f g fg h n).Exact

Tactic:
apply ShortComplex.exact_of_g_is_cokernel

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 : ℤ
⊢ Cofork.π
        (Cofork.ofπ (P := cokernel (X.cokernelSequenceCycles f g fg h n).f)
          (cokernel.π (X.cokernelSequenceCycles f g fg h n).f) ⋯) ≫
      (X.cokernelIsoCycles f g fg h n).hom =
    Cofork.π (CokernelCofork.ofπ (X.cokernelSequenceCycles f g fg h n).g ⋯)

Tactic:
simp [← cancel_mono (X.iCycles f g n)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Abelian.SpectralObject.iCycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 : ℤ
⊢ IsColimit (CokernelCofork.ofπ (X.cokernelSequenceCycles f g fg h n).g ⋯)

Tactic:
exact IsColimit.ofIsoColimit (cokernelIsCokernel _)
    (Cofork.ext (X.cokernelIsoCycles f g fg h n) (by
      simp [← cancel_mono (X.iCycles f g n)]))
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 : ℤ
hS : IsLimit (KernelFork.ofι (X.kernelSequenceOpcycles f g fg h n).f ⋯)
⊢ (X.kernelSequenceOpcycles f g fg h n).Exact

Tactic:
apply ShortComplex.exact_of_f_is_kernel

Premises used: CategoryTheory.ShortComplex.exact_of_f_is_kernel
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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.opcyclesIsoKernel f g fg h n).hom ≫
      Fork.ι
        (Fork.ofι (P := kernel (X.kernelSequenceOpcycles f g fg h n).g)
          (kernel.ι (X.kernelSequenceOpcycles f g fg h n).g) ⋯) =
    Fork.ι (KernelFork.ofι (X.kernelSequenceOpcycles f g fg h n).f ⋯)

Tactic:
simp [← cancel_epi (X.pOpcycles f g n)]

Premises used: CategoryTheory.cancel_epi, CategoryTheory.Abelian.SpectralObject.pOpcycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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 : ℤ
⊢ IsLimit (KernelFork.ofι (X.kernelSequenceOpcycles f g fg h n).f ⋯)

Tactic:
exact IsLimit.ofIsoLimit (kernelIsKernel _)
    (Iso.symm (Fork.ext (X.opcyclesIsoKernel f g fg h n) (by
      simp [← cancel_epi (X.pOpcycles f g n)])))

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Limits.Fork.ext, CategoryTheory.Limits.kernelIsKernel, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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))
⊢ 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 _ _)
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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))
this : Mono (X.toCycles f g fg h n)
⊢ IsIso (X.toCycles f g fg h n)

Tactic:
Balanced.isIso_of_mono_of_epi _

Premises used: CategoryTheory.Balanced.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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))
this : Mono (X.toCycles f g fg h n)
⊢ IsIso (X.toCycles f g fg h n)

Tactic:
exact Balanced.isIso_of_mono_of_epi _

Premises used: CategoryTheory.Balanced.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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))
⊢ 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 _ _)
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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))
this : Epi (X.fromOpcycles f g fg h n)
⊢ IsIso (X.fromOpcycles f g fg h n)

Tactic:
Balanced.isIso_of_mono_of_epi _

Premises used: CategoryTheory.Balanced.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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))
this : Epi (X.fromOpcycles f g fg h n)
⊢ IsIso (X.fromOpcycles f g fg h n)

Tactic:
exact Balanced.isIso_of_mono_of_epi _

Premises used: CategoryTheory.Balanced.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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
A : C
n : ℤ
x : (X.H n).obj (mk₁ fg) ⟶ A
hx : (X.H n).map (twoδ₂Toδ₁ f g fg h) ≫ x = 0
⊢ X.toCycles f g fg h n ≫ X.descCycles f g fg h x hx = x

Tactic:
(X.cokernelSequenceCycles_exact f g fg h n).g_desc x hx

Premises used: CategoryTheory.Abelian.SpectralObject.cycles, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_exact, CategoryTheory.Limits.limit, CategoryTheory.Abelian.SpectralObject.toCycles, CategoryTheory.ShortComplex.Exact.g_desc, CategoryTheory.Abelian.SpectralObject.descCycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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
A : C
n : ℤ
x : A ⟶ (X.H n).obj (mk₁ fg)
hx : x ≫ (X.H n).map (twoδ₁Toδ₀ f g fg h) = 0
⊢ X.liftOpcycles f g fg h x hx ≫ X.fromOpcycles f g fg h n = x

Tactic:
(X.kernelSequenceOpcycles_exact f g fg h n).lift_f x hx

Premises used: CategoryTheory.Abelian.SpectralObject.liftOpcycles, CategoryTheory.Abelian.SpectralObject.fromOpcycles, CategoryTheory.Limits.colimit, CategoryTheory.Abelian.SpectralObject.opcycles, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_exact, CategoryTheory.ShortComplex.Exact.lift_f
-- Module: Mathlib.Algebra.Homology.SpectralObject.Cycles
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.δ f₂ f₃ n₀ n₁ ⋯ ≫ X.δ f₁ f₂ n₁ (n₁ + 1) ⋯ = 0

Tactic:
simp