ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).K = c.pt
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).i = CategoryTheory.Limits.Fork.ι c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).H = c.pt
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).π = CategoryTheory.CategoryStruct.id c.pt
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).f' = 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>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).K = S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).π = CategoryTheory.CategoryStruct.id S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).H = S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).i = CategoryTheory.CategoryStruct.id S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).f' = 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>self : S.HasLeftHomology<GOAL>Nonempty S.LeftHomologyData
<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<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>h₂ : S₂.LeftHomologyData<VAR>self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<GOAL>CategoryTheory.CategoryStruct.comp h₁.π self.φH = CategoryTheory.CategoryStruct.comp self.φK 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>self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<GOAL>CategoryTheory.CategoryStruct.comp self.φK 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>h₂ : S₂.LeftHomologyData<VAR>self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<GOAL>CategoryTheory.CategoryStruct.comp h₁.f' self.φK = 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>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.zero h₁ h₂).φK = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.zero h₁ h₂).φH = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.id h).φH = CategoryTheory.CategoryStruct.id h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.id 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₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>h₃ : S₃.LeftHomologyData<VAR>ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>ψ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₂ h₃<GOAL>(ψ.comp ψ').φH = CategoryTheory.CategoryStruct.comp ψ.φH ψ'.φH
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>h₃ : S₃.LeftHomologyData<VAR>ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>ψ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₂ h₃<GOAL>(ψ.comp ψ').φK = CategoryTheory.CategoryStruct.comp ψ.φK ψ'.φ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>h₂ : S₂.LeftHomologyData<VAR>γ₁ γ₂ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>eq : γ₁ = γ₂<GOAL>γ₁.φH = γ₂.φH
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ₁ γ₂ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>eq : γ₁ = γ₂<GOAL>γ₁.φK = γ₂.φ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>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>hg₂ : S₂.g = 0<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φ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>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>hg₂ : S₂.g = 0<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).φH = φ.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>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.LeftHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φ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>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.LeftHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φH = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ 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.LeftHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φH = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hf₁ : S₁.f = 0<VAR>c₁ : CategoryTheory.Limits.KernelFork S₁.g<VAR>hc₁ : CategoryTheory.Limits.IsLimit c₁<VAR>hf₂ : S₂.f = 0<VAR>c₂ : CategoryTheory.Limits.KernelFork S₂.g<VAR>hc₂ : CategoryTheory.Limits.IsLimit c₂<VAR>f : c₁.pt ⟶ c₂.pt<VAR>comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φK = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φH = CategoryTheory.Limits.Cofork.π c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φK = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).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>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.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φH = CategoryTheory.Limits.Fork.ι c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φK = CategoryTheory.Limits.Fork.ι c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<GOAL>CategoryTheory.CategoryStruct.comp S.iCycles S.g = 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.iCycles = S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<VAR>A : C<VAR>f₁ f₂ : S.leftHomology ⟶ A<GOAL>f₁ = f₂ ↔ CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₁ = CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<VAR>A : C<VAR>f₁ f₂ : S.leftHomology ⟶ A<VAR>h : CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₁ = CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₂<GOAL>f₁ = f₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<VAR>A : C<VAR>f₁ f₂ : A ⟶ S.cycles<GOAL>f₁ = f₂ ↔ CategoryTheory.CategoryStruct.comp f₁ S.iCycles = CategoryTheory.CategoryStruct.comp f₂ 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>A : C<VAR>f₁ f₂ : A ⟶ S.cycles<VAR>h : CategoryTheory.CategoryStruct.comp f₁ S.iCycles = CategoryTheory.CategoryStruct.comp f₂ S.iCycles<GOAL>f₁ = f₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<VAR>hg : S.g = 0<GOAL>CategoryTheory.IsIso 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>hg : S.g = 0<GOAL>(S.cyclesIsoX₂ hg).hom = 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>hg : S.g = 0<GOAL>CategoryTheory.CategoryStruct.comp S.iCycles (S.cyclesIsoX₂ hg).inv = CategoryTheory.CategoryStruct.id S.cycles
<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>hg : S.g = 0<GOAL>CategoryTheory.CategoryStruct.comp (S.cyclesIsoX₂ hg).inv S.iCycles = CategoryTheory.CategoryStruct.id S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<VAR>hf : S.f = 0<GOAL>CategoryTheory.IsIso S.leftHomologyπ
<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>hf : S.f = 0<GOAL>(S.cyclesIsoLeftHomology hf).hom = S.leftHomologyπ
<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>hf : S.f = 0<GOAL>CategoryTheory.CategoryStruct.comp S.leftHomologyπ (S.cyclesIsoLeftHomology hf).inv = CategoryTheory.CategoryStruct.id S.cycles
<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>hf : S.f = 0<GOAL>CategoryTheory.CategoryStruct.comp (S.cyclesIsoLeftHomology hf).inv S.leftHomologyπ = CategoryTheory.CategoryStruct.id 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<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) 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>h₂ : S₂.LeftHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h₁.f' (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) = 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>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ 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₁.HasLeftHomology<VAR>S₂.HasLeftHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) S₂.iCycles = CategoryTheory.CategoryStruct.comp S₁.iCycles φ.τ₂
<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₁.HasLeftHomology<VAR>S₂.HasLeftHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.toCycles (CategoryTheory.ShortComplex.cyclesMap φ) = CategoryTheory.CategoryStruct.comp φ.τ₁ 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₁.HasLeftHomology<VAR>S₂.HasLeftHomology<VAR>φ : S₁ ⟶ S₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.leftHomologyπ (CategoryTheory.ShortComplex.leftHomologyMap φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) 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₂<GOAL>CategoryTheory.ShortComplex.leftHomologyMap' φ 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>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<GOAL>CategoryTheory.ShortComplex.cyclesMap' φ h₁ 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>h : S.LeftHomologyData<GOAL>CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.id S) h h = CategoryTheory.CategoryStruct.id h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<GOAL>CategoryTheory.ShortComplex.cyclesMap' (CategoryTheory.CategoryStruct.id S) h h = 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 : CategoryTheory.ShortComplex C<VAR>S.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id S.leftHomology
<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.ShortComplex.cyclesMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id S.cycles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>CategoryTheory.ShortComplex.leftHomologyMap' 0 h₁ h₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>CategoryTheory.ShortComplex.cyclesMap' 0 h₁ h₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.leftHomologyMap 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.cyclesMap 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>h₃ : S₃.LeftHomologyData<GOAL>CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ₁ h₁ h₂) (CategoryTheory.ShortComplex.leftHomologyMap' φ₂ h₂ h₃)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>h₃ : S₃.LeftHomologyData<GOAL>CategoryTheory.ShortComplex.cyclesMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ₁ h₁ h₂) (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₂ S₃ : CategoryTheory.ShortComplex C<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<VAR>S₃.HasLeftHomology<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<GOAL>CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ₁) (CategoryTheory.ShortComplex.leftHomologyMap φ₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<VAR>S₃.HasLeftHomology<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<GOAL>CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ₁) (CategoryTheory.ShortComplex.cyclesMap φ₂)
<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.leftHomologyMapIso' e h₁ h₂).hom = CategoryTheory.ShortComplex.leftHomologyMap' e.hom h₁ h₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>(CategoryTheory.ShortComplex.leftHomologyMapIso' e h₁ h₂).inv = CategoryTheory.ShortComplex.leftHomologyMap' e.inv h₂ h₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>(CategoryTheory.ShortComplex.cyclesMapIso' e h₁ h₂).inv = CategoryTheory.ShortComplex.cyclesMap' e.inv h₂ h₁