awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : Iso.inv h.cyclesIso = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
rw :
  Iso.inv h.cyclesIso ≫ (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).homologyπ =
    h.π ≫ X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂
⊢ Iso.inv
      (ShortComplex.LeftHomologyData.homologyIso
        (ShortComplex.HomologyData.left (X.homologyDataIdId f (n₁ - 1) n₁ n₂ ⋯ ⋯))) =
    X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂

Tactic:
rw [← cancel_epi h.π, h.π_comp_homologyIso_inv]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.π_comp_homologyIso_inv, CategoryTheory.ShortComplex.LeftHomologyData.π, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : Iso.inv h.cyclesIso = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
⊢ Iso.inv h.cyclesIso ≫ (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).homologyπ =
    h.π ≫ X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂

Tactic:
simp [πE, h, this]

Premises used: CategoryTheory.Abelian.SpectralObject.πE
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
⊢ f ≫ 𝟙 j = f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
rw : h.right.p = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f ⋯)
⊢ Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁

Tactic:
rw [← cancel_epi (X.opcyclesIso ..).inv, Iso.inv_hom_id_assoc,
      ← cancel_epi (X.pOpcycles ..), p_opcyclesIso_inv_assoc ..,
      h.right.pOpcycles_comp_opcyclesIso_hom, p_fromOpcycles]

Premises used: CategoryTheory.Abelian.SpectralObject.opcyclesIso, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom, CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv_assoc, CategoryTheory.Abelian.SpectralObject.p_fromOpcycles, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.HomologyData.right, CategoryTheory.Iso.inv, CategoryTheory.Abelian.SpectralObject.pOpcycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
dsimp : 𝟙 ((X.H n₁).obj (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f ⋯)
⊢ h.right.p = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f ⋯)

