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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁ = X.δ f₂ f₃ n₀ n₁ hn₁

Tactic:
simp only [δToCycles, liftCycles_i]

Premises used: CategoryTheory.Abelian.SpectralObject.δToCycles, CategoryTheory.Abelian.SpectralObject.liftCycles_i
-- 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₁₂
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  (X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₁ :
  X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.iCycles f₁ f₂ n₁ =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₂ :
  X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.iCycles f₁ f₂ n₁
rw₃ : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) = X.δ f₂ f₃ n₀ n₁ hn₁
rw₄ : (X.H n₀).map (𝟙 (mk₁ f₃)) ≫ X.δ f₂ f₃ n₀ n₁ ⋯ = X.δ f₂ f₃ n₀ n₁ hn₁
rw₅ : 𝟙 ((X.H n₀).obj (mk₁ f₃)) ≫ X.δ f₂ f₃ n₀ n₁ ⋯ = X.δ f₂ f₃ n₀ n₁ hn₁
rw₆ rw₇ : X.δ f₂ f₃ n₀ n₁ ⋯ = X.δ f₂ f₃ n₀ n₁ hn₁
⊢ X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁

Tactic:
rw [← cancel_mono (X.iCycles f₁ f₂ n₁), Category.assoc,
    toCycles_i, δToCycles_iCycles,
    ← X.δ_naturality f₁₂ f₃ f₂ f₃ (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) (𝟙 _) n₀ n₁,
    Functor.map_id, Category.id_comp]

Premises used: CategoryTheory.Abelian.SpectralObject.δToCycles_iCycles, CategoryTheory.Category.assoc, CategoryTheory.CategoryStruct.id, CategoryTheory.cancel_mono, CategoryTheory.Abelian.SpectralObject.δ_naturality, CategoryTheory.Functor.map_id, CategoryTheory.ComposableArrows.twoδ₁Toδ₀, CategoryTheory.Category.id_comp, CategoryTheory.Abelian.SpectralObject.toCycles_i, 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 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₁
⊢ 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 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₀ - 1) n₀ ⋯ ≫ X.δ f₁ f₂ n₀ n₁ hn₁ = 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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁ = X.δ f₁ f₂ n₀ n₁ hn₁

Tactic:
simp only [δFromOpcycles, p_descOpcycles]

Premises used: CategoryTheory.Abelian.SpectralObject.p_descOpcycles, CategoryTheory.Abelian.SpectralObject.δFromOpcycles
-- 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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  X.pOpcycles f₂ f₃ n₀ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
    X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
