ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>S.HasRightHomology<GOAL>CategoryTheory.CategoryStruct.comp h.rightHomologyIso.hom h.ι = CategoryTheory.CategoryStruct.comp S.rightHomologyι h.opcyclesIso.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.rightHomologyMap φ = CategoryTheory.CategoryStruct.comp h₁.rightHomologyIso.hom (CategoryTheory.CategoryStruct.comp γ.φH h₂.rightHomologyIso.inv)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.opcyclesMap φ = CategoryTheory.CategoryStruct.comp h₁.opcyclesIso.hom (CategoryTheory.CategoryStruct.comp γ.φQ h₂.opcyclesIso.inv)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) h₂.rightHomologyIso.hom = CategoryTheory.CategoryStruct.comp h₁.rightHomologyIso.hom γ.φH
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) h₂.opcyclesIso.hom = CategoryTheory.CategoryStruct.comp h₁.opcyclesIso.hom γ.φQ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.rightHomologyFunctor C).obj S = S.rightHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<GOAL>∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), (CategoryTheory.ShortComplex.rightHomologyFunctor C).map φ = CategoryTheory.ShortComplex.rightHomologyMap φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.opcyclesFunctor C).obj S = S.opcycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<GOAL>∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), (CategoryTheory.ShortComplex.opcyclesFunctor C).map φ = CategoryTheory.ShortComplex.opcyclesMap φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.rightHomologyιNatTrans C).app S = S.rightHomologyι
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.pOpcyclesNatTrans C).app S = S.pOpcycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.fromOpcyclesNatTrans C).app S = S.fromOpcycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<GOAL>ψ.op.φQ = ψ.φK.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<GOAL>ψ.op.φH = ψ.φH.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<GOAL>ψ.unop.φQ = ψ.φK.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<GOAL>ψ.unop.φH = ψ.φH.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<GOAL>ψ.op.φH = ψ.φH.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<GOAL>ψ.op.φK = ψ.φQ.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<GOAL>ψ.unop.φK = ψ.φQ.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<GOAL>ψ.unop.φH = ψ.φH.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>(CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂).op = CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.ShortComplex.opMap φ) h₂.op h₁.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>(CategoryTheory.ShortComplex.leftHomologyMap φ).op = CategoryTheory.CategoryStruct.comp S₂.rightHomologyOpIso.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap (CategoryTheory.ShortComplex.opMap φ)) S₁.rightHomologyOpIso.hom)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>(CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂).op = CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.ShortComplex.opMap φ) h₂.op h₁.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>(CategoryTheory.ShortComplex.rightHomologyMap φ).op = CategoryTheory.CategoryStruct.comp S₂.leftHomologyOpIso.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.ShortComplex.opMap φ)) S₁.leftHomologyOpIso.hom)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).Q = h.Q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).H = h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).p = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv φ.τ₂) h.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).ι = h.ι
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).g' = CategoryTheory.CategoryStruct.comp h.g' φ.τ₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).Q = h.Q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).H = h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).p = CategoryTheory.CategoryStruct.comp φ.τ₂ h.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).ι = h.ι
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).g' φ.τ₃ = h.g'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₁.HasRightHomology<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>S₂.HasRightHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₂.HasRightHomology<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>S₁.HasRightHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>S₁.HasRightHomology<GOAL>S₂.HasRightHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono φ h).φQ = CategoryTheory.CategoryStruct.id h.Q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono φ h).φH = CategoryTheory.CategoryStruct.id h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono' φ h).φQ = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).Q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.RightHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono' φ h).φH = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>CategoryTheory.Limits.HasKernels Cᵒᵖ<VAR>CategoryTheory.Limits.HasCokernels Cᵒᵖ<VAR>X : (CategoryTheory.ShortComplex C)ᵒᵖ<GOAL>(CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso C).hom.app X = (Opposite.unop X).leftHomologyOpIso.inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>CategoryTheory.Limits.HasKernels Cᵒᵖ<VAR>CategoryTheory.Limits.HasCokernels Cᵒᵖ<VAR>X : (CategoryTheory.ShortComplex C)ᵒᵖ<GOAL>(CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso C).inv.app X = (Opposite.unop X).leftHomologyOpIso.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>CategoryTheory.Limits.HasKernels Cᵒᵖ<VAR>CategoryTheory.Limits.HasCokernels Cᵒᵖ<VAR>X : (CategoryTheory.ShortComplex C)ᵒᵖ<GOAL>(CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso C).hom.app X = (Opposite.unop X).rightHomologyOpIso.inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>CategoryTheory.Limits.HasKernels Cᵒᵖ<VAR>CategoryTheory.Limits.HasCokernels Cᵒᵖ<VAR>X : (CategoryTheory.ShortComplex C)ᵒᵖ<GOAL>(CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso C).inv.app X = (Opposite.unop X).rightHomologyOpIso.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : CategoryTheory.CategoryStruct.comp S.f k = 0<VAR>S.HasRightHomology<GOAL>CategoryTheory.CategoryStruct.comp S.pOpcycles (S.descOpcycles k hk) = k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : CategoryTheory.CategoryStruct.comp S.f k = 0<VAR>S.HasRightHomology<VAR>A' : C<VAR>α : A ⟶ A'<GOAL>CategoryTheory.CategoryStruct.comp (S.descOpcycles k hk) α = S.descOpcycles (CategoryTheory.CategoryStruct.comp k α) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasRightHomology<VAR>CategoryTheory.Limits.HasCokernel S.f<GOAL>S.opcyclesIsoCokernel.hom = S.descOpcycles (CategoryTheory.Limits.cokernel.π S.f) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasRightHomology<VAR>CategoryTheory.Limits.HasCokernel S.f<GOAL>S.opcyclesIsoCokernel.inv = CategoryTheory.Limits.cokernel.desc S.f S.pOpcycles ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>S.HasRightHomology<VAR>x : S.X₃ ⟶ A<VAR>hx : k = CategoryTheory.CategoryStruct.comp S.g x<GOAL>CategoryTheory.CategoryStruct.comp S.rightHomologyι (S.descOpcycles k ⋯) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasRightHomology<GOAL>CategoryTheory.CategoryStruct.comp S.rightHomologyι S.fromOpcycles = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S S₁ : CategoryTheory.ShortComplex C<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : CategoryTheory.CategoryStruct.comp S.f k = 0<VAR>S.HasRightHomology<VAR>φ : S₁ ⟶ S<VAR>S₁.HasRightHomology<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) (S.descOpcycles k hk) = S₁.descOpcycles (CategoryTheory.CategoryStruct.comp φ.τ₂ k) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : CategoryTheory.CategoryStruct.comp S.f k = 0<VAR>S.HasRightHomology<GOAL>CategoryTheory.CategoryStruct.comp h.opcyclesIso.inv (S.descOpcycles k hk) = h.descQ k hk
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : CategoryTheory.CategoryStruct.comp S.f k = 0<VAR>S.HasRightHomology<GOAL>CategoryTheory.CategoryStruct.comp h.opcyclesIso.hom (h.descQ k hk) = S.descOpcycles k hk
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasRightHomology<GOAL>CategoryTheory.Limits.HasCokernel S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasRightHomology<VAR>CategoryTheory.Limits.HasCokernel S.f<GOAL>CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₂ : CategoryTheory.IsIso φ.τ₂<VAR>h₁ : CategoryTheory.Epi φ.τ₁<GOAL>∀ (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData), CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₂ : CategoryTheory.IsIso φ.τ₂<VAR>h₁ : CategoryTheory.Epi φ.τ₁<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap φ)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>CategoryTheory.Limits.biprod.inl ≫ (K.biprodXIso L i).inv = CategoryTheory.Limits.biprod.inl.f i
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>CategoryTheory.Limits.biprod.inr ≫ (K.biprodXIso L i).inv = CategoryTheory.Limits.biprod.inr.f i
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>(K.biprodXIso L i).hom ≫ CategoryTheory.Limits.biprod.fst = CategoryTheory.Limits.biprod.fst.f i
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>(K.biprodXIso L i).hom ≫ CategoryTheory.Limits.biprod.snd = CategoryTheory.Limits.biprod.snd.f i
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>CategoryTheory.Limits.biprod.inl.f i ≫ CategoryTheory.Limits.biprod.fst.f i = 𝟙 (K.X i)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>CategoryTheory.Limits.biprod.inl.f i ≫ CategoryTheory.Limits.biprod.snd.f i = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>CategoryTheory.Limits.biprod.inr.f i ≫ CategoryTheory.Limits.biprod.fst.f i = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>CategoryTheory.Limits.biprod.inr.f i ≫ CategoryTheory.Limits.biprod.snd.f i = 𝟙 (L.X i)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)<VAR>M : HomologicalComplex C c<VAR>α : K ⟶ M<VAR>β : L ⟶ M<VAR>i : ι<GOAL>CategoryTheory.Limits.biprod.inl.f i ≫ (CategoryTheory.Limits.biprod.desc α β).f i = α.f i