ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>n₁ n₂ n₁₂ : ℤ<VAR>h : n₁ + n₂ = n₁₂<VAR>X : CochainComplex C ℤ<VAR>i : ℤ<GOAL>((CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h).hom.app X).f i = (HomologicalComplex.XIsoOfEq X ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>n₁ n₂ n₁₂ : ℤ<VAR>h : n₁ + n₂ = n₁₂<VAR>X : CochainComplex C ℤ<VAR>i : ℤ<GOAL>((CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h).inv.app X).f i = (HomologicalComplex.XIsoOfEq X ⋯).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<VAR>n p : ℤ<GOAL>((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X p = K.X (p + n)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>n p : ℤ<GOAL>((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ).f p = φ.f (p + n)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<VAR>n i j : ℤ<GOAL>((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = n.negOnePow • K.d (i + { as := n }.as) (j + { as := n }.as)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<VAR>a b n : ℤ<GOAL>((CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<VAR>a b n : ℤ<GOAL>((CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<VAR>a b ab : ℤ<VAR>h : a + b = ab<VAR>n : ℤ<GOAL>((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).inv.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<VAR>a b ab : ℤ<VAR>h : a + b = ab<VAR>n : ℤ<GOAL>((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<VAR>n : ℤ<GOAL>((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<VAR>n : ℤ<GOAL>((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<VAR>n : ℤ<VAR>p q : ℤ<VAR>hpq : p = q<GOAL>HomologicalComplex.XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) hpq = HomologicalComplex.XIsoOfEq K ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>a b c : ℤ<VAR>h : a + b = c<GOAL>CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b c h = CochainComplex.shiftFunctorAdd' C a b c h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>a b : ℤ<GOAL>CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b = CochainComplex.shiftFunctorAdd' C a b (a + b) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<GOAL>CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ = CochainComplex.shiftFunctorZero' C 0 ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<VAR>a b p : ℤ<GOAL>((CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) a b).hom.app K).f p = (HomologicalComplex.XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<VAR>X : CochainComplex C ℤ<GOAL>(CochainComplex.shiftEval C n i i' hi).hom.app X = (HomologicalComplex.XIsoOfEq X ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<VAR>X : CochainComplex C ℤ<GOAL>(CochainComplex.shiftEval C n i i' hi).inv.app X = (HomologicalComplex.XIsoOfEq X ⋯).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Preadditive D<VAR>F : C ⥤ D<VAR>F.Additive<VAR>n : ℤ<VAR>X : HomologicalComplex C (ComplexShape.up ℤ)<VAR>i : ℤ<GOAL>((F.mapCochainComplexShiftIso n).hom.app X).f i = 𝟙 (F.obj (X.X (i + n)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Preadditive D<VAR>F : C ⥤ D<VAR>F.Additive<VAR>n : ℤ<VAR>X : HomologicalComplex C (ComplexShape.up ℤ)<VAR>i : ℤ<GOAL>((F.mapCochainComplexShiftIso n).inv.app X).f i = 𝟙 (F.obj (X.X (i + n)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Preadditive D<VAR>F : C ⥤ D<VAR>F.Additive<VAR>n : ℤ<GOAL>(F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n = F.mapCochainComplexShiftIso n
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Preadditive D<VAR>F : C ⥤ D<VAR>F.Additive<VAR>K : CochainComplex C ℤ<VAR>n i : ℤ<GOAL>(((F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n).hom.app K).f i = 𝟙 (((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K).X i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Preadditive D<VAR>F : C ⥤ D<VAR>F.Additive<VAR>K : CochainComplex C ℤ<VAR>n i : ℤ<GOAL>(((F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n).inv.app K).f i = 𝟙 (((F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) n).obj K).X i)
<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.Abelian C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>h : ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Mono (F.map S.f)<GOAL>F.PreservesMonomorphisms
<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.Abelian C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>[∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Mono (F.map S.f), ∀ (S : CategoryTheory.ShortComplex C), S.Exact ∧ CategoryTheory.Mono S.f → (S.map F).Exact ∧ CategoryTheory.Mono (F.map S.f), ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F), Nonempty (CategoryTheory.Limits.PreservesFiniteLimits F)].TFAE
<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.Abelian C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>h : ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g)<GOAL>F.PreservesEpimorphisms
<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.Abelian C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>[∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g), ∀ (S : CategoryTheory.ShortComplex C), S.Exact ∧ CategoryTheory.Epi S.g → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g), ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F), Nonempty (CategoryTheory.Limits.PreservesFiniteColimits F)].TFAE
<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.Abelian C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>[∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : CategoryTheory.ShortComplex C), S.Exact → (S.map F).Exact, Nonempty F.PreservesHomology, Nonempty (CategoryTheory.Limits.PreservesFiniteLimits F) ∧ Nonempty (CategoryTheory.Limits.PreservesFiniteColimits F)].TFAE
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i j k i' j' k' : ℤ<VAR>hi : n + i = i'<VAR>hj : n + j = j'<VAR>hk : n + k = k'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i j k i' j' k' : ℤ<VAR>hi : n + i = i'<VAR>hj : n + j = j'<VAR>hk : n + k = k'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i j k i' j' k' : ℤ<VAR>hi : n + i = i'<VAR>hj : n + j = j'<VAR>hk : n + k = k'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i j k i' j' k' : ℤ<VAR>hi : n + i = i'<VAR>hj : n + j = j'<VAR>hk : n + k = k'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i j k i' j' k' : ℤ<VAR>hi : n + i = i'<VAR>hj : n + j = j'<VAR>hk : n + k = k'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i j k i' j' k' : ℤ<VAR>hi : n + i = i'<VAR>hj : n + j = j'<VAR>hk : n + k = k'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<VAR>X : CochainComplex C ℤ<GOAL>((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>a : ℤ<VAR>K : CochainComplex C ℤ<GOAL>(CochainComplex.shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K = (HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) a).map ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n m mn : ℤ<VAR>hmn : m + n = mn<VAR>a a' a'' : ℤ<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>K : CochainComplex C ℤ<GOAL>(CochainComplex.shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K = (HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) a).map ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫ (CochainComplex.shiftShortComplexFunctorIso C n a a' ha').hom.app ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫ (CochainComplex.shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>n a a' : ℤ<VAR>ha' : n + a = a'<VAR>K : CochainComplex C ℤ<GOAL>(CochainComplex.ShiftSequence.shiftIso C n a a' ha').hom.app K = CategoryTheory.ShortComplex.homologyMap ((CochainComplex.shiftShortComplexFunctorIso C n a a' ha').hom.app K)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>n a a' : ℤ<VAR>ha' : n + a = a'<VAR>K : CochainComplex C ℤ<GOAL>(CochainComplex.ShiftSequence.shiftIso C n a a' ha').inv.app K = CategoryTheory.ShortComplex.homologyMap ((CochainComplex.shiftShortComplexFunctorIso C n a a' ha').inv.app K)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>n i j : ℤ<VAR>h : n + i = j<GOAL>QuasiIsoAt ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ) i ↔ QuasiIsoAt φ j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>n : ℤ<GOAL>QuasiIso ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ) ↔ QuasiIso φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>n : ℤ<GOAL>(HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shift n = HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>K : CochainComplex C ℤ<VAR>A : C<VAR>n i : ℤ<VAR>f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i<VAR>j : ℤ<VAR>hj : (ComplexShape.up ℤ).next i = j<VAR>hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0<VAR>i' : ℤ<VAR>hi' : n + i = i'<VAR>j' : ℤ<VAR>hj' : (ComplexShape.up ℤ).next i' = j'<GOAL>HomologicalComplex.liftCycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) f j hj hf ≫ HomologicalComplex.homologyπ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i = HomologicalComplex.liftCycles K (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) j' hj' ⋯ ≫ HomologicalComplex.homologyπ K i' ≫ ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i i' hi').inv.app K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>n a a' : ℤ<VAR>ha' : n + a = a'<VAR>K : CochainComplex C ℤ<GOAL>((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n a a' ha').hom.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) = (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) a).map (((HomotopyCategory.quotient C (ComplexShape.up ℤ)).commShiftIso n).inv.app K) ≫ (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a).hom.app ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K) ≫ ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n a a' ha').hom.app K ≫ (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a').inv.app K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L<VAR>a a' : ℤ<VAR>h : n + a = a'<GOAL>(HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f ≫ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).commShiftIso n).hom.app L) a a' h = (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a).hom.app K ≫ (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫ (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a').inv.app L
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>self : HomologicalComplex V c<VAR>i j k : ι<GOAL>c.Rel i j → c.Rel j k → self.d i j ≫ self.d j k = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>self : HomologicalComplex V c<VAR>i j : ι<GOAL>¬c.Rel i j → self.d i j = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>i j k : ι<GOAL>C.d i j ≫ C.d j k = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C₁ C₂ : HomologicalComplex V c<VAR>h_X : C₁.X = C₂.X<VAR>h_d : ∀ (i j : ι), c.Rel i j → C₁.d i j ≫ CategoryTheory.eqToHom ⋯ = CategoryTheory.eqToHom ⋯ ≫ C₂.d i j<GOAL>C₁ = C₂
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p : ι<GOAL>K.XIsoOfEq ⋯ = CategoryTheory.Iso.refl (K.X p)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p₁ p₂ p₃ : ι<VAR>h₁₂ : p₁ = p₂<VAR>h₂₃ : p₂ = p₃<GOAL>(K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p₁ p₂ p₃ : ι<VAR>h₁₂ : p₁ = p₂<VAR>h₃₂ : p₃ = p₂<GOAL>(K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p₁ p₂ p₃ : ι<VAR>h₂₁ : p₂ = p₁<VAR>h₂₃ : p₂ = p₃<GOAL>(K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p₁ p₂ p₃ : ι<VAR>h₂₁ : p₂ = p₁<VAR>h₃₂ : p₃ = p₂<GOAL>(K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p₁ p₂ : ι<VAR>h : p₁ = p₂<VAR>p₃ : ι<GOAL>(K.XIsoOfEq h).hom ≫ K.d p₂ p₃ = K.d p₁ p₃
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p₂ p₁ : ι<VAR>h : p₂ = p₁<VAR>p₃ : ι<GOAL>(K.XIsoOfEq h).inv ≫ K.d p₂ p₃ = K.d p₁ p₃
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p₂ p₃ : ι<VAR>h : p₂ = p₃<VAR>p₁ : ι<GOAL>K.d p₁ p₂ ≫ (K.XIsoOfEq h).hom = K.d p₁ p₃
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p₂ p₃ : ι<VAR>h : p₃ = p₂<VAR>p₁ : ι<GOAL>K.d p₁ p₂ ≫ (K.XIsoOfEq h).inv = K.d p₁ p₃
<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>i : α<GOAL>(ComplexShape.down α).prev i = i + 1
<VAR>α : Type u_2<VAR>AddGroup α<VAR>One α<VAR>i : α<GOAL>(ComplexShape.down α).next i = i - 1
<GOAL>(ComplexShape.down ℕ).next 0 = 0
<VAR>i : ℕ<GOAL>(ComplexShape.down ℕ).next (i + 1) = i
<VAR>α : Type u_2<VAR>AddGroup α<VAR>One α<VAR>i : α<GOAL>(ComplexShape.up α).prev i = i - 1
<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>i : α<GOAL>(ComplexShape.up α).next i = i + 1
<GOAL>(ComplexShape.up ℕ).prev 0 = 0
<VAR>i : ℕ<GOAL>(ComplexShape.up ℕ).prev (i + 1) = i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>A B : HomologicalComplex V c<VAR>self : A.Hom B<VAR>i j : ι<GOAL>c.Rel i j → self.f i ≫ B.d i j = A.d i j ≫ self.f j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>A B : HomologicalComplex V c<VAR>f : A.Hom B<VAR>i j : ι<GOAL>f.f i ≫ B.d i j = A.d i j ≫ f.f j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h : ∀ (i : ι), f.f i = g.f i<GOAL>f = g
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>i : ι<GOAL>(𝟙 C).f i = 𝟙 (C.X i)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C₁ C₂ C₃ : HomologicalComplex V c<VAR>f : C₁ ⟶ C₂<VAR>g : C₂ ⟶ C₃<VAR>i : ι<GOAL>(f ≫ g).f i = f.f i ≫ g.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C₁ C₂ : HomologicalComplex V c<VAR>h : C₁ = C₂<VAR>n : ι<GOAL>(CategoryTheory.eqToHom h).f n = CategoryTheory.eqToHom ⋯
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C₁ C₂ : HomologicalComplex V c<GOAL>Function.Injective fun f => f.f
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>i : ι<GOAL>HomologicalComplex.Hom.f 0 i = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroObject V<GOAL>CategoryTheory.Limits.IsZero HomologicalComplex.zero
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>w : f = g<VAR>i : ι<GOAL>f.f i = g.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex V c<VAR>φ : K ⟶ L<VAR>hφ : ∀ (i : ι), CategoryTheory.Mono (φ.f i)<GOAL>CategoryTheory.Mono φ