ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>CategoryTheory.ShortComplex.homologyMap φ = CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom (CategoryTheory.CategoryStruct.comp γ.φH h₂.homologyIso.inv)
<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₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h₂.homologyIso.hom = CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom γ.φ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₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>CategoryTheory.ShortComplex.homologyMap φ = CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom (CategoryTheory.CategoryStruct.comp γ.φH h₂.homologyIso.inv)
<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₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h₂.homologyIso.hom = CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom γ.φH
<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.homologyMap' (CategoryTheory.CategoryStruct.id S) h h = CategoryTheory.CategoryStruct.id h.left.H
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>CategoryTheory.ShortComplex.homologyMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id S.homology
<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.homologyMap' 0 h₁ h₂ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>CategoryTheory.ShortComplex.homologyMap 0 = 0
<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<GOAL>CategoryTheory.ShortComplex.homologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap' φ₁ h₁ h₂) (CategoryTheory.ShortComplex.homologyMap' φ₂ h₂ h₃)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>S₃.HasHomology<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<GOAL>CategoryTheory.ShortComplex.homologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ₁) (CategoryTheory.ShortComplex.homologyMap φ₂)
<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<VAR>h₂ : S₂.HomologyData<GOAL>(CategoryTheory.ShortComplex.homologyMapIso' e h₁ h₂).hom = CategoryTheory.ShortComplex.homologyMap' e.hom h₁ 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<VAR>h₂ : S₂.HomologyData<GOAL>(CategoryTheory.ShortComplex.homologyMapIso' e h₁ h₂).inv = CategoryTheory.ShortComplex.homologyMap' e.inv h₂ 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>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>(CategoryTheory.ShortComplex.homologyMapIso e).hom = CategoryTheory.ShortComplex.homologyMap 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>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>(CategoryTheory.ShortComplex.homologyMapIso e).inv = CategoryTheory.ShortComplex.homologyMap e.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<GOAL>CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = h₂.liftH (h₁.descH (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) h₂.ι) = CategoryTheory.CategoryStruct.comp h₁.i h₂.p
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<GOAL>CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = h₁.descH (h₂.liftH (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<VAR>S.HasRightHomology<GOAL>CategoryTheory.CategoryStruct.comp S.leftHomologyπ (CategoryTheory.CategoryStruct.comp S.leftRightHomologyComparison S.rightHomologyι) = CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles
<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₁.LeftHomologyData<VAR>h₂ : S₁.RightHomologyData<VAR>h₁' : S₂.LeftHomologyData<VAR>h₂' : S₂.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₁') (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁' h₂') = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) (CategoryTheory.ShortComplex.rightHomologyMap' φ h₂ h₂')
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h₁ h₁' : S.LeftHomologyData<VAR>h₂ h₂' : S.RightHomologyData<GOAL>CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.id S) h₁ h₁') (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁' h₂') (CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.id S) h₂' h₂))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<VAR>S.HasRightHomology<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<GOAL>S.leftRightHomologyComparison = CategoryTheory.CategoryStruct.comp h₁.leftHomologyIso.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) h₂.rightHomologyIso.inv)
<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.leftRightHomologyComparison' h.left h.right = h.iso.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<VAR>CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂).iso = CategoryTheory.asIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<VAR>CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂).right = h₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<VAR>CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)<GOAL>(CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂).left = h₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<GOAL>CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.id S) h₁ h.left) (CategoryTheory.CategoryStruct.comp h.iso.hom (CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.id S) h.right h₂))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<VAR>S.HasHomology<GOAL>CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv h₂.homologyIso.hom
<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.leftRightHomologyComparison = CategoryTheory.CategoryStruct.comp S.leftHomologyIso.hom S.rightHomologyIso.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<VAR>S.HasHomology<GOAL>h.right.homologyIso = h.left.homologyIso ≪≫ h.iso
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<VAR>CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)<GOAL>S.HasHomology
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<VAR>S.HasRightHomology<VAR>h : CategoryTheory.IsIso S.leftRightHomologyComparison<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₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h₂.homologyIso.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv (CategoryTheory.ShortComplex.homologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) h₂.homologyIso.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.leftHomologyIso.hom (CategoryTheory.ShortComplex.homologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ) S₂.leftHomologyIso.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.leftHomologyIso.inv (CategoryTheory.ShortComplex.leftHomologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) S₂.leftHomologyIso.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h₂.homologyIso.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv (CategoryTheory.ShortComplex.homologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) h₂.homologyIso.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.rightHomologyIso.hom (CategoryTheory.ShortComplex.homologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) S₂.rightHomologyIso.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.rightHomologyIso.inv (CategoryTheory.ShortComplex.rightHomologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) S₂.rightHomologyIso.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>self : CategoryTheory.CategoryWithHomology C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.HasHomology
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.CategoryWithHomology C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.homologyFunctor C).obj S = S.homology
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.CategoryWithHomology C<GOAL>∀ {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.homologyFunctor C).map f = CategoryTheory.ShortComplex.homologyMap f
<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>S₂.HasHomology<VAR>h₁ : CategoryTheory.Epi φ.τ₁<VAR>h₂ : CategoryTheory.IsIso φ.τ₂<VAR>h₃ : CategoryTheory.Mono φ.τ₃<GOAL>CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp S.homologyπ S.leftHomologyIso.inv = S.leftHomologyπ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp S.rightHomologyIso.hom S.homologyι = S.rightHomologyι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp S.toCycles S.homologyπ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp S.homologyι S.fromOpcycles = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>A : C<VAR>S.HasHomology<VAR>k : S.cycles ⟶ A<VAR>hk : CategoryTheory.CategoryStruct.comp S.toCycles k = 0<GOAL>CategoryTheory.CategoryStruct.comp S.homologyπ (S.descHomology k hk) = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>A : C<VAR>S.HasHomology<VAR>k : A ⟶ S.opcycles<VAR>hk : CategoryTheory.CategoryStruct.comp k S.fromOpcycles = 0<GOAL>CategoryTheory.CategoryStruct.comp (S.liftHomology k hk) S.homologyι = 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>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp S₁.homologyπ (CategoryTheory.ShortComplex.homologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) S₂.homologyπ
<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>S₂.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) S₂.homologyι = CategoryTheory.CategoryStruct.comp S₁.homologyι (CategoryTheory.ShortComplex.opcyclesMap φ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp S.homologyπ S.homologyι = CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.LeftHomologyData<GOAL>CategoryTheory.CategoryStruct.comp S.homologyπ h.homologyIso.hom = CategoryTheory.CategoryStruct.comp h.cyclesIso.hom h.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.LeftHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h.π h.homologyIso.inv = CategoryTheory.CategoryStruct.comp h.cyclesIso.inv S.homologyπ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h.homologyIso.inv S.homologyι = CategoryTheory.CategoryStruct.comp h.ι h.opcyclesIso.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h.homologyIso.hom h.ι = CategoryTheory.CategoryStruct.comp S.homologyι h.opcyclesIso.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.LeftHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h.homologyIso.hom h.leftHomologyIso.inv = S.leftHomologyIso.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.LeftHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h.leftHomologyIso.hom h.homologyIso.inv = S.leftHomologyIso.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h.homologyIso.hom h.rightHomologyIso.inv = S.rightHomologyIso.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h.rightHomologyIso.hom h.homologyIso.inv = S.rightHomologyIso.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) (CategoryTheory.CategoryStruct.comp h₂.homologyIso.hom h₂.ι))) = CategoryTheory.CategoryStruct.comp h₁.i (CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.homologyπ (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) S₂.homologyι) = CategoryTheory.CategoryStruct.comp S₁.iCycles (CategoryTheory.CategoryStruct.comp φ.τ₂ S₂.pOpcycles)
<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<GOAL>(CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂).op = CategoryTheory.CategoryStruct.comp h₂.iso.inv.op (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap' (CategoryTheory.ShortComplex.opMap φ) h₂.op h₁.op) h₁.iso.hom.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>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>(CategoryTheory.ShortComplex.homologyMap φ).op = CategoryTheory.CategoryStruct.comp S₂.homologyOpIso.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (CategoryTheory.ShortComplex.opMap φ)) S₁.homologyOpIso.hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>A : C<VAR>S.HasHomology<VAR>k : A ⟶ S.X₂<VAR>x : A ⟶ S.X₁<VAR>hx : k = CategoryTheory.CategoryStruct.comp x S.f<GOAL>CategoryTheory.CategoryStruct.comp (S.liftCycles k ⋯) S.homologyπ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>A : C<VAR>S.HasHomology<VAR>k : S.X₂ ⟶ A<VAR>x : S.X₃ ⟶ A<VAR>hx : k = CategoryTheory.CategoryStruct.comp S.g x<GOAL>CategoryTheory.CategoryStruct.comp S.homologyι (S.descOpcycles k ⋯) = 0
<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>S₂.HasHomology<VAR>h₁ : CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap φ)<VAR>h₂ : CategoryTheory.Epi φ.τ₁<GOAL>CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)