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<GOAL>S.HasLeftHomology ↔ S.op.HasRightHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.HasRightHomology ↔ S.op.HasLeftHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<GOAL>S.HasLeftHomology ↔ S.unop.HasRightHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<GOAL>S.HasRightHomology ↔ S.unop.HasLeftHomology
<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>self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<GOAL>CategoryTheory.CategoryStruct.comp self.φH h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι self.φ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>h₂ : S₂.RightHomologyData<VAR>self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<GOAL>CategoryTheory.CategoryStruct.comp h₁.p self.φQ = 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>h₂ : S₂.RightHomologyData<VAR>self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<GOAL>CategoryTheory.CategoryStruct.comp self.φQ 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>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.zero h₁ h₂).φQ = 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>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.zero h₁ h₂).φH = 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>h : S.RightHomologyData<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.id 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 : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.id 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₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>h₃ : S₃.RightHomologyData<VAR>ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>ψ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₂ h₃<GOAL>(ψ.comp ψ').φH = CategoryTheory.CategoryStruct.comp ψ.φH ψ'.φH
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>h₃ : S₃.RightHomologyData<VAR>ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>ψ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₂ h₃<GOAL>(ψ.comp ψ').φQ = CategoryTheory.CategoryStruct.comp ψ.φQ ψ'.φ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>h₂ : S₂.RightHomologyData<VAR>γ₁ γ₂ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>eq : γ₁ = γ₂<GOAL>γ₁.φ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>h₂ : S₂.RightHomologyData<VAR>γ₁ γ₂ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>eq : γ₁ = γ₂<GOAL>γ₁.φQ = γ₂.φ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>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>hg₂ : S₂.g = 0<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φ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>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>hg₂ : S₂.g = 0<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φ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>hf₁ : S₁.f = 0<VAR>c₁ : CategoryTheory.Limits.KernelFork S₁.g<VAR>hc₁ : CategoryTheory.Limits.IsLimit c₁<VAR>hf₂ : S₂.f = 0<VAR>c₂ : CategoryTheory.Limits.KernelFork S₂.g<VAR>hc₂ : CategoryTheory.Limits.IsLimit c₂<VAR>f : c₁.pt ⟶ c₂.pt<VAR>comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φH = f
<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>hf₁ : S₁.f = 0<VAR>c₁ : CategoryTheory.Limits.KernelFork S₁.g<VAR>hc₁ : CategoryTheory.Limits.IsLimit c₁<VAR>hf₂ : S₂.f = 0<VAR>c₂ : CategoryTheory.Limits.KernelFork S₂.g<VAR>hc₂ : CategoryTheory.Limits.IsLimit c₂<VAR>f : c₁.pt ⟶ c₂.pt<VAR>comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φ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>hg₁ : S₁.g = 0<VAR>c₁ : CategoryTheory.Limits.CokernelCofork S₁.f<VAR>hc₁ : CategoryTheory.Limits.IsColimit c₁<VAR>hg₂ : S₂.g = 0<VAR>c₂ : CategoryTheory.Limits.CokernelCofork S₂.f<VAR>hc₂ : CategoryTheory.Limits.IsColimit c₂<VAR>f : c₁.pt ⟶ c₂.pt<VAR>comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φQ = f
<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>hg₁ : S₁.g = 0<VAR>c₁ : CategoryTheory.Limits.CokernelCofork S₁.f<VAR>hc₁ : CategoryTheory.Limits.IsColimit c₁<VAR>hg₂ : S₂.g = 0<VAR>c₂ : CategoryTheory.Limits.CokernelCofork S₂.f<VAR>hc₂ : CategoryTheory.Limits.IsColimit c₂<VAR>f : c₁.pt ⟶ c₂.pt<VAR>comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φH = 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>hf : S.f = 0<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φQ = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).Q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φH = CategoryTheory.Limits.Fork.ι c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φH = CategoryTheory.Limits.Cofork.π c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φQ = CategoryTheory.Limits.Cofork.π c
<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.f S.pOpcycles = 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.pOpcycles S.fromOpcycles = S.g
<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>A : C<VAR>f₁ f₂ : A ⟶ S.rightHomology<GOAL>f₁ = f₂ ↔ CategoryTheory.CategoryStruct.comp f₁ S.rightHomologyι = CategoryTheory.CategoryStruct.comp f₂ S.rightHomologyι
<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>A : C<VAR>f₁ f₂ : A ⟶ S.rightHomology<VAR>h : CategoryTheory.CategoryStruct.comp f₁ S.rightHomologyι = CategoryTheory.CategoryStruct.comp f₂ S.rightHomologyι<GOAL>f₁ = 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>A : C<VAR>f₁ f₂ : S.opcycles ⟶ A<GOAL>f₁ = f₂ ↔ CategoryTheory.CategoryStruct.comp S.pOpcycles f₁ = CategoryTheory.CategoryStruct.comp S.pOpcycles 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>A : C<VAR>f₁ f₂ : S.opcycles ⟶ A<VAR>h : CategoryTheory.CategoryStruct.comp S.pOpcycles f₁ = CategoryTheory.CategoryStruct.comp S.pOpcycles f₂<GOAL>f₁ = 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>hf : S.f = 0<GOAL>CategoryTheory.IsIso 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>S.HasRightHomology<VAR>hf : S.f = 0<GOAL>(S.opcyclesIsoX₂ hf).inv = 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>S.HasRightHomology<VAR>hf : S.f = 0<GOAL>CategoryTheory.CategoryStruct.comp S.pOpcycles (S.opcyclesIsoX₂ hf).hom = CategoryTheory.CategoryStruct.id S.X₂
<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>hf : S.f = 0<GOAL>CategoryTheory.CategoryStruct.comp (S.opcyclesIsoX₂ hf).hom S.pOpcycles = CategoryTheory.CategoryStruct.id S.opcycles
<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>hg : S.g = 0<GOAL>CategoryTheory.IsIso S.rightHomologyι
<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>hg : S.g = 0<GOAL>(S.opcyclesIsoRightHomology hg).inv = S.rightHomologyι
<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>hg : S.g = 0<GOAL>CategoryTheory.CategoryStruct.comp S.rightHomologyι (S.opcyclesIsoRightHomology hg).hom = CategoryTheory.CategoryStruct.id S.rightHomology
<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>hg : S.g = 0<GOAL>CategoryTheory.CategoryStruct.comp (S.opcyclesIsoRightHomology hg).hom S.rightHomologyι = CategoryTheory.CategoryStruct.id S.opcycles
<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.CategoryStruct.comp h₁.p (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) = 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>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) 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>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι (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₁.HasRightHomology<VAR>S₂.HasRightHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.pOpcycles (CategoryTheory.ShortComplex.opcyclesMap φ) = CategoryTheory.CategoryStruct.comp φ.τ₂ S₂.pOpcycles
<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₁.HasRightHomology<VAR>S₂.HasRightHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) S₂.fromOpcycles = CategoryTheory.CategoryStruct.comp 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₁.HasRightHomology<VAR>S₂.HasRightHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) S₂.rightHomologyι = CategoryTheory.CategoryStruct.comp S₁.rightHomologyι (CategoryTheory.ShortComplex.opcyclesMap φ)
<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>CategoryTheory.ShortComplex.rightHomologyMap' φ 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>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<GOAL>CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂ = γ.φQ
<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<GOAL>CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.id S) 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 : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<GOAL>CategoryTheory.ShortComplex.opcyclesMap' (CategoryTheory.CategoryStruct.id S) h h = 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 : CategoryTheory.ShortComplex C<VAR>S.HasRightHomology<GOAL>CategoryTheory.ShortComplex.rightHomologyMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id S.rightHomology
<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.ShortComplex.opcyclesMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id S.opcycles
<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>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.ShortComplex.rightHomologyMap' 0 h₁ h₂ = 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>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.ShortComplex.opcyclesMap' 0 h₁ h₂ = 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>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.rightHomologyMap 0 = 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>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.opcyclesMap 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>h₃ : S₃.RightHomologyData<GOAL>CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ₁ h₁ h₂) (CategoryTheory.ShortComplex.rightHomologyMap' φ₂ h₂ h₃)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>h₃ : S₃.RightHomologyData<GOAL>CategoryTheory.ShortComplex.opcyclesMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ₁ h₁ h₂) (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₂ S₃ : CategoryTheory.ShortComplex C<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<VAR>S₃.HasRightHomology<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<GOAL>CategoryTheory.ShortComplex.rightHomologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ₁) (CategoryTheory.ShortComplex.rightHomologyMap φ₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<VAR>S₃.HasRightHomology<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<GOAL>CategoryTheory.ShortComplex.opcyclesMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ₁) (CategoryTheory.ShortComplex.opcyclesMap φ₂)
<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>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>(CategoryTheory.ShortComplex.rightHomologyMapIso' e h₁ h₂).inv = CategoryTheory.ShortComplex.rightHomologyMap' e.inv 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>e : S₁ ≅ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>(CategoryTheory.ShortComplex.rightHomologyMapIso' e h₁ h₂).hom = CategoryTheory.ShortComplex.rightHomologyMap' e.hom 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>e : S₁ ≅ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>(CategoryTheory.ShortComplex.opcyclesMapIso' e h₁ h₂).inv = CategoryTheory.ShortComplex.opcyclesMap' e.inv 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>e : S₁ ≅ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>(CategoryTheory.ShortComplex.opcyclesMapIso' e h₁ h₂).hom = CategoryTheory.ShortComplex.opcyclesMap' e.hom 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>e : S₁ ≅ S₂<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>(CategoryTheory.ShortComplex.rightHomologyMapIso e).inv = CategoryTheory.ShortComplex.rightHomologyMap e.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>e : S₁ ≅ S₂<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>(CategoryTheory.ShortComplex.rightHomologyMapIso e).hom = CategoryTheory.ShortComplex.rightHomologyMap e.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>e : S₁ ≅ S₂<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>(CategoryTheory.ShortComplex.opcyclesMapIso e).hom = CategoryTheory.ShortComplex.opcyclesMap e.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>e : S₁ ≅ S₂<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>(CategoryTheory.ShortComplex.opcyclesMapIso e).inv = CategoryTheory.ShortComplex.opcyclesMap e.inv
<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.p h.opcyclesIso.inv = 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>h : S.RightHomologyData<VAR>S.HasRightHomology<GOAL>CategoryTheory.CategoryStruct.comp S.pOpcycles h.opcyclesIso.hom = h.p
<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.inv S.rightHomologyι = CategoryTheory.CategoryStruct.comp h.ι h.opcyclesIso.inv