rw₁ :
  (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
    X.pOpcycles f₂ f₃ n₀ ≫ X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
rw₂ : (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δ f₁ f₂ n₀ n₁ hn₁
rw₃ : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ (X.H n₁).map (𝟙 (mk₁ f₁)) = X.δ f₁ f₂ n₀ n₁ hn₁
rw₄ : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ 𝟙 ((X.H n₁).obj (mk₁ f₁)) = X.δ f₁ f₂ n₀ n₁ hn₁
rw₅ rw₆ : X.δ f₁ f₂ n₀ n₁ ⋯ = X.δ f₁ f₂ n₀ n₁ hn₁
⊢ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ = X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁

Tactic:
rw [← cancel_epi (X.pOpcycles f₂ f₃ n₀),
    p_fromOpcycles_assoc, pOpcycles_δFromOpcycles,
    X.δ_naturality f₁ f₂ f₁ f₂₃ (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) n₀ n₁,
    Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles, CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id, CategoryTheory.Abelian.SpectralObject.p_fromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.δ_naturality, CategoryTheory.ComposableArrows.twoδ₂Toδ₁, CategoryTheory.Functor.map_id, CategoryTheory.cancel_epi, CategoryTheory.Abelian.SpectralObject.pOpcycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫
      (X.H n₂).map (𝟙 (mk₁ (f₁ ≫ f₂))) ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0
rw₁ :
  X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫
      𝟙 ((X.H n₂).obj (mk₁ (f₁ ≫ f₂))) ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0
rw₂ : X.δ (f₁ ≫ f₂) f₃ n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ = 0
rw₃ : X.δToCycles f₁ f₂ f₃ n₁ n₂ ⋯ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ = 0
rw₄ rw₅ : Eq.{v_1 + 1} (α := (X.H n₁).obj (mk₁ f₃) ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) 0 0
⊢ (X.H n₁).map (twoδ₂Toδ₁ f₃ f₄ (f₃ ≫ f₄) ⋯) ≫
      X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0

Tactic:
rw [X.δ_naturality_assoc (f₁ ≫ f₂) f₃ (f₁ ≫ f₂) (f₃ ≫ f₄)
        (𝟙 _) (twoδ₂Toδ₁ f₃ f₄ _ rfl) n₁ n₂ rfl hn₂, Functor.map_id, id_comp,
        δ_toCycles_assoc .., δToCycles_πE ..]

Premises used: CategoryTheory.Abelian.SpectralObject.δToCycles_πE, CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.SpectralObject.δ_naturality_assoc, CategoryTheory.ComposableArrows.twoδ₂Toδ₁, CategoryTheory.Functor.map_id, CategoryTheory.Abelian.SpectralObject.δ_toCycles_assoc, CategoryTheory.CategoryStruct.comp, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  Eq (α := (X.H n₀).obj (mk₁ f₅) ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃)
    (0 ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := (X.H n₀).obj (mk₁ f₅) ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) 0 0
⊢ X.δ (f₃ ≫ f₄) f₅ n₀ n₁ hn₁ ≫
      X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0

Tactic:
rw [δ_δ_assoc .., zero_comp]

Premises used: CategoryTheory.Abelian.SpectralObject.δ_δ_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
subst :
  X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ =
    X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃
⊢ X.toCycles f₃ f₄ f₃₄ h₃₄ n₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ =
    X.δ f₁₂ f₃₄ n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃

Tactic:
subst h₁₂ h₃₄
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ =
    X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃

Tactic:
simp only [d, δ_toCycles_assoc, toCycles_πE_descE]

Premises used: CategoryTheory.Abelian.SpectralObject.d, CategoryTheory.Abelian.SpectralObject.δ_toCycles_assoc, CategoryTheory.Abelian.SpectralObject.toCycles_πE_descE
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) ≫ X.δ f₂₃ f₄ n₁ n₂ ⋯ =
    X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯ ≫ twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃)
⊢ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₂ =
    X.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.fromOpcycles f₄ f₅ f₄₅ h₄₅ n₁ ≫ X.δ f₂₃ f₄₅ n₁ n₂ hn₂

Tactic:
rw [← cancel_epi (X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₃ f₄ f₃₄ h₃₄ n₁),
    X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_ιE_assoc .., p_fromOpcycles, toCycles_i_assoc, fromOpcyles_δ ..,
    πE_ιE_assoc .., pOpcycles_δFromOpcycles, toCycles_i_assoc, ← Functor.map_comp, Eq.comm]

Premises used: CategoryTheory.Abelian.SpectralObject.toCycles_πE_d_assoc, CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles, CategoryTheory.Abelian.SpectralObject.πE_ιE_assoc, CategoryTheory.Abelian.SpectralObject.p_fromOpcycles, CategoryTheory.Abelian.SpectralObject.toCycles, Eq.comm, CategoryTheory.Functor.map_comp, CategoryTheory.Abelian.SpectralObject.πE, CategoryTheory.cancel_epi, CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ, rfl, CategoryTheory.Abelian.SpectralObject.toCycles_i_assoc
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hαβ :
  autoParam
    (Eq (α := (mk₁ (f₁ ≫ f₂)).obj 1 ⟶ (mk₁ f₂₃).obj 1) ((twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯ ≫ twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃).app 1)
      ((twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄).app 0))
    δ_naturality._auto_1
⊢ (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) ≫ X.δ f₂₃ f₄ n₁ n₂ ⋯ =
    X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯ ≫ twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃)

Tactic:
apply δ_naturality

