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
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
⊢ n₀ = n₁ - 1

Tactic:
lia
-- 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
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
⊢ n₁ - 1 + 1 = n₁

Tactic:
obtain rfl : n₀ = n₁ -1 := by lia

Premises used: rfl
-- 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
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
hn₂ : n₁ - 1 + 1 = n₁
⊢ X.δ f g (n₁ - 1) n₁ hn₂ ≫ x = 0

Tactic:
obtain rfl : n₀ = n₁ -1 := by lia

Premises used: rfl
-- 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
n₁ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f) ⟶ A
hn₁ : n₁ - 1 + 1 = n₁
hx : X.δ f g (n₁ - 1) n₁ hn₁ ≫ x = 0
⊢ X.δ f g (n₁ - 1) n₁ ⋯ ≫ x = 0

Tactic:
hx
-- 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
n₁ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f) ⟶ A
hn₁ : n₁ - 1 + 1 = n₁
hx : X.δ f g (n₁ - 1) n₁ hn₁ ≫ x = 0
⊢ X.δ f g (n₁ - 1) n₁ ⋯ ≫ x = 0

Tactic:
exact hx
-- 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
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.pOpcycles f g n₁ ≫ X.descOpcycles f g n₀ n₁ hn₁ x hx = x

Tactic:
apply cokernel.π_desc

Premises used: CategoryTheory.Limits.cokernel.π_desc
-- 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''
α : 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
rw₃ rw₄ : Eq.{v_1 + 1} (α := X.cycles f g n ⟶ (X.H (n + 1)).obj (mk₁ f')) 0 0
⊢ (X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯)) ≫ X.δ f' g' n (n + 1) ⋯ = 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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ComposableArrows.naturality', CategoryTheory.Abelian.SpectralObject.δ_naturality, HAdd.hAdd, CategoryTheory.ComposableArrows.homMk₁, CategoryTheory.Limits.zero_comp, OfNat.ofNat, CategoryTheory.Abelian.SpectralObject.iCycles_δ_assoc, CategoryTheory.NatTrans.app
-- 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'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ g ⟶ mk₁ g'
n : ℤ
hβ : β = homMk₁ (α.app 1) (α.app 2) ⋯
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) ⋯)
⊢ X.cyclesMap f g f' g' α n ≫ X.iCycles f' g' n = X.iCycles f g n ≫ (X.H n).map β

Tactic:
subst 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'
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ 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) ⋯)

Tactic:
simp [cyclesMap]

Premises used: CategoryTheory.Abelian.SpectralObject.cyclesMap
-- 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
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
rw₄ rw₅ : X.iCycles f g n = X.iCycles f g n
⊢ X.cyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.cycles 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]

Premises used: CategoryTheory.Abelian.SpectralObject.cyclesMap_i, CategoryTheory.CategoryStruct.id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp, 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
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 : α ≫ α' = α''
subst : X.cyclesMap f g f' g' α n ≫ X.cyclesMap f' g' f'' g'' α' n = X.cyclesMap f g f'' g'' (α ≫ α') n
⊢ X.cyclesMap f g f' g' α n ≫ X.cyclesMap f' g' f'' g'' α' n = X.cyclesMap f g f'' g'' α'' n

