ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>e : K ≅ L<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<GOAL>L.HasTotal c₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h : ¬c₁.Rel i₁ (c₁.next i₁)<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h : ¬c₂.Rel i₂ (c₂.next i₂)<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<VAR>i₁₂ : I₁₂<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<VAR>i : I₁ × I₂<VAR>h : c₁.π c₂ c₁₂ i = i₁₂<GOAL>K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' = K.d₁ c₁₂ i.1 i.2 i₁₂'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<VAR>i : I₁ × I₂<VAR>h : c₁.π c₂ c₁₂ i = i₁₂<GOAL>K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' = K.d₂ c₁₂ i.1 i.2 i₁₂'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<VAR>h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'<GOAL>K.D₁ c₁₂ i₁₂ i₁₂' = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<VAR>h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'<GOAL>K.D₂ c₁₂ i₁₂ i₁₂' = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁₂ i₁₂' i₁₂'' : I₁₂<GOAL>K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁₂ i₁₂' i₁₂'' : I₁₂<GOAL>K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁₂ i₁₂' i₁₂'' : I₁₂<GOAL>K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = -K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁₂ i₁₂' i₁₂'' : I₁₂<GOAL>K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = -K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂''
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<GOAL>(K.total c₁₂).d i₁₂ i₁₂' = K.D₁ c₁₂ i₁₂ i₁₂' + K.D₂ c₁₂ i₁₂ i₁₂'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>x₁ y₁ : I₁<VAR>h₁ : x₁ = y₁<VAR>x₂ y₂ : I₂<VAR>h₂ : x₂ = y₂<VAR>i₁₂ : I₁₂<VAR>h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂<GOAL>(HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂).hom ≫ K.ιTotal c₁₂ y₁ y₂ i₁₂ h = K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>x₁ y₁ : I₁<VAR>h₁ : x₁ = y₁<VAR>x₂ y₂ : I₂<VAR>h₂ : x₂ = y₂<VAR>i₁₂ : I₁₂<VAR>h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂<GOAL>(HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = K.ιTotal c₁₂ y₁ y₂ i₁₂ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂<GOAL>K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ = K.ιTotal c₁₂ i₁ i₂ i₁₂ h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h : c₁.π c₂ c₁₂ (i₁, i₂) ≠ i₁₂<GOAL>K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂<GOAL>K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' = K.d₁ c₁₂ i₁ i₂ i₁₂'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂<GOAL>K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' = K.d₂ c₁₂ i₁ i₂ i₁₂'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.ιTotalOrZero c₁₂ i₁' i₂ i₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.ιTotal c₁₂ i₁' i₂ i₁₂ h'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<VAR>i₁₂ : I₁₂<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.ιTotalOrZero c₁₂ i₁ i₂' i₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.ιTotal c₁₂ i₁ i₂' i₁₂ h'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>A : C<VAR>i₁₂ : I₁₂<VAR>f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂<GOAL>K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ K.totalDesc f = f i₁ i₂ hi
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>A : C<VAR>i₁₂ : I₁₂<VAR>f g : (K.total c₁₂).X i₁₂ ⟶ A<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>L.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>L.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂ ≫ CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>L.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<GOAL>CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂' = K.D₁ c₁₂ i₁₂ i₁₂' ≫ CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>L.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<GOAL>CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂' = K.D₂ c₁₂ i₁₂ i₁₂' ≫ CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>L.HasTotal c₁₂<GOAL>(HomologicalComplex.forget C c₁₂).map (HomologicalComplex₂.total.map φ c₁₂) = CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<GOAL>HomologicalComplex₂.total.map (𝟙 K) c₁₂ = 𝟙 (K.total c₁₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>L.HasTotal c₁₂<VAR>M.HasTotal c₁₂<GOAL>HomologicalComplex₂.total.map (φ ≫ ψ) c₁₂ = HomologicalComplex₂.total.map φ c₁₂ ≫ HomologicalComplex₂.total.map ψ c₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>e : K ≅ L<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>L.HasTotal c₁₂<GOAL>(HomologicalComplex₂.total.mapIso e c₁₂).inv = HomologicalComplex₂.total.map e.inv c₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>e : K ≅ L<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>L.HasTotal c₁₂<GOAL>(HomologicalComplex₂.total.mapIso e c₁₂).hom = HomologicalComplex₂.total.map e.hom c₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>L.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂<GOAL>K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ (HomologicalComplex₂.total.map φ c₁₂).f i₁₂ = (φ.f i₁).f i₂ ≫ L.ιTotal c₁₂ i₁ i₂ i₁₂ h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>K.HasTotal c₁₂<VAR>L.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<GOAL>K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ ≫ (HomologicalComplex₂.total.map φ c₁₂).f i₁₂ = (φ.f i₁).f i₂ ≫ L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>∀ (K : HomologicalComplex₂ C c₁ c₂), K.HasTotal c₁₂<GOAL>∀ {X Y : HomologicalComplex₂ C c₁ c₂} (φ : X ⟶ Y), (HomologicalComplex₂.totalFunctor C c₁ c₂ c₁₂).map φ = HomologicalComplex₂.total.map φ c₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>DecidableEq I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>∀ (K : HomologicalComplex₂ C c₁ c₂), K.HasTotal c₁₂<VAR>K : HomologicalComplex₂ C c₁ c₂<GOAL>(HomologicalComplex₂.totalFunctor C c₁ c₂ c₁₂).obj K = K.total c₁₂
<VAR>K : Type u_1<VAR>β : Type u_2<VAR>Coe K β<VAR>b : ℤ<VAR>fr : K<GOAL>↑{ b := b, fr := fr } = { b := b, fr := Coe.coe fr }
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<GOAL>(GenContFract.IntFractPair.stream v).IsSeq
<VAR>α : Type u<VAR>self : Shelf α<VAR>x y z : α<GOAL>x ◃ y ◃ z = (x ◃ y) ◃ x ◃ z
<VAR>α : Type u<VAR>self : UnitalShelf α<VAR>a : α<GOAL>1 ◃ a = a
<VAR>α : Type u<VAR>self : UnitalShelf α<VAR>a : α<GOAL>a ◃ 1 = a
<VAR>S₁ : Type u_1<VAR>S₂ : Type u_2<VAR>Shelf S₁<VAR>Shelf S₂<VAR>self : S₁ →◃ S₂<VAR>x y : S₁<GOAL>self.toFun (x ◃ y) = self.toFun x ◃ self.toFun y
<VAR>α : Type u<VAR>self : Rack α<VAR>x : α<GOAL>Function.LeftInverse (Rack.invAct x) (Shelf.act x)
<VAR>α : Type u<VAR>self : Rack α<VAR>x : α<GOAL>Function.RightInverse (Rack.invAct x) (Shelf.act x)
<VAR>S : Type u_1<VAR>UnitalShelf S<VAR>x y : S<GOAL>(x ◃ y) ◃ x = x ◃ y
<VAR>S : Type u_1<VAR>UnitalShelf S<VAR>x : S<GOAL>x ◃ x = x
<VAR>S : Type u_1<VAR>UnitalShelf S<VAR>x y : S<GOAL>x ◃ x ◃ y = x ◃ y
<VAR>S : Type u_1<VAR>UnitalShelf S<VAR>x y z : S<GOAL>(x ◃ y) ◃ z = x ◃ y ◃ z
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>(Rack.act' x) y = x ◃ y
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>(Rack.act' x).symm y = x ◃⁻¹ y
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>(Rack.act' x)⁻¹ y = x ◃⁻¹ y
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>x ◃⁻¹ x ◃ y = y
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>x ◃ x ◃⁻¹ y = y
<VAR>R : Type u_1<VAR>Rack R<VAR>x : R<VAR>y y' : R<GOAL>x ◃ y = x ◃ y' ↔ y = y'
<VAR>R : Type u_1<VAR>Rack R<VAR>x : R<VAR>y y' : R<GOAL>x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'
<VAR>R : Type u_1<VAR>Rack R<VAR>x y z : R<GOAL>x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z
<VAR>R : Type u_2<VAR>Rack R<VAR>x y : R<GOAL>Rack.act' (x ◃ y) = Rack.act' x * Rack.act' y * (Rack.act' x)⁻¹
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>MulOpposite.op x ◃ MulOpposite.op y = MulOpposite.op (x ◃⁻¹ y)
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>MulOpposite.op x ◃⁻¹ MulOpposite.op y = MulOpposite.op (x ◃ y)
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>(x ◃ x) ◃ y = x ◃ y
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>(x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>(x ◃ x) ◃⁻¹ y = x ◃⁻¹ y
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>(x ◃⁻¹ x) ◃ y = x ◃ y
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>x ◃ x = y ◃ y ↔ x = y
<VAR>R : Type u_1<VAR>Rack R<VAR>x y : R<GOAL>x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y
<VAR>R : Type u_2<VAR>Rack R<VAR>h : Rack.IsInvolutory R<VAR>x y : R<GOAL>x ◃⁻¹ y = x ◃ y
<VAR>R : Type u_2<VAR>Rack R<VAR>x y z : R<GOAL>x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
<VAR>S₁ : Type u_1<VAR>S₂ : Type u_2<VAR>Shelf S₁<VAR>Shelf S₂<VAR>f : S₁ →◃ S₂<GOAL>f.toFun = ⇑f
<VAR>S₁ : Type u_1<VAR>S₂ : Type u_2<VAR>Shelf S₁<VAR>Shelf S₂<VAR>f : S₁ →◃ S₂<VAR>x y : S₁<GOAL>f (x ◃ y) = f x ◃ f y
<VAR>S₁ : Type u_1<VAR>S₂ : Type u_2<VAR>S₃ : Type u_3<VAR>Shelf S₁<VAR>Shelf S₂<VAR>Shelf S₃<VAR>g : S₂ →◃ S₃<VAR>f : S₁ →◃ S₂<VAR>x : S₁<GOAL>(g.comp f) x = g (f x)
<VAR>α : Type u_1<VAR>self : Quandle α<VAR>x : α<GOAL>x ◃ x = x
<VAR>Q : Type u_1<VAR>Quandle Q<VAR>x : Q<GOAL>x ◃⁻¹ x = x
<VAR>G : Type u_2<VAR>Group G<VAR>x y : Quandle.Conj G<GOAL>x ◃ y = x * y * x⁻¹
<VAR>G : Type u_2<VAR>Group G<VAR>x y : Quandle.Conj G<GOAL>x ◃ y = y ↔ y ◃ x = x
<VAR>n : ℕ<VAR>a : ZMod n<GOAL>Function.Involutive (Quandle.dihedralAct n a)