ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>hg₂ : S₂.g = 0<GOAL>CategoryTheory.ShortComplex.QuasiIso φ ↔ (CategoryTheory.ShortComplex.mk S₁.f φ.τ₂ ⋯).Exact ∧ CategoryTheory.Epi φ.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>J : C<VAR>f : S.X₂ ⟶ J<VAR>CategoryTheory.Injective J<VAR>hf : CategoryTheory.CategoryStruct.comp S.f f = 0<GOAL>CategoryTheory.CategoryStruct.comp S.g (hS.descToInjective f hf) = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>P : C<VAR>f : P ⟶ S.X₂<VAR>CategoryTheory.Projective P<VAR>hf : CategoryTheory.CategoryStruct.comp f S.g = 0<GOAL>CategoryTheory.CategoryStruct.comp (hS.liftFromProjective f hf) S.f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.HomologyData<GOAL>CategoryTheory.CategoryStruct.comp self.left.π (CategoryTheory.CategoryStruct.comp self.iso.hom self.right.ι) = CategoryTheory.CategoryStruct.comp self.left.i self.right.p
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>h : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<GOAL>CategoryTheory.CategoryStruct.comp h.left.φH h₂.iso.hom = CategoryTheory.CategoryStruct.comp h₁.iso.hom h.right.φH
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>γ₁ γ₂ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<VAR>eq : γ₁ = γ₂<GOAL>γ₁.left.φH = γ₂.left.φH
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S hf c hc).right = CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S hf c hc).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).H
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S hf c hc).left = CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>CategoryTheory.Limits.HasKernel S.g<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofHasKernel S hf).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel S hf).H
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>CategoryTheory.Limits.HasKernel S.g<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofHasKernel S hf).right = CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>CategoryTheory.Limits.HasKernel S.g<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofHasKernel S hf).left = CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel S hf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).right = CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).H
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).left = CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>CategoryTheory.Limits.HasCokernel S.f<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofHasCokernel S hg).left = CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>CategoryTheory.Limits.HasCokernel S.f<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofHasCokernel S hg).right = CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernel S hg
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>CategoryTheory.Limits.HasCokernel S.f<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofHasCokernel S hg).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).H
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).H
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg).right = CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg).left = CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.HomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono φ h).left = CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.HomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono φ h).iso = h.iso
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.HomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono φ h).right = CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.HomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' φ h).right = CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.HomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' φ h).left = CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.HomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' φ h).iso = h.iso
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.H = h.left.H
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIso e h).iso = h.iso
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.i = CategoryTheory.CategoryStruct.comp h.left.i e.hom.τ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.K = h.left.K
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.ι = h.right.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.H = h.right.H
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.p = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv e.hom.τ₂) h.right.p
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.Q = h.right.Q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.π = h.left.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<GOAL>h.op.left = h.right.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<GOAL>h.op.iso = h.iso.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<GOAL>h.op.right = h.left.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.HomologyData<GOAL>h.unop.iso = h.iso.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.HomologyData<GOAL>h.unop.left = h.right.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.HomologyData<GOAL>h.unop.right = h.left.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.HasHomology<GOAL>Nonempty S.HomologyData
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<GOAL>S.HasHomology
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₁.HasHomology<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>S₂.HasHomology
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₂.HasHomology<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>S₁.HasHomology
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>S₁.HasHomology<GOAL>S₂.HasHomology
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyMapData.id h).left = CategoryTheory.ShortComplex.LeftHomologyMapData.id h.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyMapData.id h).right = CategoryTheory.ShortComplex.RightHomologyMapData.id h.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyMapData.zero h₁ h₂).left = CategoryTheory.ShortComplex.LeftHomologyMapData.zero h₁.left h₂.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<GOAL>(CategoryTheory.ShortComplex.HomologyMapData.zero h₁ h₂).right = CategoryTheory.ShortComplex.RightHomologyMapData.zero h₁.right h₂.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>h₃ : S₃.HomologyData<VAR>ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<VAR>ψ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₂ h₃<GOAL>(ψ.comp ψ').left = ψ.left.comp ψ'.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>h₃ : S₃.HomologyData<VAR>ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<VAR>ψ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₂ h₃<GOAL>(ψ.comp ψ').right = ψ.right.comp ψ'.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<GOAL>ψ.op.right = ψ.left.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<GOAL>ψ.op.left = ψ.right.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<GOAL>ψ.unop.right = ψ.left.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<GOAL>ψ.unop.left = ψ.right.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} 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.HomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).right = CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} 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.HomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).left = CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} 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.HomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).left = CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} 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.HomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).right = CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} 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.HomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).right = CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} 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.HomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).left = CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} 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.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork hf hg c hc).right = CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} 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.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork hf hg c hc).left = CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>S.leftHomologyData.homologyIso = S.leftHomologyIso.symm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>S.rightHomologyData.homologyIso = S.rightHomologyIso.symm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<GOAL>CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂ = γ.left.φH
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<GOAL>CategoryTheory.ShortComplex.cyclesMap' φ h₁.left h₂.left = γ.left.φK
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<GOAL>CategoryTheory.ShortComplex.opcyclesMap' φ h₁.right h₂.right = γ.right.φQ