ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>ψ : S₃ ⟶ S₁<GOAL>(h.compLeft ψ).h₃ = CategoryTheory.CategoryStruct.comp ψ.τ₃ h.h₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>ψ : S₂ ⟶ S₃<GOAL>(h.compRight ψ).h₂ = CategoryTheory.CategoryStruct.comp h.h₂ ψ.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>ψ : S₂ ⟶ S₃<GOAL>(h.compRight ψ).h₃ = CategoryTheory.CategoryStruct.comp h.h₃ ψ.τ₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>ψ : S₂ ⟶ S₃<GOAL>(h.compRight ψ).h₀ = CategoryTheory.CategoryStruct.comp h.h₀ ψ.τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>ψ : S₂ ⟶ S₃<GOAL>(h.compRight ψ).h₁ = CategoryTheory.CategoryStruct.comp h.h₁ ψ.τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>ψ₁ ψ₂ : S₂ ⟶ S₃<VAR>h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂<GOAL>(h.comp h').h₀ = CategoryTheory.CategoryStruct.comp h.h₀ ψ₁.τ₁ + CategoryTheory.CategoryStruct.comp φ₂.τ₁ h'.h₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>ψ₁ ψ₂ : S₂ ⟶ S₃<VAR>h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂<GOAL>(h.comp h').h₁ = CategoryTheory.CategoryStruct.comp h.h₁ ψ₁.τ₁ + CategoryTheory.CategoryStruct.comp φ₂.τ₂ h'.h₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>ψ₁ ψ₂ : S₂ ⟶ S₃<VAR>h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂<GOAL>(h.comp h').h₃ = CategoryTheory.CategoryStruct.comp h.h₃ ψ₁.τ₃ + CategoryTheory.CategoryStruct.comp φ₂.τ₃ h'.h₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>ψ₁ ψ₂ : S₂ ⟶ S₃<VAR>h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂<GOAL>(h.comp h').h₂ = CategoryTheory.CategoryStruct.comp h.h₂ ψ₁.τ₂ + CategoryTheory.CategoryStruct.comp φ₂.τ₃ h'.h₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.op.h₃ = h.h₀.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.op.h₁ = h.h₂.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.op.h₀ = h.h₃.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.op.h₂ = h.h₁.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.unop.h₂ = h.h₁.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.unop.h₃ = h.h₀.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.unop.h₁ = h.h₂.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.unop.h₀ = h.h₃.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>(CategoryTheory.ShortComplex.Homotopy.equivSubZero φ₁ φ₂) h = (h.sub (CategoryTheory.ShortComplex.Homotopy.refl φ₂)).trans (CategoryTheory.ShortComplex.Homotopy.ofEq ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy (φ₁ - φ₂) 0<GOAL>(CategoryTheory.ShortComplex.Homotopy.equivSubZero φ₁ φ₂).symm h = ((CategoryTheory.ShortComplex.Homotopy.ofEq ⋯).trans (h.add (CategoryTheory.ShortComplex.Homotopy.refl φ₂))).trans (CategoryTheory.ShortComplex.Homotopy.ofEq ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0<GOAL>(CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₂ = h₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0<GOAL>(CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₁ = h₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0<GOAL>(CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₃ = h₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0<GOAL>(CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₀ = h₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>H₁ : S₁.LeftHomologyData<VAR>H₂ : S₂.LeftHomologyData<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0<GOAL>CategoryTheory.ShortComplex.leftHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>H₁ : S₁.RightHomologyData<VAR>H₂ : S₂.RightHomologyData<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0<GOAL>CategoryTheory.ShortComplex.rightHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>H₁ : S₁.HomologyData<VAR>H₂ : S₂.HomologyData<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0<GOAL>CategoryTheory.ShortComplex.homologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0<GOAL>CategoryTheory.ShortComplex.leftHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0<GOAL>CategoryTheory.ShortComplex.rightHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0<GOAL>CategoryTheory.ShortComplex.homologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>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.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.ShortComplex.rightHomologyMap' φ₁ h₁ h₂ = CategoryTheory.ShortComplex.rightHomologyMap' φ₂ h₁ h₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<GOAL>CategoryTheory.ShortComplex.homologyMap' φ₁ h₁ h₂ = CategoryTheory.ShortComplex.homologyMap' φ₂ h₁ h₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.leftHomologyMap φ₁ = CategoryTheory.ShortComplex.leftHomologyMap φ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.rightHomologyMap φ₁ = CategoryTheory.ShortComplex.rightHomologyMap φ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>CategoryTheory.ShortComplex.homologyMap φ₁ = CategoryTheory.ShortComplex.homologyMap φ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.HomotopyEquiv.refl S).hom = CategoryTheory.CategoryStruct.id S
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.HomotopyEquiv.refl S).homotopyHomInvId = CategoryTheory.ShortComplex.Homotopy.ofEq ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.HomotopyEquiv.refl S).inv = CategoryTheory.CategoryStruct.id S
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.HomotopyEquiv.refl S).homotopyInvHomId = CategoryTheory.ShortComplex.Homotopy.ofEq ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁.HomotopyEquiv S₂<GOAL>e.symm.homotopyHomInvId = e.homotopyInvHomId
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁.HomotopyEquiv S₂<GOAL>e.symm.homotopyInvHomId = e.homotopyHomInvId
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁.HomotopyEquiv S₂<GOAL>e.symm.inv = e.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁.HomotopyEquiv S₂<GOAL>e.symm.hom = e.inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>e : S₁.HomotopyEquiv S₂<VAR>e' : S₂.HomotopyEquiv S₃<GOAL>(e.trans e').hom = CategoryTheory.CategoryStruct.comp e.hom e'.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>e : S₁.HomotopyEquiv S₂<VAR>e' : S₂.HomotopyEquiv S₃<GOAL>(e.trans e').homotopyHomInvId = (CategoryTheory.ShortComplex.Homotopy.ofEq ⋯).trans (((e'.homotopyHomInvId.compRight e.inv).compLeft e.hom).trans ((CategoryTheory.ShortComplex.Homotopy.ofEq ⋯).trans e.homotopyHomInvId))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>e : S₁.HomotopyEquiv S₂<VAR>e' : S₂.HomotopyEquiv S₃<GOAL>(e.trans e').homotopyInvHomId = (CategoryTheory.ShortComplex.Homotopy.ofEq ⋯).trans (((e.homotopyInvHomId.compRight e'.hom).compLeft e'.inv).trans ((CategoryTheory.ShortComplex.Homotopy.ofEq ⋯).trans e'.homotopyInvHomId))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>e : S₁.HomotopyEquiv S₂<VAR>e' : S₂.HomotopyEquiv S₃<GOAL>(e.trans e').inv = CategoryTheory.CategoryStruct.comp e'.inv e.inv
<VAR>R : Type (max u v)<VAR>CommRing R<VAR>D : Type v<VAR>CategoryTheory.SmallCategory D<VAR>I : D ⥤ Ideal R<VAR>i : ℕ<GOAL>CategoryTheory.Limits.HasColimit (localCohomology.diagram I i)
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>hIJ : I ≤ J.radical<VAR>hJ : J.radical.FG<GOAL>∃ k, I ^ k ≤ J
<VAR>R : Type u_1<VAR>Semiring R<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>ι : Type u_4<VAR>c : ComplexShape ι<VAR>X Y : HomologicalComplex C c<VAR>r : R<VAR>f : X ⟶ Y<VAR>n : ι<GOAL>(r • f).f n = r • f.f n
<VAR>R : Type u_1<VAR>Semiring R<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>ι : Type u_4<VAR>c : ComplexShape ι<VAR>X Y : HomologicalComplex C c<VAR>r : Rˣ<VAR>f : X ⟶ Y<VAR>n : ι<GOAL>(r • f).f n = r • f.f n
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>A : C<VAR>i : ι<VAR>γ : A ⟶ K.homology i<VAR>j : ι<VAR>hj : c.next i = j<GOAL>∃ A' π, ∃ (_ : CategoryTheory.Epi π), ∃ z, ∃ (hz : z ≫ K.d i j = 0), π ≫ γ = K.liftCycles z j hj hz ≫ K.homologyπ 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>self : S.LeftHomologyData<GOAL>CategoryTheory.CategoryStruct.comp (self.hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) self.π = 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.LeftHomologyData<GOAL>CategoryTheory.CategoryStruct.comp self.i 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>CategoryTheory.Limits.HasKernel S.g<VAR>CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).π = CategoryTheory.Limits.cokernel.π (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 : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasKernel S.g<VAR>CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).K = 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>CategoryTheory.Limits.HasKernel S.g<VAR>CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).i = 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>CategoryTheory.Limits.HasKernel S.g<VAR>CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).H = CategoryTheory.Limits.cokernel (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 : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : CategoryTheory.CategoryStruct.comp k S.g = 0<GOAL>CategoryTheory.CategoryStruct.comp (h.liftK k hk) h.i = 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.CategoryStruct.comp h.f' h.i = 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>h : S.LeftHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h.f' 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<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>x : A ⟶ S.X₁<VAR>hx : k = CategoryTheory.CategoryStruct.comp x S.f<GOAL>CategoryTheory.CategoryStruct.comp (h.liftK k ⋯) 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<VAR>A : C<VAR>k : h.K ⟶ A<VAR>hk : CategoryTheory.CategoryStruct.comp h.f' k = 0<GOAL>CategoryTheory.CategoryStruct.comp h.π (h.descH k hk) = 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>hg : S.g = 0<GOAL>CategoryTheory.IsIso 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>hf : S.f = 0<GOAL>CategoryTheory.IsIso 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>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).π = 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>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).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>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).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>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg 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>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).f' = 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>CategoryTheory.Limits.HasCokernel S.f<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).π = CategoryTheory.Limits.cokernel.π 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>CategoryTheory.Limits.HasCokernel S.f<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S 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>CategoryTheory.Limits.HasCokernel S.f<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S 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>CategoryTheory.Limits.HasCokernel S.f<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).H = CategoryTheory.Limits.cokernel S.f