Tactic:
dsimp [h]
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
rw : (X.H n₁).map (𝟙 (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f ⋯)
⊢ 𝟙 ((X.H n₁).obj (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f ⋯)

Tactic:
rw [← Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
e_a : 𝟙 (mk₁ f) = twoδ₂Toδ₁ f (𝟙 j) f ⋯
⊢ (X.H n₁).map (𝟙 (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f ⋯)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
⊢ Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁

Tactic:
have : h.right.opcyclesIso.hom =
      (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).hom ≫
        X.fromOpcycles f (𝟙 j) f (by simp) n₁ := by
    rw [← cancel_epi (X.opcyclesIso ..).inv, Iso.inv_hom_id_assoc,
      ← cancel_epi (X.pOpcycles ..), p_opcyclesIso_inv_assoc ..,
      h.right.pOpcycles_comp_opcyclesIso_hom, p_fromOpcycles]
    dsimp [h]
    rw [← Functor.map_id]
    congr 1
    cat_disch
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
this : Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ n₂ = n₁ + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
this : Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
obtain :
  ∀ (hn₂ : n₁ + 1 = n₁ + 1),
    let h := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂;
    ∀
      (this :
        Iso.hom h.right.opcyclesIso =
          (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁),
      (X.EIsoH f n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv =
        X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂
⊢ (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv = X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂

Tactic:
obtain rfl : n₂ = n₁ + 1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i j : ι
f : i ⟶ j
hn₂ : n₁ + 1 = n₁ + 1
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂
this :
  Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
rw :
  (X.EIsoH f n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ 𝟙 ((X.H n₁).obj (mk₁ f)) =
    X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ (X.EIsoH f n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv = X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂

Tactic:
rw [← cancel_mono (X.opcyclesIsoH f n₀ n₁ hn₁).hom, Category.assoc,
    opcyclesIsoH_hom .., opcyclesIsoH_inv_hom_id ..]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_id, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i j : ι
f : i ⟶ j
hn₂ : n₁ + 1 = n₁ + 1
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂
this :
  Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
dsimp :
  Eq (α := X.E (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f))
    (CategoryStruct.comp (Y := (X.H n₁).obj (mk₁ f))
      (Iso.hom
          (ShortComplex.LeftHomologyData.homologyIso
            (ShortComplex.HomologyData.left (X.homologyDataIdId f n₀ n₁ (n₁ + 1) ⋯ ⋯))) :
        X.E (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f))
      (𝟙 ((X.H n₁).obj (mk₁ f))))
    (((X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).homologyι ≫
        (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom) ≫
      X.fromOpcycles f (𝟙 j) f ⋯ n₁)
⊢ (X.EIsoH f n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ 𝟙 ((X.H n₁).obj (mk₁ f)) =
    X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁

Tactic:
dsimp [EIsoH, ιE]

Premises used: CategoryTheory.Abelian.SpectralObject.EIsoH, CategoryTheory.Abelian.SpectralObject.ιE
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i j : ι
f : i ⟶ j
hn₂ : n₁ + 1 = n₁ + 1
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂
this :
  Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
rw :
  Eq (α := X.E (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f))
    (Iso.hom (h.right.homologyIso ≪≫ h.iso.symm) ≫ 𝟙 ((X.H n₁).obj (mk₁ f))) (Iso.hom h.right.homologyIso ≫ h.right.ι)
⊢ Eq (α := X.E (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f))
    (CategoryStruct.comp (Y := (X.H n₁).obj (mk₁ f))
      (Iso.hom
          (ShortComplex.LeftHomologyData.homologyIso
            (ShortComplex.HomologyData.left (X.homologyDataIdId f n₀ n₁ (n₁ + 1) ⋯ ⋯))) :
        X.E (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f))
      (𝟙 ((X.H n₁).obj (mk₁ f))))
    (((X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).homologyι ≫
        (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom) ≫
      X.fromOpcycles f (𝟙 j) f ⋯ n₁)

Tactic:
rw [Category.assoc, ← this,
    h.left_homologyIso_eq_right_homologyIso_trans_iso_symm,
    ← ShortComplex.RightHomologyData.homologyIso_hom_comp_ι]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_ι, CategoryTheory.ShortComplex.HomologyData.left_homologyIso_eq_right_homologyIso_trans_iso_symm
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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 ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i j : ι
f : i ⟶ j
hn₂ : n₁ + 1 = n₁ + 1
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂
this :
  Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ Eq (α := X.E (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f))
    (Iso.hom (h.right.homologyIso ≪≫ h.iso.symm) ≫ 𝟙 ((X.H n₁).obj (mk₁ f))) (Iso.hom h.right.homologyIso ≫ h.right.ι)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
rw :
  (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁ ≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = 0
⊢ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫
      X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ =
    0

Tactic:
rw [← cancel_epi (X.pOpcycles ..), comp_zero,
    p_opcyclesMap_assoc _ _ _ _ _ _ (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Abelian.SpectralObject.p_opcyclesMap_assoc, CategoryTheory.ComposableArrows.twoδ₂Toδ₁, CategoryTheory.cancel_epi, CategoryTheory.Abelian.SpectralObject.pOpcycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁ ≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
dsimp : Mono (X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁)
⊢ Mono (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
rw :
  ∀ (P : C) (g : P ⟶ X.opcycles f₁ f₂₃ n₁),
    g ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ = 0 → g = 0
⊢ Mono (X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁)

Tactic:
rw [Preadditive.mono_iff_cancel_zero]

Premises used: CategoryTheory.Preadditive.mono_iff_cancel_zero
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx : x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ = 0
⊢ (x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁) ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ =
    0 ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁

Tactic:
replace hx := hx =≫ X.fromOpcycles f₁₂ f₃ _ rfl n₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
⊢ Eq (α := (mk₁ (f₁₂ ≫ f₃)).obj 0 ⟶ (mk₁ (f₁₂ ≫ f₃)).obj 0) (NatTrans.app (𝟙 (mk₁ (f₁₂ ≫ f₃))) 0)
    ((threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α := (mk₁ (f₁₂ ≫ f₃)).obj 1 ⟶ (mk₁ (f₁₂ ≫ f₃)).obj 1) (NatTrans.app (𝟙 (mk₁ (f₁₂ ≫ f₃))) 1)
    ((threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 2)
⊢ Eq (α := (mk₁ (f₁₂ ≫ f₃)).obj 1 ⟶ (mk₁ (f₁₂ ≫ f₃)).obj 1) (NatTrans.app (𝟙 (mk₁ (f₁₂ ≫ f₃))) 1)
    ((threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 2)

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx :
  (x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁) ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ =
    0 ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁
⊢ x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0

Tactic:
rw [zero_comp, Category.assoc,
    X.opcyclesMap_fromOpcycles f₁ f₂₃ f₁₂ f₃ (f₁₂ ≫ f₃) (by cat_disch) _ rfl _ (𝟙 _) n₁
      (by simp) (by cat_disch), Functor.map_id, Category.comp_id] at hx

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id, CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles, CategoryTheory.Functor.map_id, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.zero_comp, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx :
  (x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁) ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ =
    0 ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁
hx₁ :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
⊢ Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) (x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁) 0

Tactic:
rw [zero_comp, Category.assoc,
    X.opcyclesMap_fromOpcycles f₁ f₂₃ f₁₂ f₃ (f₁₂ ≫ f₃) (by cat_disch) _ rfl _ (𝟙 _) n₁
      (by simp) (by cat_disch), Functor.map_id, Category.comp_id] at hx

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id, CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles, CategoryTheory.Functor.map_id, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.zero_comp, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx_1 :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
hx : Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) (x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁) 0
rw :
  Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) (x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁)
    (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁)
rw₁ : Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) 0 (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁)
rw₂ rw₃ : Eq.{v_1 + 1} (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) 0 0
⊢ x = 0

Tactic:
rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) (by cat_disch) n₁), hx, zero_comp]

Premises used: CategoryTheory.Abelian.SpectralObject.fromOpcycles, CategoryTheory.cancel_mono, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
dsimp : Epi (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)
⊢ Epi (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
dsimp :
  X.pOpcycles f₁ f₂₃ n₁ ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ =
    ((X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁) ≫ 𝟙 (X.opcycles f₁₂ f₃ n₁)
⊢ X.pOpcycles f₁ f₂₃ n₁ ≫ (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ ⋯ ⋯).f =
    (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).f ≫
      𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₂

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
rw :
  X.pOpcycles f₁ f₂₃ n₁ ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ =
    (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁
rw₁ rw₂ :
  (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ ⋯) ≫ X.pOpcycles f₁₂ f₃ n₁ =
    (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁
⊢ X.pOpcycles f₁ f₂₃ n₁ ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ =
    ((X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁) ≫ 𝟙 (X.opcycles f₁₂ f₃ n₁)

Tactic:
rw [Category.comp_id, X.p_opcyclesMap _ _ _ _ _ (twoδ₂Toδ₁ f₁ f₂ f₁₂)]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.ComposableArrows.twoδ₂Toδ₁, CategoryTheory.Abelian.SpectralObject.p_opcyclesMap