ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>X : V<GOAL>(HomologicalComplex.singleCompEvalIsoSelf V c j).hom.app X = (HomologicalComplex.singleObjXSelf c j X).hom
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j i : ι<VAR>hi : i ≠ j<GOAL>CategoryTheory.Limits.IsZero (HomologicalComplex.single V c j ⋙ HomologicalComplex.eval V c i)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>j : ι<VAR>A : V<VAR>f g : (HomologicalComplex.single V c j).obj A ⟶ K<VAR>hfg : f.f j = g.f j<GOAL>f = g
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>j : ι<VAR>A : V<VAR>f g : K ⟶ (HomologicalComplex.single V c j).obj A<VAR>hfg : f.f j = g.f j<GOAL>f = g
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>j : ι<VAR>A : V<VAR>φ : K.X j ⟶ A<VAR>hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0<GOAL>(HomologicalComplex.mkHomToSingle φ hφ).f j = φ ≫ (HomologicalComplex.singleObjXSelf c j A).inv
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>j : ι<VAR>A : V<VAR>φ : A ⟶ K.X j<VAR>hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0<GOAL>(HomologicalComplex.mkHomFromSingle φ hφ).f j = (HomologicalComplex.singleObjXSelf c j A).hom ≫ φ
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>A : V<GOAL>((ChainComplex.single₀ V).obj A).X 0 = A
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>A B : V<VAR>f : A ⟶ B<GOAL>((ChainComplex.single₀ V).map f).f 0 = f
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>X : V<GOAL>HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X = CategoryTheory.Iso.refl (((HomologicalComplex.single V (ComplexShape.down ℕ) 0).obj X).X 0)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>φ : C ⟶ (ChainComplex.single₀ V).obj X<GOAL>↑((C.toSingle₀Equiv X) φ) = φ.f 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : C.X 0 ⟶ X<VAR>hf : C.d 1 0 ≫ f = 0<GOAL>((C.toSingle₀Equiv X).symm ⟨f, hf⟩).f 0 = f
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : (ChainComplex.single₀ V).obj X ⟶ C<GOAL>(C.fromSingle₀Equiv X) f = f.f 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : X ⟶ C.X 0<GOAL>((C.fromSingle₀Equiv X).symm f).f 0 = f
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : X ⟶ C.X 0<VAR>n : ℕ<GOAL>((C.fromSingle₀Equiv X).symm f).f (n + 1) = 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>A : V<GOAL>((CochainComplex.single₀ V).obj A).X 0 = A
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>A B : V<VAR>f : A ⟶ B<GOAL>((CochainComplex.single₀ V).map f).f 0 = f
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>X : V<GOAL>HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 X = CategoryTheory.Iso.refl (((HomologicalComplex.single V (ComplexShape.up ℕ) 0).obj X).X 0)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>φ : (CochainComplex.single₀ V).obj X ⟶ C<GOAL>↑((C.fromSingle₀Equiv X) φ) = φ.f 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : X ⟶ C.X 0<VAR>hf : f ≫ C.d 0 1 = 0<GOAL>((C.fromSingle₀Equiv X).symm ⟨f, hf⟩).f 0 = f
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : C ⟶ (CochainComplex.single₀ V).obj X<GOAL>(C.toSingle₀Equiv X) f = f.f 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : C.X 0 ⟶ X<GOAL>((C.toSingle₀Equiv X).symm f).f 0 = f
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>C : CochainComplex V ℕ<VAR>X : V<VAR>f : C.X 0 ⟶ X<VAR>n : ℕ<GOAL>((C.toSingle₀Equiv X).symm f).f (n + 1) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>self : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.CategoryStruct.comp self.f self.g = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>self : S₁.Hom S₂<GOAL>CategoryTheory.CategoryStruct.comp self.τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f self.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>self : S₁.Hom S₂<GOAL>CategoryTheory.CategoryStruct.comp self.τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g self.τ₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.Hom.id S).τ₃ = CategoryTheory.CategoryStruct.id S.X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.Hom.id S).τ₂ = CategoryTheory.CategoryStruct.id S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.Hom.id S).τ₁ = CategoryTheory.CategoryStruct.id S.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁₂ : S₁.Hom S₂<VAR>φ₂₃ : S₂.Hom S₃<GOAL>(φ₁₂.comp φ₂₃).τ₃ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ φ₂₃.τ₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁₂ : S₁.Hom S₂<VAR>φ₂₃ : S₂.Hom S₃<GOAL>(φ₁₂.comp φ₂₃).τ₁ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₁ φ₂₃.τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁₂ : S₁.Hom S₂<VAR>φ₂₃ : S₂.Hom S₃<GOAL>(φ₁₂.comp φ₂₃).τ₂ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₂ φ₂₃.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>f g : S₁ ⟶ S₂<VAR>h₁ : f.τ₁ = g.τ₁<VAR>h₂ : f.τ₂ = g.τ₂<VAR>h₃ : f.τ₃ = g.τ₃<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>τ₁ : S₁.X₁ ⟶ S₂.X₁<VAR>τ₂ : S₁.X₂ ⟶ S₂.X₂<VAR>τ₃ : S₁.X₃ ⟶ S₂.X₃<VAR>comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂<VAR>comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃<GOAL>(CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₂ = τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>τ₁ : S₁.X₁ ⟶ S₂.X₁<VAR>τ₂ : S₁.X₂ ⟶ S₂.X₂<VAR>τ₃ : S₁.X₃ ⟶ S₂.X₃<VAR>comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂<VAR>comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃<GOAL>(CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₃ = τ₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>τ₁ : S₁.X₁ ⟶ S₂.X₁<VAR>τ₂ : S₁.X₂ ⟶ S₂.X₂<VAR>τ₃ : S₁.X₃ ⟶ S₂.X₃<VAR>comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂<VAR>comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃<GOAL>(CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₁ = τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.CategoryStruct.id S).τ₁ = CategoryTheory.CategoryStruct.id S.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.CategoryStruct.id S).τ₂ = CategoryTheory.CategoryStruct.id S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.CategoryStruct.id S).τ₃ = CategoryTheory.CategoryStruct.id S.X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁₂ : S₁ ⟶ S₂<VAR>φ₂₃ : S₂ ⟶ S₃<GOAL>(CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₁ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₁ φ₂₃.τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁₂ : S₁ ⟶ S₂<VAR>φ₂₃ : S₂ ⟶ S₃<GOAL>(CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₂ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₂ φ₂₃.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ S₃ : CategoryTheory.ShortComplex C<VAR>φ₁₂ : S₁ ⟶ S₂<VAR>φ₂₃ : S₂ ⟶ S₃<GOAL>(CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₃ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ φ₂₃.τ₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.ShortComplex.Hom.τ₁ 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.ShortComplex.Hom.τ₂ 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.ShortComplex.Hom.τ₃ 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.ShortComplex.π₁.obj S = S.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y), CategoryTheory.ShortComplex.π₁.map f = f.τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y), CategoryTheory.ShortComplex.π₂.map f = f.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.ShortComplex.π₂.obj S = S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.ShortComplex.π₃.obj S = S.X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y), CategoryTheory.ShortComplex.π₃.map f = f.τ₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.ShortComplex.π₁Toπ₂.app S = S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.ShortComplex.π₂Toπ₃.app S = S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.π₁Toπ₂ CategoryTheory.ShortComplex.π₂Toπ₃ = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<GOAL>(S.map F).g = F.map S.g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<GOAL>(S.map F).X₂ = F.obj S.X₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<GOAL>(S.map F).X₃ = F.obj S.X₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<GOAL>(S.map F).f = F.map S.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<GOAL>(S.map F).X₁ = F.obj S.X₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>τ : F ⟶ G<GOAL>(S.mapNatTrans τ).τ₂ = τ.app S.X₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>τ : F ⟶ G<GOAL>(S.mapNatTrans τ).τ₁ = τ.app S.X₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>τ : F ⟶ G<GOAL>(S.mapNatTrans τ).τ₃ = τ.app S.X₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>τ : F ≅ G<GOAL>(S.mapNatIso τ).inv = S.mapNatTrans τ.inv
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>τ : F ≅ G<GOAL>(S.mapNatIso τ).hom = S.mapNatTrans τ.hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S : CategoryTheory.ShortComplex C<GOAL>F.mapShortComplex.obj S = S.map F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<GOAL>∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), (F.mapShortComplex.map φ).τ₂ = F.map φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<GOAL>∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), (F.mapShortComplex.map φ).τ₃ = F.map φ.τ₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<GOAL>∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), (F.mapShortComplex.map φ).τ₁ = F.map φ.τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e₁ : S₁.X₁ ≅ S₂.X₁<VAR>e₂ : S₁.X₂ ≅ S₂.X₂<VAR>e₃ : S₁.X₃ ≅ S₂.X₃<VAR>comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom := by aesop_cat<VAR>comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom := by aesop_cat<GOAL>(CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.τ₃ = e₃.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e₁ : S₁.X₁ ≅ S₂.X₁<VAR>e₂ : S₁.X₂ ≅ S₂.X₂<VAR>e₃ : S₁.X₃ ≅ S₂.X₃<VAR>comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom := by aesop_cat<VAR>comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom := by aesop_cat<GOAL>(CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.τ₂ = e₂.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e₁ : S₁.X₁ ≅ S₂.X₁<VAR>e₂ : S₁.X₂ ≅ S₂.X₂<VAR>e₃ : S₁.X₃ ≅ S₂.X₃<VAR>comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom := by aesop_cat<VAR>comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom := by aesop_cat<GOAL>(CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).inv = CategoryTheory.ShortComplex.homMk e₁.inv e₂.inv e₃.inv ⋯ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e₁ : S₁.X₁ ≅ S₂.X₁<VAR>e₂ : S₁.X₂ ≅ S₂.X₂<VAR>e₃ : S₁.X₃ ≅ S₂.X₃<VAR>comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom := by aesop_cat<VAR>comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom := by aesop_cat<GOAL>(CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.τ₁ = e₁.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>f : S₁ ⟶ S₂<VAR>CategoryTheory.IsIso f.τ₁<VAR>CategoryTheory.IsIso f.τ₂<VAR>CategoryTheory.IsIso f.τ₃<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.op.X₁ = Opposite.op S.X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.op.g = S.f.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.op.f = S.g.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.op.X₂ = Opposite.op S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.op.X₃ = Opposite.op S.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<GOAL>(CategoryTheory.ShortComplex.opMap φ).τ₂ = φ.τ₂.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<GOAL>(CategoryTheory.ShortComplex.opMap φ).τ₁ = φ.τ₃.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<GOAL>(CategoryTheory.ShortComplex.opMap φ).τ₃ = φ.τ₁.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.ShortComplex.opMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id S.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<GOAL>S.unop.X₁ = Opposite.unop S.X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<GOAL>S.unop.X₂ = Opposite.unop S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<GOAL>S.unop.f = S.g.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<GOAL>S.unop.X₃ = Opposite.unop S.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<GOAL>S.unop.g = S.f.unop