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 ι
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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
⊢ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).RightHomologyData

Tactic:
exact {
    Q := X.opcycles f₂ f₃ n₁
    H := kernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂)
    p := X.pOpcycles f₂ f₃ n₁
    ι := kernel.ι _
    wp := by simp
    hp := hp
    wι := by rw [this]; simp
    hι := by
      refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
        (kernelIsKernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂))
      · exact parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa) (by simp)
      · exact Fork.ext (Iso.refl _) }
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
⊢ Cofork.π (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) ≫
      (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g' =
    Cofork.π (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) ≫ X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂

Tactic:
simpa using hp.fac _ .one

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingParallelPair.one
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
⊢ (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g' = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂

Tactic:
exact Cofork.IsColimit.hom_ext hp (by simpa using hp.fac _ .one)

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles ≫ (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom =
    X.pOpcycles f₂ f₃ n₁

Tactic:
ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom _

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom, CategoryTheory.Abelian.SpectralObject.opcycles, CategoryTheory.Abelian.SpectralObject.pOpcycles, CategoryTheory.Limits.colimit.ι
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.pOpcycles f₂ f₃ n₁ ≫ (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv =
    (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles

Tactic:
(X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).p_comp_opcyclesIso_inv

Premises used: CategoryTheory.ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv, CategoryTheory.Limits.colimit, CategoryTheory.Abelian.SpectralObject.opcycles, CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex, CategoryTheory.Abelian.SpectralObject.pOpcycles, CategoryTheory.Limits.colimit.ι
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂ =
    (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles

Tactic:
simp [← cancel_epi (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles]

Premises used: CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.Abelian.SpectralObject.shortComplex, 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 ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂ = 0

Tactic:
simp [ιE]

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

Tactic:
simp [πE, ιE]

Premises used: CategoryTheory.Abelian.SpectralObject.ιE, 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 ι
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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Iso.hom
        (Iso.refl
          (ShortComplex.mk (X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology)
              (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyι
              (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles ⋯).X₁) ≫
      (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f =
    (ShortComplex.mk (X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology)
          (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles
          ⋯).f ≫
      (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom

Tactic:
simp [ιE]

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 ι
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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g =
    (ShortComplex.mk (X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology)
          (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles
          ⋯).g ≫
      Iso.hom
        (Iso.refl
          (ShortComplex.mk (X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology)
              (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyι
              (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles ⋯).X₃)

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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).Exact

Tactic:
ShortComplex.exact_of_iso (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).symm
    (ShortComplex.exact_of_f_is_kernel _ (ShortComplex.homologyIsKernel _))

Premises used: CategoryTheory.ShortComplex.homologyIsKernel, CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.ShortComplex.exact_of_f_is_kernel, CategoryTheory.Iso.symm, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso
-- 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 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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
dsimp : Mono (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
⊢ Mono (X.kernelSequenceOpcyclesE f₁ f₂ f₃ 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 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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)

Tactic:
infer_instance
-- 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 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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
dsimp : Epi (Y := 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₂ ⋯ ⋯)
⊢ Epi (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ 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 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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi (Y := 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₂ ⋯ ⋯)

Tactic:
infer_instance
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
rw :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₂),
    x₂ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
        π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
⊢ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).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.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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) 0
⊢ (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) ≫ (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).g = 0

Tactic:
simpa using hx₂
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) 0
obtain :
  ∀ (A₁ : C) (π₁ : A₁ ⟶ A),
    Epi π₁ →
      ∀ (y₁ : A₁ ⟶ (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).X₁)
        (hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f),
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
          π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
    π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
obtain ⟨A₁, π₁, _, y₁, hy₁⟩ :=
    (X.cokernelSequenceCyclesE_exact f₁ f₂ f₃ n₀ n₁ n₂).exact_up_to_refinements
      (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (by simpa using hx₂)

Premises used: CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_exact, CategoryTheory.ShortComplex.Exact.exact_up_to_refinements, CategoryTheory.Abelian.SpectralObject.toCycles, CategoryTheory.CategoryStruct.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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₁ : A₁ ⟶ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
z : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂) := π₁ ≫ x₂ - y₁ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯
⊢ z ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = 0

Tactic:
simp [z, hy₁]
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₁ : A₁ ⟶ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
z : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂) := π₁ ≫ x₂ - y₁ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯
⊢ z ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = 0

Tactic:
have : z ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = 0 := by simp [z, hy₁]
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₁ : A₁ ⟶ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
z : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂) := π₁ ≫ x₂ - y₁ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯
this : z ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = 0
⊢ z ≫ (X.sc₂ f₁ f₂ f₁₂ h₁₂ n₁).g = 0

Tactic:
simpa only [zero_comp, Category.assoc, toCycles_i] using this =≫ X.iCycles f₁ f₂ n₁

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.zero_comp, CategoryTheory.Abelian.SpectralObject.toCycles_i, CategoryTheory.Abelian.SpectralObject.iCycles
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₁ : A₁ ⟶ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
z : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂) := π₁ ≫ x₂ - y₁ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯
obtain :
  ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁),
    Epi π₂ →
      ∀ (x₁ : A₂ ⟶ (X.sc₂ f₁ f₂ f₁₂ h₁₂ n₁).X₁) (hx₁ : π₂ ≫ z = x₁ ≫ (X.sc₂ f₁ f₂ f₁₂ h₁₂ n₁).f),
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
          π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
    π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
obtain ⟨A₂, π₂, _, x₁, hx₁⟩ := (X.exact₂ f₁ f₂ f₁₂ h₁₂ n₁).exact_up_to_refinements z (by
      have : z ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = 0 := by simp [z, hy₁]
      simpa only [zero_comp, Category.assoc, toCycles_i] using this =≫ X.iCycles f₁ f₂ n₁)

Premises used: CategoryTheory.Abelian.SpectralObject.exact₂, CategoryTheory.ShortComplex.Exact.exact_up_to_refinements
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₁ : A₁ ⟶ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
z : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂) := π₁ ≫ x₂ - y₁ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
x₁ : A₂ ⟶ (X.H n₁).obj (mk₁ f₁)
hx₁ : π₂ ≫ z = x₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)
⊢ (π₂ ≫ π₁) ≫ x₂ = biprod.lift x₁ (π₂ ≫ y₁) ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
simp [z, ← hx₁]
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₁ : A₁ ⟶ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
z : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂) := π₁ ≫ x₂ - y₁ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
x₁ : A₂ ⟶ (X.H n₁).obj (mk₁ f₁)
hx₁ : π₂ ≫ z = x₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁),
    π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
exact ⟨A₂, π₂ ≫ π₁, epi_comp _ _, biprod.lift x₁ (π₂ ≫ y₁), by simp [z, ← hx₁]⟩
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f₁₂) ⟶ A
h : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ x = 0
hn₁ : n₀ + 1 = n₁
h' : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ x = 0
hn₂ : n₁ + 1 = n₂
dsimp : X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ ⋯.desc x ⋯ = x
⊢ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ X.descE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ x h hn₁ h' hn₂ = x

Tactic:
dsimp only [descE]

Premises used: CategoryTheory.Abelian.SpectralObject.descE
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f₁₂) ⟶ A
h : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ x = 0
hn₁ : n₀ + 1 = n₁
h' : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ x = 0
hn₂ : n₁ + 1 = n₂
rw : (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) ≫ ⋯.desc x ⋯ = x
⊢ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ ⋯.desc x ⋯ = x

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
A : C
x : (X.H n₁).obj (mk₁ f₁₂) ⟶ A
h : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ x = 0
hn₁ : n₀ + 1 = n₁
h' : X.δ f₁₂ f₃ n₀ n₁ hn₁ ≫ x = 0
hn₂ : n₁ + 1 = n₂
⊢ (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) ≫ ⋯.desc x ⋯ = x

Tactic:
apply (X.cokernelSequenceE_exact f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂).g_desc

Premises used: CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_exact, CategoryTheory.ShortComplex.Exact.g_desc
-- 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 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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h₀ :
  Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f₃))
    (CategoryStruct.comp (Y := biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
      ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
        biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯))
      biprod.fst)
    (CategoryStruct.comp (Y := biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁))) 0 biprod.fst)
h₁ :
  Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ (X.H n₂).obj (mk₁ f₁))
    (CategoryStruct.comp (Y := biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
      ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
        biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯))
      biprod.snd)
    (CategoryStruct.comp (Y := biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁))) 0 biprod.snd)
⊢ Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ biprod.{v_1, u_1} ((X.H n₁).obj (mk₁ f₃)) ((X.H n₂).obj (mk₁ f₁)))
    ((X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
      biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯))
    0

Tactic:
ext