Premises used: CategoryTheory.Abelian.SpectralObject.δ_naturality
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ autoParam
    (Eq (α := (mk₁ (f₁ ≫ f₂)).obj 1 ⟶ (mk₁ f₂₃).obj 1) ((twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯ ≫ twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃).app 1)
      ((twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄).app 0))
    δ_naturality._auto_1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₆ : i₅ ⟶ i₆
f₇ : i₆ ⟶ i₇
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
rw :
  X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
rw₁ :
  X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫
      X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫
        X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫ 0
rw₂ :
  X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫
      X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫
        X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫ 0
rw₃ :
  X.toCycles f₅ f₆ (f₅ ≫ f₆) ⋯ n₁ ≫
      X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂ ≫
        X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    0
rw₄ :
  X.δ (f₃ ≫ f₄) (f₅ ≫ f₆) n₁ n₂ hn₂ ≫
      X.toCycles f₃ f₄ (f₃ ≫ f₄) ⋯ n₂ ≫ X.πE f₃ f₄ f₅ n₁ n₂ n₃ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ =
    0
rw₅ :
  X.δ (f₃ ≫ f₄) (f₅ ≫ f₆) n₁ n₂ hn₂ ≫
      X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₂ n₃ hn₃ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₃ ≫ X.πE f₁ f₂ f₃ n₂ n₃ n₄ hn₃ hn₄ =
    0
rw₆ :
  Eq (α := (X.H n₁).obj (mk₁ (f₅ ≫ f₆)) ⟶ X.E f₁ f₂ f₃ n₂ n₃ n₄ hn₃ hn₄)
    (0 ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₃ ≫ X.πE f₁ f₂ f₃ n₂ n₃ n₄ hn₃ hn₄) 0
rw₇ rw₈ : Eq.{v_1 + 1} (α := (X.H n₁).obj (mk₁ (f₅ ≫ f₆)) ⟶ X.E f₁ f₂ f₃ n₂ n₃ n₄ hn₃ hn₄) 0 0
⊢ X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ = 0

Tactic:
rw [← cancel_epi (X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁), comp_zero, comp_zero,
    X.toCycles_πE_d_assoc f₃ f₄ f₅ f₆ f₇ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    X.toCycles_πE_d f₁ f₂ f₃ f₄ f₅ _ rfl _ rfl n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄,
    δ_δ_assoc .., zero_comp]

