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₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>(CategoryTheory.ShortComplex.cyclesMapIso' e h₁ h₂).hom = CategoryTheory.ShortComplex.cyclesMap' 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₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>(CategoryTheory.ShortComplex.leftHomologyMapIso e).inv = CategoryTheory.ShortComplex.leftHomologyMap 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₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>(CategoryTheory.ShortComplex.leftHomologyMapIso e).hom = CategoryTheory.ShortComplex.leftHomologyMap 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₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>(CategoryTheory.ShortComplex.cyclesMapIso e).hom = CategoryTheory.ShortComplex.cyclesMap 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₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>(CategoryTheory.ShortComplex.cyclesMapIso e).inv = CategoryTheory.ShortComplex.cyclesMap 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.LeftHomologyData<VAR>S.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp h.cyclesIso.hom h.i = S.iCycles
<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.LeftHomologyData<VAR>S.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp h.cyclesIso.inv S.iCycles = h.i
<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.LeftHomologyData<VAR>S.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp S.leftHomologyπ h.leftHomologyIso.hom = CategoryTheory.CategoryStruct.comp h.cyclesIso.hom 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.LeftHomologyData<VAR>S.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp h.π h.leftHomologyIso.inv = CategoryTheory.CategoryStruct.comp h.cyclesIso.inv S.leftHomologyπ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.leftHomologyMap φ = CategoryTheory.CategoryStruct.comp h₁.leftHomologyIso.hom (CategoryTheory.CategoryStruct.comp γ.φH h₂.leftHomologyIso.inv)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.cyclesMap φ = CategoryTheory.CategoryStruct.comp h₁.cyclesIso.hom (CategoryTheory.CategoryStruct.comp γ.φK h₂.cyclesIso.inv)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ) h₂.leftHomologyIso.hom = CategoryTheory.CategoryStruct.comp h₁.leftHomologyIso.hom γ.φH
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) h₂.cyclesIso.hom = CategoryTheory.CategoryStruct.comp h₁.cyclesIso.hom γ.φK
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.leftHomologyFunctor C).obj S = S.leftHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<GOAL>∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), (CategoryTheory.ShortComplex.leftHomologyFunctor C).map φ = CategoryTheory.ShortComplex.leftHomologyMap φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.cyclesFunctor C).obj S = S.cycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<GOAL>∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), (CategoryTheory.ShortComplex.cyclesFunctor C).map φ = CategoryTheory.ShortComplex.cyclesMap φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.leftHomologyπNatTrans C).app S = S.leftHomologyπ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.iCyclesNatTrans C).app S = S.iCycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.toCyclesNatTrans C).app S = S.toCycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h).H = h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h).π = h.π
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h).K = h.K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h).i = CategoryTheory.CategoryStruct.comp h.i φ.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h).f' = 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>h : S₂.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).i = CategoryTheory.CategoryStruct.comp h.i (CategoryTheory.inv φ.τ₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).H = h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).π = h.π
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).K = h.K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).f' = CategoryTheory.CategoryStruct.comp φ.τ₁ 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>S₁.HasLeftHomology<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>S₂.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>S₂.HasLeftHomology<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>S₁.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>e : S₁ ≅ S₂<VAR>S₁.HasLeftHomology<GOAL>S₂.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₁.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h).φK = CategoryTheory.CategoryStruct.id h.K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h).φH = CategoryTheory.CategoryStruct.id h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono' φ h).φH = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono' φ h).φK = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : CategoryTheory.CategoryStruct.comp k S.g = 0<VAR>S.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) S.iCycles = k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : CategoryTheory.CategoryStruct.comp k S.g = 0<VAR>S.HasLeftHomology<VAR>A' : C<VAR>α : A' ⟶ A<GOAL>CategoryTheory.CategoryStruct.comp α (S.liftCycles k hk) = S.liftCycles (CategoryTheory.CategoryStruct.comp α k) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<VAR>CategoryTheory.Limits.HasKernel S.g<GOAL>S.cyclesIsoKernel.hom = CategoryTheory.Limits.kernel.lift S.g S.iCycles ⋯
<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.HasLeftHomology<VAR>CategoryTheory.Limits.HasKernel S.g<GOAL>S.cyclesIsoKernel.inv = S.liftCycles (CategoryTheory.Limits.kernel.ι 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>A : C<VAR>k : A ⟶ S.X₂<VAR>S.HasLeftHomology<VAR>x : A ⟶ S.X₁<VAR>hx : k = CategoryTheory.CategoryStruct.comp x S.f<GOAL>CategoryTheory.CategoryStruct.comp (S.liftCycles k ⋯) S.leftHomologyπ = 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.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp S.toCycles S.leftHomologyπ = 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₁ : CategoryTheory.ShortComplex C<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : CategoryTheory.CategoryStruct.comp k S.g = 0<VAR>S.HasLeftHomology<VAR>φ : S ⟶ S₁<VAR>S₁.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) (CategoryTheory.ShortComplex.cyclesMap φ) = S₁.liftCycles (CategoryTheory.CategoryStruct.comp k φ.τ₂) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : CategoryTheory.CategoryStruct.comp k S.g = 0<VAR>S.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) h.cyclesIso.hom = h.liftK k hk
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : CategoryTheory.CategoryStruct.comp k S.g = 0<VAR>S.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp (h.liftK k hk) h.cyclesIso.inv = S.liftCycles k hk
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<GOAL>CategoryTheory.Limits.HasKernel 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.HasLeftHomology<VAR>CategoryTheory.Limits.HasKernel S.g<GOAL>CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.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>h₂ : CategoryTheory.IsIso φ.τ₂<VAR>h₃ : CategoryTheory.Mono φ.τ₃<VAR>h₁ : S₁.LeftHomologyData<GOAL>∀ (h₂ : S₂.LeftHomologyData), CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₂ : CategoryTheory.IsIso φ.τ₂<VAR>h₃ : CategoryTheory.Mono φ.τ₃<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap φ)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(CochainComplex.mappingConeCompTriangle f g).mor₂ = CochainComplex.mappingCone.map (f ≫ g) g f (𝟙 X₃) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(CochainComplex.mappingConeCompTriangle f g).obj₁ = CochainComplex.mappingCone f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(CochainComplex.mappingConeCompTriangle f g).mor₁ = CochainComplex.mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(CochainComplex.mappingConeCompTriangle f g).obj₂ = CochainComplex.mappingCone (f ≫ g)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(CochainComplex.mappingConeCompTriangle f g).obj₃ = CochainComplex.mappingCone g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(CochainComplex.mappingConeCompTriangle f g).mor₃ = (CochainComplex.mappingCone.triangle g).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.inr f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>Y₁ Y₂ Y₃ : CochainComplex C ℤ<VAR>f' : Y₁ ⟶ Y₂<VAR>g' : Y₂ ⟶ Y₃<VAR>φ : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g'<GOAL>CochainComplex.mappingCone.map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (CochainComplex.mappingConeCompTriangle f' g').mor₃ = (CochainComplex.mappingConeCompTriangle f g).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.map f f' (φ.app 0) (φ.app 1) ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>CochainComplex.MappingConeCompHomotopyEquiv.hom f g ≫ CochainComplex.MappingConeCompHomotopyEquiv.inv f g = 𝟙 (CochainComplex.mappingCone g)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(CochainComplex.mappingConeCompHomotopyEquiv f g).hom ≫ (CochainComplex.mappingConeCompHomotopyEquiv f g).inv = 𝟙 (CochainComplex.mappingCone g)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>CochainComplex.mappingCone.inr (CochainComplex.mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯) ≫ (CochainComplex.mappingConeCompHomotopyEquiv f g).inv = (CochainComplex.mappingConeCompTriangle f g).mor₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(CochainComplex.mappingConeCompHomotopyEquiv f g).hom ≫ (CochainComplex.mappingCone.triangle (CochainComplex.mappingConeCompTriangle f g).mor₁).mor₃ = (CochainComplex.mappingConeCompTriangle f g).mor₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(CochainComplex.mappingConeCompTriangleh f g).mor₂ ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingConeCompHomotopyEquiv f g).hom = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr (CochainComplex.mappingConeCompTriangle f g).mor₁)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>CochainComplex.mappingConeCompTriangleh f g ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>∀ (a : Fin (1 + 1 + 1)), S.toComposableArrows.obj a = CategoryTheory.ComposableArrows.Precomp.obj (CategoryTheory.ComposableArrows.mk₁ S.g) S.X₁ a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>∀ {X Y : Fin (1 + 1 + 1)} (g : X ⟶ Y), S.toComposableArrows.map g = CategoryTheory.ComposableArrows.Precomp.map (CategoryTheory.ComposableArrows.mk₁ S.g) S.f X Y ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S : CategoryTheory.ComposableArrows C n<VAR>self : S.IsComplex<VAR>i : ℕ<VAR>hi : i + 2 ≤ n := by omega<GOAL>CategoryTheory.CategoryStruct.comp (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ hi) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S : CategoryTheory.ComposableArrows C n<VAR>hS : S.IsComplex<VAR>i j k : ℕ<VAR>hij : i + 1 = j := by omega<VAR>hjk : j + 1 = k := by omega<VAR>hk : k ≤ n := by omega<GOAL>CategoryTheory.CategoryStruct.comp (S.map' i j ⋯ ⋯) (S.map' j k ⋯ hk) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.IsComplex<GOAL>S₂.IsComplex
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>e : S₁ ≅ S₂<GOAL>S₁.IsComplex ↔ S₂.IsComplex
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ComposableArrows C 0<GOAL>S.IsComplex