Tactic:
subst 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'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
n : ℤ
rw :
  X.iCycles f g n ≫
      (X.H n).map (CategoryStruct.comp (Y := mk₁ g') (homMk₁ (α.app 1) (α.app 2) ⋯) (homMk₁ (α'.app 1) (α'.app 2) ⋯)) =
    X.cyclesMap f g f'' g'' (α ≫ α') n ≫ X.iCycles f'' g'' n
⊢ X.cyclesMap f g f' g' α n ≫ X.cyclesMap f' g' f'' g'' α' n = X.cyclesMap f g 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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.SpectralObject.cyclesMap_i, CategoryTheory.cancel_mono, CategoryTheory.Functor.map_comp, CategoryTheory.Abelian.SpectralObject.cyclesMap_i_assoc, rfl, 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
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.iCycles f g n ≫
      (X.H n).map (CategoryStruct.comp (Y := mk₁ g') (homMk₁ (α.app 1) (α.app 2) ⋯) (homMk₁ (α'.app 1) (α'.app 2) ⋯)) =
    X.cyclesMap f g f'' g'' (α ≫ α') n ≫ X.iCycles f'' g'' n

Tactic:
(X.cyclesMap_i _ _ _ _ _ _ _).symm

Premises used: CategoryTheory.Abelian.SpectralObject.cyclesMap_i, 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
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.iCycles f g n ≫
      (X.H n).map (CategoryStruct.comp (Y := mk₁ g') (homMk₁ (α.app 1) (α.app 2) ⋯) (homMk₁ (α'.app 1) (α'.app 2) ⋯)) =
    X.cyclesMap f g f'' g'' (α ≫ α') n ≫ X.iCycles f'' g'' n

Tactic:
exact (X.cyclesMap_i _ _ _ _ _ _ _).symm

Premises used: CategoryTheory.Abelian.SpectralObject.cyclesMap_i, 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
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 : ℤ
⊢ n - 1 + 1 = n

Tactic:
lia
-- 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''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ (mk₁ f).obj' 0 homMk₁._proof_4 ⟶ (mk₁ f').obj' 0 homMk₁._proof_4

Tactic:
exact α.app 0

Premises used: OfNat.ofNat, CategoryTheory.NatTrans.app
-- 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''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ (mk₁ f).obj' 1 homMk₁._proof_5 ⟶ (mk₁ f').obj' 1 homMk₁._proof_5

Tactic:
exact α.app 1

Premises used: OfNat.ofNat, CategoryTheory.NatTrans.app
-- 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''
α : 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
rw₂ rw₃ : Eq.{v_1 + 1} (α := (X.H (n - 1)).obj (mk₁ g) ⟶ X.opcycles f' g' n) 0 0
⊢ X.δ f g (n - 1) n ⋯ ≫ (X.H n).map (homMk₁ (α.app 0) (α.app 1) ⋯) ≫ 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]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.ComposableArrows.naturality', CategoryTheory.Abelian.SpectralObject.δ_naturality_assoc, CategoryTheory.ComposableArrows.homMk₁, CategoryTheory.Abelian.SpectralObject.δ_pOpcycles, OfNat.ofNat, CategoryTheory.NatTrans.app
-- 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'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ f ⟶ mk₁ f'
n : ℤ
hβ : β = homMk₁ (α.app 0) (α.app 1) ⋯
subst :
  X.pOpcycles f g n ≫ X.opcyclesMap f g f' g' α n = (X.H n).map (homMk₁ (α.app 0) (α.app 1) ⋯) ≫ X.pOpcycles f' g' n
⊢ X.pOpcycles f g n ≫ X.opcyclesMap f g f' g' α n = (X.H n).map β ≫ X.pOpcycles f' g' n

Tactic:
subst 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'
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ X.pOpcycles f g n ≫ X.opcyclesMap f g f' g' α n = (X.H n).map (homMk₁ (α.app 0) (α.app 1) ⋯) ≫ X.pOpcycles f' g' n

Tactic:
simp [opcyclesMap]

Premises used: CategoryTheory.Abelian.SpectralObject.opcyclesMap
-- 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
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
rw₄ rw₅ : 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)

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]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id, CategoryTheory.ComposableArrows.mk₂, CategoryTheory.Functor.map_id, CategoryTheory.Abelian.SpectralObject.p_opcyclesMap, CategoryTheory.cancel_epi, CategoryTheory.Abelian.SpectralObject.pOpcycles, CategoryTheory.ComposableArrows.mk₁, 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''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
α'' : mk₂ f g ⟶ mk₂ f'' g''
n : ℤ
h : α ≫ α' = α''
subst : X.opcyclesMap f g f' g' α n ≫ X.opcyclesMap f' g' f'' g'' α' n = X.opcyclesMap f g f'' g'' (α ≫ α') n
⊢ X.opcyclesMap f g f' g' α n ≫ X.opcyclesMap f' g' f'' g'' α' n = X.opcyclesMap f g f'' g'' α'' n

Tactic:
subst 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'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
n : ℤ
rw :
  (X.H n).map (CategoryStruct.comp (Y := mk₁ f') (homMk₁ (α.app 0) (α.app 1) ⋯) (homMk₁ (α'.app 0) (α'.app 1) ⋯)) ≫
      X.pOpcycles f'' g'' n =
    X.pOpcycles f g n ≫ X.opcyclesMap f g f'' g'' (α ≫ α') n
⊢ X.opcyclesMap f g f' g' α n ≫ X.opcyclesMap f' g' 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]

Premises used: CategoryTheory.Abelian.SpectralObject.p_opcyclesMap_assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Abelian.SpectralObject.p_opcyclesMap, 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''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
n : ℤ
⊢ (X.H n).map (CategoryStruct.comp (Y := mk₁ f') (homMk₁ (α.app 0) (α.app 1) ⋯) (homMk₁ (α'.app 0) (α'.app 1) ⋯)) ≫
      X.pOpcycles f'' g'' n =
    X.pOpcycles f g n ≫ X.opcyclesMap f g f'' g'' (α ≫ α') n

Tactic:
exact (X.p_opcyclesMap _ _ _ _ _ _ _ (by cat_disch)).symm

Premises used: CategoryTheory.Abelian.SpectralObject.p_opcyclesMap, 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 : ℤ
⊢ cokernel.π ((X.H n).map (twoδ₂Toδ₁ f g fg h)) ≫ (X.cokernelIsoCycles f g fg h n).hom ≫ X.iCycles f g n =
    (X.H n).map (twoδ₁Toδ₀ f g fg h)

Tactic:
(X.composableArrows₅_exact f g fg h n (n + 1)).cokerIsoKer_hom_fac 0

Premises used: CategoryTheory.Abelian.SpectralObject.cycles, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.Abelian.SpectralObject.composableArrows₅_exact, HAdd.hAdd, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac, CategoryTheory.Abelian.SpectralObject.δ, OfNat.ofNat, CategoryTheory.ComposableArrows.Precomp.map, 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.pOpcycles f g n ≫ (X.opcyclesIsoKernel f g fg h n).hom ≫ kernel.ι ((X.H n).map (twoδ₁Toδ₀ f g fg h)) =
    (X.H n).map (twoδ₂Toδ₁ f g fg h)

Tactic:
(X.composableArrows₅_exact f g fg h (n - 1) n).cokerIsoKer_hom_fac 2

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, HSub.hSub, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.Abelian.SpectralObject.composableArrows₅_exact, CategoryTheory.Abelian.SpectralObject.opcycles, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac, CategoryTheory.Abelian.SpectralObject.δ, CategoryTheory.ComposableArrows.Mk₁.map, OfNat.ofNat, CategoryTheory.ComposableArrows.Precomp.map, 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 : ℤ
⊢ (X.H n).map (twoδ₁Toδ₀ f g fg h) ≫ X.δ f g n (n + 1) ⋯ = 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 : ℤ
⊢ Epi (X.toCycles f g fg h n)

Tactic:
(ShortComplex.exact_iff_epi_kernel_lift _).1 (X.exact₃ f g fg h n (n + 1))

Premises used: CategoryTheory.Abelian.SpectralObject.cycles, HAdd.hAdd, CategoryTheory.Abelian.SpectralObject.exact₃, CategoryTheory.Abelian.SpectralObject.toCycles, Iff.mp, CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift, CategoryTheory.Abelian.SpectralObject.δ, 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
fg : i ⟶ k
h : f ≫ g = fg
n : ℤ
⊢ X.toCycles f g fg h n ≫ X.iCycles f g n = (X.H n).map (twoδ₁Toδ₀ f g fg h)

Tactic:
kernel.lift_ι ..

Premises used: CategoryTheory.Abelian.SpectralObject.cycles, CategoryTheory.Abelian.SpectralObject.toCycles, CategoryTheory.Limits.kernel.lift_ι, 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
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 (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯) = (X.H n).map (β ≫ twoδ₁Toδ₀ f' g' fg' h')
⊢ 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

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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.SpectralObject.cyclesMap_i, CategoryTheory.cancel_mono, CategoryTheory.ComposableArrows.naturality', CategoryTheory.ComposableArrows.homMk₁, CategoryTheory.Functor.map_comp, OfNat.ofNat, CategoryTheory.NatTrans.app, rfl, CategoryTheory.Abelian.SpectralObject.toCycles_i, CategoryTheory.Abelian.SpectralObject.toCycles_i_assoc, 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
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 : twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯ = β ≫ twoδ₁Toδ₀ f' g' fg' h'
⊢ (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')

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' (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
e_a₁ :
  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
⊢ twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯ = β ≫ twoδ₁Toδ₀ f' g' fg' h'

Tactic:
ext