awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
rw₁ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    ((X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) ≫
      X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    0
rw₂ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫
      X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁)
    0
rw₃ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯)) 0
rw₄ :
  Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃)))
    (X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯)) 0
rw₅ : Eq (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃))) (X.iCycles f₂ f₃ n₀ ≫ 0) 0
rw₆ rw₇ : Eq.{v_1 + 1} (α := X.cycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (mk₁ (f₁ ≫ f₂ ≫ f₃))) 0 0
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0

Tactic:
rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) n₁),
    zero_comp, assoc, X.opcyclesMap_fromOpcycles f₁ f₂ f₁ f₂₃ f₁₂ h₁₂
    (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃)
    (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) (by rw [reassoc_of% h₁₂])) n₁ rfl rfl,
    Ψ_fromOpcycles_assoc .., zero₁ .., comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Abelian.SpectralObject.fromOpcycles, CategoryTheory.cancel_mono, CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles, CategoryTheory.Abelian.SpectralObject.Ψ_fromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.zero₁, CategoryTheory.ComposableArrows.twoδ₂Toδ₁, CategoryTheory.ComposableArrows.threeδ₃Toδ₂, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.zero_comp, 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 :
  ∀ ⦃A : C⦄
    (x₂ :
      A ⟶
        { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
            f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
            ShortComplex.{v_1, u_1} C }.X₂),
    x₂ ≫
          { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
              f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
              ShortComplex.{v_1, u_1} C }.g =
        0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
        A' ⟶
          { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
              f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
              ShortComplex.{v_1, u_1} C }.X₁),
        π ≫ x₂ =
          x₁ ≫
            { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
                f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
                zero := ⋯ }.f
⊢ { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
      f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
      ShortComplex.{v_1, u_1} C }.Exact

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements]

Premises used: CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements
-- 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₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.g =
    0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
    A' ⟶
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.X₁),
    π ≫ z =
      x₁ ≫
        { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
            f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.f

Tactic:
⟨A, 𝟙 _, inferInstance,
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ?_, ?_⟩

Premises used: CategoryTheory.CategoryStruct.id, inferInstance, CategoryTheory.Abelian.SpectralObject.liftCycles, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Abelian.SpectralObject.iCycles
-- 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₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.g =
    0
refine_1 : (z ≫ X.iCycles f₂ f₃ n₀) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁ = 0
refine_2 :
  𝟙 A ≫ z =
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
    A' ⟶
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.X₁),
    π ≫ z =
      x₁ ≫
        { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
            f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.f

Tactic:
refine ⟨A, 𝟙 _, inferInstance,
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ?_, ?_⟩
-- 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₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.g =
    0
refine_1 : (z ≫ X.iCycles f₂ f₃ n₀) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁ = 0
⊢ (z ≫ X.iCycles f₂ f₃ n₀) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁ = 0

Tactic:
dsimp
-- 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₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.g =
    0
refine_2 :
  𝟙 A ≫ z =
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀
⊢ 𝟙 A ≫ z =
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.f

Tactic:
dsimp
-- 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₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.g =
    0
refine_1 : z ≫ X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁ = 0
refine_1₁ : z ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ = 0
refine_1₂ : Eq (α := A ⟶ (X.H n₁).obj (mk₁ f₁₂)) (0 ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁) 0
refine_1₃ refine_1₄ : Eq.{v_1 + 1} (α := A ⟶ (X.H n₁).obj (mk₁ f₁₂)) 0 0
⊢ (z ≫ X.iCycles f₂ f₃ n₀) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁ = 0

Tactic:
rw [assoc, ← X.Ψ_fromOpcycles f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ hn₁, reassoc_of% hz, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.SpectralObject.Ψ_fromOpcycles, 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 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₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.g =
    0
refine_2 :
  (𝟙 A ≫ z) ≫ X.iCycles f₂ f₃ n₀ =
    (X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫
        X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀) ≫
      X.iCycles f₂ f₃ n₀
refine_2₁ :
  z ≫ X.iCycles f₂ f₃ n₀ =
    (X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫
        X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀) ≫
      X.iCycles f₂ f₃ n₀
refine_2₂ :
  z ≫ X.iCycles f₂ f₃ n₀ =
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀ ≫ X.iCycles f₂ f₃ n₀
refine_2₃ :
  z ≫ X.iCycles f₂ f₃ n₀ =
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫ X.iCycles f₁₂ f₃ n₀ ≫ (X.H n₀).map (𝟙 (mk₁ f₃))
refine_2₄ :
  z ≫ X.iCycles f₂ f₃ n₀ =
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫ X.iCycles f₁₂ f₃ n₀ ≫ 𝟙 ((X.H n₀).obj (mk₁ f₃))
refine_2₅ : z ≫ X.iCycles f₂ f₃ n₀ = X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫ X.iCycles f₁₂ f₃ n₀
refine_2₆ refine_2₇ : z ≫ X.iCycles f₂ f₃ n₀ = z ≫ X.iCycles f₂ f₃ n₀
⊢ 𝟙 A ≫ z =
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀

Tactic:
rw [← cancel_mono (X.iCycles f₂ f₃ n₀), id_comp, assoc,
      X.cyclesMap_i _ _ _ _ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) (𝟙 _) n₀ (by cat_disch),
      Functor.map_id, comp_id, liftCycles_i]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.SpectralObject.cyclesMap_i, CategoryTheory.CategoryStruct.id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ComposableArrows.threeδ₁Toδ₀, CategoryTheory.Functor.map_id, CategoryTheory.Abelian.SpectralObject.liftCycles_i, CategoryTheory.Category.id_comp, CategoryTheory.Abelian.SpectralObject.iCycles
-- 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 :
  ∀ ⦃A : C⦄
    (x₂ :
      A ⟶
        { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
            g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
            ShortComplex.{v_1, u_1} C }.X₂),
    x₂ ≫
          { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
              g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
              ShortComplex.{v_1, u_1} C }.g =
        0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
        A' ⟶
          { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
              g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
              ShortComplex.{v_1, u_1} C }.X₁),
        π ≫ x₂ =
          x₁ ≫
            { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁,
                f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁,
                zero := ⋯ }.f
