ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.Exact<GOAL>S.unop.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.op.Exact ↔ S.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<GOAL>S.unop.Exact ↔ S.Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<VAR>(S.map F).HasHomology<GOAL>(S.map F).Exact ↔ CategoryTheory.Limits.IsZero (F.obj h.H)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<VAR>(S.map F).HasHomology<GOAL>(S.map F).Exact ↔ CategoryTheory.Limits.IsZero (F.obj h.H)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Exact<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>F.PreservesLeftHomologyOf S<VAR>(S.map F).HasHomology<GOAL>(S.map F).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Exact<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>F.PreservesRightHomologyOf S<VAR>(S.map F).HasHomology<GOAL>(S.map F).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Exact<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>F.PreservesLeftHomologyOf S<VAR>F.PreservesRightHomologyOf S<GOAL>(S.map F).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>F.PreservesLeftHomologyOf S<VAR>F.PreservesRightHomologyOf S<VAR>F.Faithful<GOAL>(S.map F).Exact ↔ S.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Exact<VAR>X Y : C<VAR>a : X ⟶ S.X₂<VAR>ha : CategoryTheory.CategoryStruct.comp a S.g = 0<VAR>b : S.X₂ ⟶ Y<VAR>hb : CategoryTheory.CategoryStruct.comp S.f b = 0<GOAL>CategoryTheory.CategoryStruct.comp a b = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>ex : S.Exact<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>CategoryTheory.Limits.IsZero S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>hf : S.f = 0<GOAL>S.Exact ↔ CategoryTheory.Mono S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>hg : S.g = 0<GOAL>S.Exact ↔ CategoryTheory.Epi S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>h : S.LeftHomologyData<GOAL>CategoryTheory.Epi h.f'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>h : S.RightHomologyData<GOAL>CategoryTheory.Mono h.g'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>S.HasLeftHomology<GOAL>CategoryTheory.Epi S.toCycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>S.HasRightHomology<GOAL>CategoryTheory.Mono S.fromOpcycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.LeftHomologyData<GOAL>S.Exact ↔ CategoryTheory.Epi h.f'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.RightHomologyData<GOAL>S.Exact ↔ CategoryTheory.Mono h.g'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>kf : CategoryTheory.Limits.KernelFork S.g<VAR>hkf : CategoryTheory.Limits.IsLimit kf<GOAL>(hS.leftHomologyDataOfIsLimitKernelFork kf hkf).i = CategoryTheory.Limits.Fork.ι kf
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>kf : CategoryTheory.Limits.KernelFork S.g<VAR>hkf : CategoryTheory.Limits.IsLimit kf<GOAL>(hS.leftHomologyDataOfIsLimitKernelFork kf hkf).π = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>kf : CategoryTheory.Limits.KernelFork S.g<VAR>hkf : CategoryTheory.Limits.IsLimit kf<GOAL>(hS.leftHomologyDataOfIsLimitKernelFork kf hkf).H = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>kf : CategoryTheory.Limits.KernelFork S.g<VAR>hkf : CategoryTheory.Limits.IsLimit kf<GOAL>(hS.leftHomologyDataOfIsLimitKernelFork kf hkf).K = kf.pt
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>cc : CategoryTheory.Limits.CokernelCofork S.f<VAR>hcc : CategoryTheory.Limits.IsColimit cc<GOAL>(hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).ι = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>cc : CategoryTheory.Limits.CokernelCofork S.f<VAR>hcc : CategoryTheory.Limits.IsColimit cc<GOAL>(hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).Q = cc.pt
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>cc : CategoryTheory.Limits.CokernelCofork S.f<VAR>hcc : CategoryTheory.Limits.IsColimit cc<GOAL>(hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).p = CategoryTheory.Limits.Cofork.π cc
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>cc : CategoryTheory.Limits.CokernelCofork S.f<VAR>hcc : CategoryTheory.Limits.IsColimit cc<GOAL>(hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).H = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>S.Exact ↔ CategoryTheory.Epi S.toCycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>S.Exact ↔ CategoryTheory.Mono S.fromOpcycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>CategoryTheory.Limits.HasKernel S.g<GOAL>S.Exact ↔ CategoryTheory.Epi (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>CategoryTheory.Limits.HasCokernel S.f<GOAL>S.Exact ↔ CategoryTheory.Mono (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>CategoryTheory.ShortComplex.QuasiIso φ<GOAL>S₁.Exact ↔ S₂.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)<VAR>S.HasHomology<GOAL>S.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)<VAR>S.HasHomology<GOAL>S.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>hf : S.f = 0<GOAL>CategoryTheory.Mono S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>hg : S.g = 0<GOAL>CategoryTheory.Epi S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<GOAL>CategoryTheory.Mono S.g ↔ S.f = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<GOAL>CategoryTheory.Epi S.f ↔ S.g = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>CategoryTheory.Limits.IsZero S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<GOAL>CategoryTheory.Limits.IsZero S.X₂ ↔ S.f = 0 ∧ S.g = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.Splitting<GOAL>CategoryTheory.CategoryStruct.comp self.r S.f + CategoryTheory.CategoryStruct.comp S.g self.s = CategoryTheory.CategoryStruct.id S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.Splitting<GOAL>CategoryTheory.CategoryStruct.comp self.s S.g = CategoryTheory.CategoryStruct.id S.X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.Splitting<GOAL>CategoryTheory.CategoryStruct.comp S.f self.r = CategoryTheory.CategoryStruct.id S.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>s : S.Splitting<GOAL>CategoryTheory.CategoryStruct.comp s.r S.f = CategoryTheory.CategoryStruct.id S.X₂ - CategoryTheory.CategoryStruct.comp S.g s.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>s : S.Splitting<GOAL>CategoryTheory.CategoryStruct.comp S.g s.s = CategoryTheory.CategoryStruct.id S.X₂ - CategoryTheory.CategoryStruct.comp s.r S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>s : S.Splitting<GOAL>s.splitMono_f.retraction = s.r
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>s : S.Splitting<GOAL>CategoryTheory.IsSplitMono S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>s : S.Splitting<GOAL>CategoryTheory.Mono S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>s : S.Splitting<GOAL>s.splitEpi_g.section_ = s.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>s : S.Splitting<GOAL>CategoryTheory.IsSplitEpi S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>s : S.Splitting<GOAL>CategoryTheory.Epi S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>s : S.Splitting<GOAL>CategoryTheory.CategoryStruct.comp s.s s.r = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>s s' : S.Splitting<VAR>h : s.r = s'.r<GOAL>s = s'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>s s' : S.Splitting<VAR>h : s.s = s'.s<GOAL>s = s'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>s.leftHomologyData.i = S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>s.leftHomologyData.K = S.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>s.leftHomologyData.π = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>s.leftHomologyData.H = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>s.rightHomologyData.H = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>s.rightHomologyData.p = S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>s.rightHomologyData.Q = S.X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>s.rightHomologyData.ι = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>s.homologyData.right = s.rightHomologyData
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>s.homologyData.iso = CategoryTheory.Iso.refl 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>s.homologyData.left = s.leftHomologyData
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>s : S.Splitting<GOAL>S.Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>S : CategoryTheory.ShortComplex C<VAR>s : S.Splitting<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>(s.map F).r = F.map s.r
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>S : CategoryTheory.ShortComplex C<VAR>s : S.Splitting<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>(s.map F).s = F.map s.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>s : S₁.Splitting<VAR>e : S₁ ≅ S₂<GOAL>(s.ofIso e).r = CategoryTheory.CategoryStruct.comp e.inv.τ₂ (CategoryTheory.CategoryStruct.comp s.r e.hom.τ₁)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>s : S₁.Splitting<VAR>e : S₁ ≅ S₂<GOAL>(s.ofIso e).s = CategoryTheory.CategoryStruct.comp e.inv.τ₃ (CategoryTheory.CategoryStruct.comp s.s e.hom.τ₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Splitting<GOAL>h.op.r = h.s.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Splitting<GOAL>h.op.s = h.r.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.Splitting<GOAL>h.unop.s = h.r.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.Splitting<GOAL>h.unop.r = h.s.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Splitting<VAR>CategoryTheory.Limits.HasBinaryBiproduct S.X₁ S.X₃<GOAL>h.isoBinaryBiproduct.inv = CategoryTheory.Limits.biprod.desc S.f h.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Splitting<VAR>CategoryTheory.Limits.HasBinaryBiproduct S.X₁ S.X₃<GOAL>h.isoBinaryBiproduct.hom = CategoryTheory.Limits.biprod.lift h.r S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>hS : S.Exact<VAR>h : S.LeftHomologyData<VAR>CategoryTheory.Mono S.f<GOAL>CategoryTheory.IsIso h.f'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>hS : S.Exact<VAR>CategoryTheory.Mono S.f<VAR>S.HasLeftHomology<GOAL>CategoryTheory.IsIso S.toCycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>hS : S.Exact<VAR>h : S.RightHomologyData<VAR>CategoryTheory.Epi S.g<GOAL>CategoryTheory.IsIso h.g'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>hS : S.Exact<VAR>CategoryTheory.Epi S.g<VAR>S.HasRightHomology<GOAL>CategoryTheory.IsIso S.fromOpcycles
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>hS : S.Exact<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>(S.map F).HasHomology<GOAL>CategoryTheory.Mono S.f → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F → (S.map F).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>hS : S.Exact<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>(S.map F).HasHomology<GOAL>CategoryTheory.Epi S.g → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F → (S.map F).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>hS : S.Exact<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : CategoryTheory.CategoryStruct.comp k S.g = 0<VAR>CategoryTheory.Mono S.f<GOAL>CategoryTheory.CategoryStruct.comp (hS.lift k hk) S.f = k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>hS : S.Exact<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : CategoryTheory.CategoryStruct.comp k S.g = 0<VAR>CategoryTheory.Mono S.f<GOAL>∃ l, CategoryTheory.CategoryStruct.comp l S.f = k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>hS : S.Exact<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : CategoryTheory.CategoryStruct.comp S.f k = 0<VAR>CategoryTheory.Epi S.g<GOAL>CategoryTheory.CategoryStruct.comp S.g (hS.desc k hk) = k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>hS : S.Exact<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : CategoryTheory.CategoryStruct.comp S.f k = 0<VAR>CategoryTheory.Epi S.g<GOAL>∃ l, CategoryTheory.CategoryStruct.comp S.g l = k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Balanced C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.Exact<VAR>CategoryTheory.Mono S₁.f<VAR>CategoryTheory.Mono S₂.f<VAR>CategoryTheory.Mono φ.τ₁<VAR>CategoryTheory.Mono φ.τ₃<GOAL>CategoryTheory.Mono φ.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Balanced C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₂ : S₂.Exact<VAR>CategoryTheory.Epi S₁.g<VAR>CategoryTheory.Epi S₂.g<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.Epi φ.τ₃<GOAL>CategoryTheory.Epi φ.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>S.HasHomology<GOAL>S.Exact ∧ CategoryTheory.Mono S.f ↔ Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Balanced C<VAR>S.HasHomology<GOAL>S.Exact ∧ CategoryTheory.Epi S.g ↔ Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯))
<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>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<GOAL>CategoryTheory.ShortComplex.QuasiIso φ ↔ (CategoryTheory.ShortComplex.mk φ.τ₂ S₂.g ⋯).Exact ∧ CategoryTheory.Mono φ.τ₂