ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>h₁ : CategoryTheory.IsIso (CategoryTheory.ShortComplex.opcyclesMap φ)<VAR>h₂ : CategoryTheory.Mono φ.τ₃<GOAL>CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : CategoryTheory.Limits.IsZero S.X₂<VAR>S.HasHomology<GOAL>CategoryTheory.Limits.IsZero S.homology
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>S.HasHomology<GOAL>CategoryTheory.IsIso S.homologyπ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>S.HasHomology<GOAL>CategoryTheory.IsIso S.homologyι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>S.HasHomology<GOAL>(S.asIsoHomologyπ hf).hom = S.homologyπ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>S.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp (S.asIsoHomologyπ hf).inv S.homologyπ = CategoryTheory.CategoryStruct.id S.homology
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>S.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp S.homologyπ (S.asIsoHomologyπ hf).inv = CategoryTheory.CategoryStruct.id S.cycles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>S.HasHomology<GOAL>(S.asIsoHomologyι hg).hom = S.homologyι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>S.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp (S.asIsoHomologyι hg).inv S.homologyι = CategoryTheory.CategoryStruct.id S.opcycles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>S.HasHomology<GOAL>CategoryTheory.CategoryStruct.comp S.homologyι (S.asIsoHomologyι hg).inv = CategoryTheory.CategoryStruct.id S.homology
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>h : CategoryTheory.Mono (CategoryTheory.ShortComplex.opcyclesMap φ)<GOAL>CategoryTheory.Mono (CategoryTheory.ShortComplex.homologyMap φ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>h : CategoryTheory.Epi (CategoryTheory.ShortComplex.cyclesMap φ)<GOAL>CategoryTheory.Epi (CategoryTheory.ShortComplex.homologyMap φ)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)<GOAL>∀ {X Y : J} (f : X ⟶ Y), ((CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).obj S).map f = S.mapNatTrans ((CategoryTheory.evaluation J C).map f)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)<VAR>j : J<GOAL>((CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).obj S).obj j = S.map ((CategoryTheory.evaluation J C).obj j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)} (φ : X ⟶ Y) (j : J), ((CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).map φ).app j = ((CategoryTheory.evaluation J C).obj j).mapShortComplex.map φ
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)<GOAL>((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).g = CategoryTheory.whiskerLeft F CategoryTheory.ShortComplex.π₂Toπ₃
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)<GOAL>((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).X₃ = F.comp CategoryTheory.ShortComplex.π₃
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)<GOAL>((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).X₂ = F.comp CategoryTheory.ShortComplex.π₂
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)<GOAL>((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).f = CategoryTheory.whiskerLeft F CategoryTheory.ShortComplex.π₁Toπ₂
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)<GOAL>((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).X₁ = F.comp CategoryTheory.ShortComplex.π₁
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (φ : X ⟶ Y), ((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).map φ).τ₂ = CategoryTheory.whiskerRight φ CategoryTheory.ShortComplex.π₂
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (φ : X ⟶ Y), ((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).map φ).τ₃ = CategoryTheory.whiskerRight φ CategoryTheory.ShortComplex.π₃
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (φ : X ⟶ Y), ((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).map φ).τ₁ = CategoryTheory.whiskerRight φ CategoryTheory.ShortComplex.π₁
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)<GOAL>∀ (X_1 : J), ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).inv.app X).τ₂.app X_1 = CategoryTheory.CategoryStruct.id (X.X₂.obj X_1)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)<GOAL>∀ (X_1 : J), ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).inv.app X).τ₃.app X_1 = CategoryTheory.CategoryStruct.id (X.X₃.obj X_1)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)<GOAL>∀ (X_1 : J), ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).hom.app X).τ₁.app X_1 = CategoryTheory.CategoryStruct.id (X.X₁.obj X_1)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)<GOAL>∀ (X_1 : J), ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).hom.app X).τ₃.app X_1 = CategoryTheory.CategoryStruct.id (X.X₃.obj X_1)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)<GOAL>∀ (X_1 : J), ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).hom.app X).τ₂.app X_1 = CategoryTheory.CategoryStruct.id (X.X₂.obj X_1)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)<GOAL>∀ (X_1 : J), ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).inv.app X).τ₁.app X_1 = CategoryTheory.CategoryStruct.id (X.X₁.obj X_1)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)<GOAL>∀ (X_1 : J), (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).inv.app X).app X_1).τ₂ = CategoryTheory.CategoryStruct.id (X.obj X_1).X₂
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)<GOAL>∀ (X_1 : J), (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).inv.app X).app X_1).τ₃ = CategoryTheory.CategoryStruct.id (X.obj X_1).X₃
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)<GOAL>∀ (X_1 : J), (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).hom.app X).app X_1).τ₂ = CategoryTheory.CategoryStruct.id (X.obj X_1).X₂
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)<GOAL>∀ (X_1 : J), (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).hom.app X).app X_1).τ₁ = CategoryTheory.CategoryStruct.id (X.obj X_1).X₁
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)<GOAL>∀ (X_1 : J), (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).inv.app X).app X_1).τ₁ = CategoryTheory.CategoryStruct.id (X.obj X_1).X₁
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)<GOAL>∀ (X_1 : J), (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).hom.app X).app X_1).τ₃ = CategoryTheory.CategoryStruct.id (X.obj X_1).X₃
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>(CategoryTheory.ShortComplex.functorEquivalence J C).unitIso = CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>(CategoryTheory.ShortComplex.functorEquivalence J C).functor = CategoryTheory.ShortComplex.FunctorEquivalence.functor J C
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>(CategoryTheory.ShortComplex.functorEquivalence J C).counitIso = CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>(CategoryTheory.ShortComplex.functorEquivalence J C).inverse = CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>self : TotalComplexShape c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<GOAL>c₁₂.Rel (TotalComplexShape.π c₁ c₂ c₁₂ (i₁, i₂)) (TotalComplexShape.π c₁ c₂ c₁₂ (i₁, i₂'))
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>self : TotalComplexShape c₁ c₂ c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<GOAL>c₁₂.Rel (TotalComplexShape.π c₁ c₂ c₁₂ (i₁, i₂)) (TotalComplexShape.π c₁ c₂ c₁₂ (i₁', i₂))
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>self : TotalComplexShape c₁ c₂ c₁₂<VAR>i₁ i₁' : I₁<VAR>i₂ i₂' : I₂<VAR>h₁ : c₁.Rel i₁ i₁'<VAR>h₂ : c₂.Rel i₂ i₂'<GOAL>TotalComplexShape.ε₂ c₁ c₂ c₁₂ (i₁, i₂) * TotalComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂') = -TotalComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂) * TotalComplexShape.ε₂ c₁ c₂ c₁₂ (i₁', i₂)
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<GOAL>c₁₂.Rel (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁.π c₂ c₁₂ (i₁', i₂))
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<GOAL>c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = c₁.π c₂ c₁₂ (i₁', i₂)
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<GOAL>c₁₂.prev (c₁.π c₂ c₁₂ (i₁', i₂)) = c₁.π c₂ c₁₂ (i₁, i₂)
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<GOAL>c₁₂.Rel (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁.π c₂ c₁₂ (i₁, i₂'))
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<GOAL>c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = c₁.π c₂ c₁₂ (i₁, i₂')
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<GOAL>c₁₂.prev (c₁.π c₂ c₁₂ (i₁, i₂')) = c₁.π c₂ c₁₂ (i₁, i₂)
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>i₁ i₁' : I₁<VAR>i₂ i₂' : I₂<VAR>h₁ : c₁.Rel i₁ i₁'<VAR>h₂ : c₂.Rel i₂ i₂'<GOAL>c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') = -c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>i₁ i₁' : I₁<VAR>i₂ i₂' : I₂<VAR>h₁ : c₁.Rel i₁ i₁'<VAR>h₂ : c₂.Rel i₂ i₂'<GOAL>c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁, i₂) = -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>self : c.TensorSigns<VAR>p q : I<VAR>hpq : c.Rel p q<GOAL>(ComplexShape.TensorSigns.ε' c) q = -(ComplexShape.TensorSigns.ε' c) p
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>self : c.TensorSigns<VAR>p q r : I<VAR>hpq : c.Rel p q<GOAL>c.Rel (p + r) (q + r)
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>self : c.TensorSigns<VAR>p q r : I<VAR>hpq : c.Rel p q<GOAL>c.Rel (r + p) (r + q)
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>c.TensorSigns<VAR>p q : I<VAR>hpq : c.Rel p q<VAR>r : I<GOAL>c.Rel (p + r) (q + r)
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>c.TensorSigns<VAR>r : I<VAR>p q : I<VAR>hpq : c.Rel p q<GOAL>c.Rel (r + p) (r + q)
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>c.TensorSigns<GOAL>c.ε 0 = 1
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>c.TensorSigns<VAR>p q : I<VAR>hpq : c.Rel p q<GOAL>c.ε q = -c.ε p
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>c.TensorSigns<VAR>p q : I<GOAL>c.ε (p + q) = c.ε p * c.ε q
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>c.TensorSigns<VAR>p q : I<VAR>hp : c.Rel p (c.next p)<GOAL>c.next (p + q) = c.next p + q
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>c.TensorSigns<VAR>p q : I<VAR>hq : c.Rel q (c.next q)<GOAL>c.next (p + q) = p + c.next q
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>c.TensorSigns<GOAL>∀ (x : I × I), TotalComplexShape.π c c c x = match x with | (p, q) => p + q
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>c.TensorSigns<GOAL>∀ (x : I × I), TotalComplexShape.ε₂ c c c x = match x with | (p, snd) => c.ε p
<VAR>I : Type u_4<VAR>AddMonoid I<VAR>c : ComplexShape I<VAR>c.TensorSigns<GOAL>∀ (x : I × I), TotalComplexShape.ε₁ c c c x = 1
<VAR>n : ℕ<GOAL>(ComplexShape.down ℕ).ε n = (-1) ^ n
<VAR>n : ℤ<GOAL>(ComplexShape.up ℤ).ε n = n.negOnePow
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>TotalComplexShape c₂ c₁ c₁₂<VAR>self : TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h₂ : c₂.Rel i₂ i₂'<GOAL>TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂ * c₁.ε₂ c₂ c₁₂ (i₁, i₂) = c₂.ε₁ c₁ c₁₂ (i₂, i₁) * TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂'
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>TotalComplexShape c₂ c₁ c₁₂<VAR>self : TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>i₁ i₁' : I₁<VAR>h₁ : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<GOAL>TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂) = c₂.ε₂ c₁ c₁₂ (i₂, i₁) * TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁' i₂
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>TotalComplexShape c₂ c₁ c₁₂<VAR>self : TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>TotalComplexShape c₂ c₁ c₁₂<VAR>TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>TotalComplexShape c₂ c₁ c₁₂<VAR>TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>i₁ i₁' : I₁<VAR>h₁ : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<GOAL>c₁.σ c₂ c₁₂ i₁ i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂) = c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁' i₂
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>TotalComplexShape c₂ c₁ c₁₂<VAR>TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h₂ : c₂.Rel i₂ i₂'<GOAL>c₁.σ c₂ c₁₂ i₁ i₂ * c₁.ε₂ c₂ c₁₂ (i₁, i₂) = c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁ i₂'
<VAR>p q : ℤ<GOAL>TotalComplexShapeSymmetry.σ (ComplexShape.up ℤ) (ComplexShape.up ℤ) (ComplexShape.up ℤ) p q = (p * q).negOnePow
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>TotalComplexShape c₂ c₁ c₁₂<VAR>TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>TotalComplexShapeSymmetry c₂ c₁ c₁₂<VAR>self : TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>TotalComplexShape c₁ c₂ c₁₂<VAR>TotalComplexShape c₂ c₁ c₁₂<VAR>TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>TotalComplexShapeSymmetry c₂ c₁ c₁₂<VAR>TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂
<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>(φ + φ').τ₁ = φ.τ₁ + φ'.τ₁
<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>(φ + φ').τ₂ = φ.τ₂ + φ'.τ₂
<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>(φ + φ').τ₃ = φ.τ₃ + φ'.τ₃
<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>(φ - φ').τ₁ = φ.τ₁ - φ'.τ₁
<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>(φ - φ').τ₂ = φ.τ₂ - φ'.τ₂
<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>(φ - φ').τ₃ = φ.τ₃ - φ'.τ₃
<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>(-φ).τ₁ = -φ.τ₁
<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>(-φ).τ₂ = -φ.τ₂
<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>(-φ).τ₃ = -φ.τ₃
<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₂<GOAL>γ.neg.φK = -γ.φK
<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₂<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₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂<VAR>γ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₁ h₂<GOAL>(γ.add γ').φK = γ.φK + γ'.φK