ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<GOAL>(h.map F).Q = F.obj h.Q
<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>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<GOAL>(h.map F).ι = F.map h.ι
<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>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<GOAL>(h.map F).p = F.map h.p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.IsPreservedBy F<GOAL>(h.map F).g' = F.map h.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>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h₁.IsPreservedBy F<VAR>h₂.IsPreservedBy F<GOAL>(ψ.map F).φH = F.map ψ.φH
<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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h₁.IsPreservedBy F<VAR>h₂.IsPreservedBy F<GOAL>(ψ.map F).φQ = F.map ψ.φQ
<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>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.left.IsPreservedBy F<VAR>h.right.IsPreservedBy F<GOAL>(h.map F).iso = F.mapIso h.iso
<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>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.left.IsPreservedBy F<VAR>h.right.IsPreservedBy F<GOAL>(h.map F).left = h.left.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>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h.left.IsPreservedBy F<VAR>h.right.IsPreservedBy F<GOAL>(h.map F).right = h.right.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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h₁.left.IsPreservedBy F<VAR>h₁.right.IsPreservedBy F<VAR>h₂.left.IsPreservedBy F<VAR>h₂.right.IsPreservedBy F<GOAL>(ψ.map F).right = ψ.right.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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h₁.left.IsPreservedBy F<VAR>h₁.right.IsPreservedBy F<VAR>h₂.left.IsPreservedBy F<VAR>h₂.right.IsPreservedBy F<GOAL>(ψ.map F).left = ψ.left.map F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>hl₁.IsPreservedBy F<VAR>hl₂.IsPreservedBy F<GOAL>F.map (CategoryTheory.ShortComplex.cyclesMap' φ hl₁ hl₂) = CategoryTheory.ShortComplex.cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>hl₁.IsPreservedBy F<VAR>hl₂.IsPreservedBy F<GOAL>F.map (CategoryTheory.ShortComplex.leftHomologyMap' φ hl₁ hl₂) = CategoryTheory.ShortComplex.leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hr₁ : S₁.RightHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>hr₁.IsPreservedBy F<VAR>hr₂.IsPreservedBy F<GOAL>F.map (CategoryTheory.ShortComplex.opcyclesMap' φ hr₁ hr₂) = CategoryTheory.ShortComplex.opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hr₁ : S₁.RightHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>hr₁.IsPreservedBy F<VAR>hr₂.IsPreservedBy F<GOAL>F.map (CategoryTheory.ShortComplex.rightHomologyMap' φ hr₁ hr₂) = CategoryTheory.ShortComplex.rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>h₁.left.IsPreservedBy F<VAR>h₁.right.IsPreservedBy F<VAR>h₂.left.IsPreservedBy F<VAR>h₂.right.IsPreservedBy F<GOAL>F.map (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂) = CategoryTheory.ShortComplex.homologyMap' (F.mapShortComplex.map φ) (h₁.map F) (h₂.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>S : CategoryTheory.ShortComplex C<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S.HasLeftHomology<VAR>F.PreservesLeftHomologyOf S<GOAL>CategoryTheory.CategoryStruct.comp (S.mapCyclesIso F).hom (F.map S.iCycles) = (S.map F).iCycles
<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>S : CategoryTheory.ShortComplex C<VAR>hl : S.LeftHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S.HasLeftHomology<VAR>F.PreservesLeftHomologyOf S<GOAL>S.mapCyclesIso F = (hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm
<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>S : CategoryTheory.ShortComplex C<VAR>hl : S.LeftHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S.HasLeftHomology<VAR>F.PreservesLeftHomologyOf S<GOAL>S.mapLeftHomologyIso F = (hl.map F).leftHomologyIso ≪≫ F.mapIso hl.leftHomologyIso.symm
<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>S : CategoryTheory.ShortComplex C<VAR>hr : S.RightHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S.HasRightHomology<VAR>F.PreservesRightHomologyOf S<GOAL>S.mapOpcyclesIso F = (hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm
<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>S : CategoryTheory.ShortComplex C<VAR>hr : S.RightHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S.HasRightHomology<VAR>F.PreservesRightHomologyOf S<GOAL>S.mapRightHomologyIso F = (hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm
<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>S : CategoryTheory.ShortComplex C<VAR>hl : S.LeftHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S.HasHomology<VAR>(S.map F).HasHomology<VAR>F.PreservesLeftHomologyOf S<GOAL>S.mapHomologyIso F = (hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm
<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>S : CategoryTheory.ShortComplex C<VAR>hr : S.RightHomologyData<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S.HasHomology<VAR>(S.map F).HasHomology<VAR>F.PreservesRightHomologyOf S<GOAL>S.mapHomologyIso' F = (hr.map F).homologyIso ≪≫ F.mapIso hr.homologyIso.symm
<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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<VAR>F.PreservesLeftHomologyOf S₁<VAR>F.PreservesLeftHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.map φ)) (S₂.mapCyclesIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).hom (F.map (CategoryTheory.ShortComplex.cyclesMap φ))
<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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<VAR>F.PreservesLeftHomologyOf S₁<VAR>F.PreservesLeftHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.cyclesMap φ)) (S₂.mapCyclesIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).inv (CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<VAR>F.PreservesLeftHomologyOf S₁<VAR>F.PreservesLeftHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.map φ)) (S₂.mapLeftHomologyIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).hom (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ))
<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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasLeftHomology<VAR>S₂.HasLeftHomology<VAR>F.PreservesLeftHomologyOf S₁<VAR>F.PreservesLeftHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ)) (S₂.mapLeftHomologyIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).inv (CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<VAR>F.PreservesRightHomologyOf S₁<VAR>F.PreservesRightHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.map φ)) (S₂.mapOpcyclesIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).hom (F.map (CategoryTheory.ShortComplex.opcyclesMap φ))
<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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<VAR>F.PreservesRightHomologyOf S₁<VAR>F.PreservesRightHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.opcyclesMap φ)) (S₂.mapOpcyclesIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).inv (CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<VAR>F.PreservesRightHomologyOf S₁<VAR>F.PreservesRightHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.map φ)) (S₂.mapRightHomologyIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).hom (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ))
<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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasRightHomology<VAR>S₂.HasRightHomology<VAR>F.PreservesRightHomologyOf S₁<VAR>F.PreservesRightHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ)) (S₂.mapRightHomologyIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).inv (CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>(S₁.map F).HasHomology<VAR>(S₂.map F).HasHomology<VAR>F.PreservesLeftHomologyOf S₁<VAR>F.PreservesLeftHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ)) (S₂.mapHomologyIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).hom (F.map (CategoryTheory.ShortComplex.homologyMap φ))
<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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>(S₁.map F).HasHomology<VAR>(S₂.map F).HasHomology<VAR>F.PreservesLeftHomologyOf S₁<VAR>F.PreservesLeftHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) (S₂.mapHomologyIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).inv (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>(S₁.map F).HasHomology<VAR>(S₂.map F).HasHomology<VAR>F.PreservesRightHomologyOf S₁<VAR>F.PreservesRightHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ)) (S₂.mapHomologyIso' F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).hom (F.map (CategoryTheory.ShortComplex.homologyMap φ))
<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>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S₁.HasHomology<VAR>S₂.HasHomology<VAR>(S₁.map F).HasHomology<VAR>(S₂.map F).HasHomology<VAR>F.PreservesRightHomologyOf S₁<VAR>F.PreservesRightHomologyOf S₂<GOAL>CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) (S₂.mapHomologyIso' F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).inv (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.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>S : CategoryTheory.ShortComplex C<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>S.HasHomology<VAR>F.PreservesLeftHomologyOf S<VAR>F.PreservesRightHomologyOf S<GOAL>S.mapHomologyIso' F = S.mapHomologyIso 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>S : CategoryTheory.ShortComplex C<VAR>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>F.PreservesLeftHomologyOf S<VAR>G.PreservesLeftHomologyOf S<VAR>h : S.LeftHomologyData<VAR>τ : F ⟶ G<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h τ).φH = τ.app h.H
<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>S : CategoryTheory.ShortComplex C<VAR>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>F.PreservesLeftHomologyOf S<VAR>G.PreservesLeftHomologyOf S<VAR>h : S.LeftHomologyData<VAR>τ : F ⟶ G<GOAL>(CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h τ).φK = τ.app h.K
<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>S : CategoryTheory.ShortComplex C<VAR>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>F.PreservesRightHomologyOf S<VAR>G.PreservesRightHomologyOf S<VAR>h : S.RightHomologyData<VAR>τ : F ⟶ G<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h τ).φH = τ.app h.H
<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>S : CategoryTheory.ShortComplex C<VAR>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>F.PreservesRightHomologyOf S<VAR>G.PreservesRightHomologyOf S<VAR>h : S.RightHomologyData<VAR>τ : F ⟶ G<GOAL>(CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h τ).φQ = τ.app h.Q
<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>S : CategoryTheory.ShortComplex C<VAR>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>F.PreservesLeftHomologyOf S<VAR>G.PreservesLeftHomologyOf S<VAR>F.PreservesRightHomologyOf S<VAR>G.PreservesRightHomologyOf S<VAR>h : S.HomologyData<VAR>τ : F ⟶ G<GOAL>(CategoryTheory.ShortComplex.HomologyMapData.natTransApp h τ).right = CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h.right τ
<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>S : CategoryTheory.ShortComplex C<VAR>F G : CategoryTheory.Functor C D<VAR>F.PreservesZeroMorphisms<VAR>G.PreservesZeroMorphisms<VAR>F.PreservesLeftHomologyOf S<VAR>G.PreservesLeftHomologyOf S<VAR>F.PreservesRightHomologyOf S<VAR>G.PreservesRightHomologyOf S<VAR>h : S.HomologyData<VAR>τ : F ⟶ G<GOAL>(CategoryTheory.ShortComplex.HomologyMapData.natTransApp h τ).left = CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h.left τ