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₂ : CategoryTheory.ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>γ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₁ h₂<GOAL>(γ.add γ').φ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>φ : S₁ ⟶ S₂<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₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>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.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>CategoryTheory.ShortComplex.leftHomologyMap' (φ + φ') h₁ h₂ = 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₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>CategoryTheory.ShortComplex.cyclesMap' (φ + φ') h₁ h₂ = 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.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>CategoryTheory.ShortComplex.leftHomologyMap' (φ - φ') h₁ h₂ = 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₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>CategoryTheory.ShortComplex.cyclesMap' (φ - φ') h₁ h₂ = 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.Preadditive C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<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>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.cyclesMap (-φ) = -CategoryTheory.ShortComplex.cyclesMap φ
<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>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.leftHomologyMap (φ + φ') = 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>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.cyclesMap (φ + φ') = CategoryTheory.ShortComplex.cyclesMap φ + CategoryTheory.ShortComplex.cyclesMap φ'
<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>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.leftHomologyMap (φ - φ') = 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>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<GOAL>CategoryTheory.ShortComplex.cyclesMap (φ - φ') = CategoryTheory.ShortComplex.cyclesMap φ - CategoryTheory.ShortComplex.cyclesMap φ'
<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₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<GOAL>γ.neg.φ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₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<GOAL>γ.neg.φQ = -γ.φQ
<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₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>γ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₁ h₂<GOAL>(γ.add γ').φQ = γ.φQ + γ'.φQ
<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₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>γ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₁ h₂<GOAL>(γ.add γ').φ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>φ : S₁ ⟶ S₂<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₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.ShortComplex.opcyclesMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.opcyclesMap' φ 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₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.ShortComplex.rightHomologyMap' (φ + φ') h₁ h₂ = 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₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.ShortComplex.opcyclesMap' (φ + φ') h₁ h₂ = CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂ + CategoryTheory.ShortComplex.opcyclesMap' φ' 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₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.ShortComplex.rightHomologyMap' (φ - φ') h₁ h₂ = 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₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>CategoryTheory.ShortComplex.opcyclesMap' (φ - φ') h₁ h₂ = CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂ - CategoryTheory.ShortComplex.opcyclesMap' φ' 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>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>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.opcyclesMap (-φ) = -CategoryTheory.ShortComplex.opcyclesMap φ
<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>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.rightHomologyMap (φ + φ') = 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>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.opcyclesMap (φ + φ') = CategoryTheory.ShortComplex.opcyclesMap φ + CategoryTheory.ShortComplex.opcyclesMap φ'
<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>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.rightHomologyMap (φ - φ') = 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>S₁.HasRightHomology<VAR>S₂.HasRightHomology<GOAL>CategoryTheory.ShortComplex.opcyclesMap (φ - φ') = CategoryTheory.ShortComplex.opcyclesMap φ - CategoryTheory.ShortComplex.opcyclesMap φ'
<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₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<GOAL>γ.neg.left = γ.left.neg
<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₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<GOAL>γ.neg.right = γ.right.neg
<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₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<VAR>γ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₁ h₂<GOAL>(γ.add γ').left = γ.left.add γ'.left
<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₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<VAR>γ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₁ h₂<GOAL>(γ.add γ').right = γ.right.add γ'.right
<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₁ : 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₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<GOAL>CategoryTheory.ShortComplex.homologyMap' (φ + φ') h₁ h₂ = 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₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<GOAL>CategoryTheory.ShortComplex.homologyMap' (φ - φ') h₁ h₂ = 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>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₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>CategoryTheory.ShortComplex.homologyMap (φ + φ') = 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₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<GOAL>CategoryTheory.ShortComplex.homologyMap (φ - φ') = 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₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>CategoryTheory.CategoryStruct.comp S₁.g self.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>self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f self.h₁ + self.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>self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>φ₁.τ₃ = self.h₃ + CategoryTheory.CategoryStruct.comp self.h₂ S₂.g + φ₂.τ₃
<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>self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>φ₁.τ₂ = CategoryTheory.CategoryStruct.comp S₁.g self.h₂ + CategoryTheory.CategoryStruct.comp self.h₁ S₂.f + φ₂.τ₂
<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>self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>CategoryTheory.CategoryStruct.comp self.h₀ S₂.f = 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₁.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>(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = h₀ + CategoryTheory.CategoryStruct.comp S₁.f 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>(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃ = CategoryTheory.CategoryStruct.comp h₂ S₂.g + 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>(S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ = CategoryTheory.CategoryStruct.comp h₁ S₂.f + CategoryTheory.CategoryStruct.comp S₁.g 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 : φ₁ = φ₂<GOAL>(CategoryTheory.ShortComplex.Homotopy.ofEq 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₁ ⟶ S₂<VAR>h : φ₁ = φ₂<GOAL>(CategoryTheory.ShortComplex.Homotopy.ofEq 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₁ ⟶ S₂<VAR>h : φ₁ = φ₂<GOAL>(CategoryTheory.ShortComplex.Homotopy.ofEq 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₁ ⟶ S₂<VAR>h : φ₁ = φ₂<GOAL>(CategoryTheory.ShortComplex.Homotopy.ofEq 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₁ ⟶ S₂<GOAL>(CategoryTheory.ShortComplex.Homotopy.refl φ).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₂<GOAL>(CategoryTheory.ShortComplex.Homotopy.refl φ).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₂<GOAL>(CategoryTheory.ShortComplex.Homotopy.refl φ).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₂<GOAL>(CategoryTheory.ShortComplex.Homotopy.refl φ).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 φ₁ φ₂<GOAL>h.symm.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>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.symm.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>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.symm.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>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.symm.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>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.neg.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>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.neg.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>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.neg.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>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<GOAL>h.neg.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>φ₁ φ₂ φ₃ : S₁ ⟶ S₂<VAR>h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃<GOAL>(h₁₂.trans 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>φ₁ φ₂ φ₃ : S₁ ⟶ S₂<VAR>h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃<GOAL>(h₁₂.trans 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>φ₁ φ₂ φ₃ : S₁ ⟶ S₂<VAR>h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃<GOAL>(h₁₂.trans 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>φ₁ φ₂ φ₃ : S₁ ⟶ S₂<VAR>h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃<GOAL>(h₁₂.trans 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>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄<GOAL>(h.add 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>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄<GOAL>(h.add 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>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄<GOAL>(h.add 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>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄<GOAL>(h.add 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>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄<GOAL>(h.sub 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>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄<GOAL>(h.sub 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>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄<GOAL>(h.sub 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>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂<VAR>h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄<GOAL>(h.sub 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₂ 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.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.compLeft ψ).h₂ = CategoryTheory.CategoryStruct.comp ψ.τ₃ h.h₂