Premises used: CategoryTheory.Abelian.SpectralObject.toCycles_πE_d, CategoryTheory.Abelian.SpectralObject.toCycles_πE_d_assoc, CategoryTheory.Abelian.SpectralObject.δ_δ_assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Abelian.SpectralObject.toCycles, CategoryTheory.Abelian.SpectralObject.πE, CategoryTheory.Limits.zero_comp, CategoryTheory.cancel_epi, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
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₁
rw : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ (X.H n₁).map (𝟙 (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂ n₁ = 0
rw₁ : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ 𝟙 ((X.H n₁).obj (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂ n₁ = 0
rw₂ : X.δ f₁ f₂ n₀ n₁ ⋯ ≫ X.pOpcycles f₁ f₂ n₁ = 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := (X.H n₀).obj (mk₁ f₂) ⟶ X.opcycles f₁ f₂ n₁) 0 0
⊢ (X.H n₀).map (twoδ₂Toδ₁ f₂ f₃ (f₂ ≫ f₃) ⋯) ≫ X.δ f₁ (f₂ ≫ f₃) n₀ n₁ hn₁ ≫ X.pOpcycles f₁ f₂ n₁ = 0

Tactic:
rw [X.δ_naturality_assoc f₁ f₂ f₁ (f₂ ≫ f₃) (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ _ rfl) _ _ rfl,
        Functor.map_id, id_comp, δ_pOpcycles ..]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.SpectralObject.δ_naturality_assoc, CategoryTheory.ComposableArrows.twoδ₂Toδ₁, CategoryTheory.Functor.map_id, CategoryTheory.CategoryStruct.comp, CategoryTheory.Abelian.SpectralObject.δ_pOpcycles, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
subst : X.toCycles f₂ f₃ (f₂ ≫ f₃) ⋯ n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = X.δ f₁ (f₂ ≫ f₃) n₀ n₁ hn₁ ≫ X.pOpcycles f₁ f₂ n₁
⊢ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = X.δ f₁ f₂₃ n₀ n₁ hn₁ ≫ X.pOpcycles f₁ f₂ n₁

Tactic:
subst h₂₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.toCycles f₂ f₃ (f₂ ≫ f₃) ⋯ n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = X.δ f₁ (f₂ ≫ f₃) n₀ n₁ hn₁ ≫ X.pOpcycles f₁ f₂ n₁

Tactic:
simp only [Ψ, toCycles_descCycles]

Premises used: CategoryTheory.Abelian.SpectralObject.toCycles_descCycles, CategoryTheory.Abelian.SpectralObject.Ψ
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw :
  X.δ f₁ (f₂ ≫ f₃) n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) =
    (X.H n₀).map (twoδ₁Toδ₀ f₂ f₃ (f₂ ≫ f₃) ⋯) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ = X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁

Tactic:
rw [← cancel_epi (X.toCycles f₂ f₃ _ rfl n₀),
    toCycles_Ψ_assoc .., p_fromOpcycles, toCycles_i_assoc]

Premises used: CategoryTheory.Abelian.SpectralObject.toCycles_Ψ_assoc, CategoryTheory.Abelian.SpectralObject.p_fromOpcycles, CategoryTheory.Abelian.SpectralObject.toCycles, CategoryTheory.cancel_epi, rfl, CategoryTheory.Abelian.SpectralObject.toCycles_i_assoc
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f₁ (f₂ ≫ f₃) n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) =
    (X.H n₀).map (twoδ₁Toδ₀ f₂ f₃ (f₂ ≫ f₃) ⋯) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁

Tactic:
exact (X.δ_naturality _ _ _ _ _ _ _ _ rfl).symm

Premises used: CategoryTheory.Abelian.SpectralObject.δ_naturality, Eq.symm
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
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₁
rw rw₁ : f₁₂ ≫ f₃ = f₁₂ ≫ f₃
⊢ f₁₂ ≫ f₃ = f₁ ≫ f₂ ≫ f₃

Tactic:
rw [reassoc_of% h₁₂]
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
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₁
rw rw₁ : f₁ ≫ f₂₃ = f₁ ≫ f₂₃
⊢ f₁ ≫ f₂₃ = f₁ ≫ f₂ ≫ f₃

Tactic:
rw [h₂₃]
-- Module: Mathlib.Algebra.Homology.SpectralObject.Differentials
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₁
rw :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫ 0)
rw₁ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₀ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
    0
rw₂ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    ((X.H n₀).map (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯) ≫ X.toCycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) 0
rw₃ :
  Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁)
    ((X.H n₀).map (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯) ≫ X.δ f₁ f₂₃ n₀ n₁ ⋯ ≫ X.pOpcycles f₁ f₂ n₁) 0
rw₄ : Eq (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁) (0 ≫ X.pOpcycles f₁ f₂ n₁) 0
rw₅ rw₆ : Eq.{v_1 + 1} (α := (X.H n₀).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)) ⟶ X.opcycles f₁ f₂ n₁) 0 0
⊢ X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = 0

Tactic:
rw [← cancel_epi (X.toCycles f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) n₀), comp_zero,
    X.toCycles_cyclesMap_assoc f₁₂ f₃ f₂ f₃ (f₁ ≫ f₂ ≫ f₃)
    (by rw [reassoc_of% h₁₂]) f₂₃ h₂₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂)
    (twoδ₁Toδ₀ f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃])) n₀ rfl rfl,
    toCycles_Ψ .., zero₃_assoc .., zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap_assoc, CategoryTheory.ComposableArrows.threeδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.toCycles, CategoryTheory.CategoryStruct.comp, CategoryTheory.Abelian.SpectralObject.zero₃_assoc, CategoryTheory.Limits.zero_comp, CategoryTheory.Abelian.SpectralObject.toCycles_Ψ, CategoryTheory.cancel_epi, CategoryTheory.ComposableArrows.twoδ₁Toδ₀, rfl