⊢ { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
      g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements]

Premises used: CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements
-- 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₁
A : C
z₀ :
  A ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    0
obtain :
  ∀ (A₁ : C) (π₁ : A₁ ⟶ A),
    Epi π₁ →
      ∀ (z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)) (hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁),
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
          A' ⟶
            { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁,
                f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁,
                zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁),
          π ≫ z₀ =
            x₁ ≫
              { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁,
                  f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁,
                  zero := ⋯ }.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
    A' ⟶
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.X₁),
    π ≫ z₀ =
      x₁ ≫
        { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
            g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.f

Tactic:
obtain ⟨A₁, π₁, _, z₁, hz₁⟩ := surjective_up_to_refinements_of_epi (X.pOpcycles f₁ f₂ n₁) z₀

Premises used: CategoryTheory.surjective_up_to_refinements_of_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 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₁
A : C
z₀ :
  A ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
dsimp : z₁ ≫ X.pOpcycles f₁ f₂₃ n₁ = 0
⊢ z₁ ≫ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).g = 0

Tactic:
dsimp
-- 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₁
A : C
z₀ :
  A ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
⊢ X.pOpcycles f₁ f₂ n₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ =
    (X.H n₁).map (𝟙 (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂₃ n₁

Tactic:
have H := X.p_opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) (𝟙 _) n₁ (by cat_disch)
-- 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₁
A : C
z₀ :
  A ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
H :
  X.pOpcycles f₁ f₂ n₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ =
    (X.H n₁).map (𝟙 (mk₁ f₁)) ≫ X.pOpcycles f₁ f₂₃ n₁
⊢ X.pOpcycles f₁ f₂ n₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = X.pOpcycles f₁ f₂₃ n₁

Tactic:
rw [Functor.map_id, id_comp] at H

Premises used: CategoryTheory.Functor.map_id, 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₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z₀ :
  A ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
H : X.pOpcycles f₁ f₂ n₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = X.pOpcycles f₁ f₂₃ n₁
rw : z₁ ≫ X.pOpcycles f₁ f₂ n₁ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0
rw₁ : π₁ ≫ z₀ ≫ X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ = 0
rw₂ : Eq (α := A₁ ⟶ X.opcycles f₁ f₂₃ n₁) (π₁ ≫ 0) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := A₁ ⟶ X.opcycles f₁ f₂₃ n₁) 0 0
⊢ z₁ ≫ X.pOpcycles f₁ f₂₃ n₁ = 0

Tactic:
rw [← H, ← reassoc_of% hz₁, hz₀, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero