ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.Epi (φ.f i)<GOAL>CategoryTheory.Epi φ
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>i : ι<VAR>C : HomologicalComplex V c<GOAL>(HomologicalComplex.eval V c i).obj C = 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>i : ι<GOAL>∀ {X Y : HomologicalComplex V c} (f : X ⟶ Y), (HomologicalComplex.eval V c i).map f = f.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<GOAL>∀ {X Y : HomologicalComplex V c} (f : X ⟶ Y) (i : ι), (HomologicalComplex.forget V c).map f i = f.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 : HomologicalComplex V c<GOAL>∀ (a : ι), (HomologicalComplex.forget V c).obj C a = C.X a
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>i : ι<VAR>X : HomologicalComplex V c<GOAL>(HomologicalComplex.forgetEval V c i).inv.app X = 𝟙 (X.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>i : ι<VAR>X : HomologicalComplex V c<GOAL>(HomologicalComplex.forgetEval V c i).hom.app X = 𝟙 (X.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>K L : HomologicalComplex V c<VAR>φ : K ⟶ L<VAR>n n' : ι<VAR>h : n = n'<GOAL>φ.f n ≫ (L.XIsoOfEq h).hom = (K.XIsoOfEq h).hom ≫ φ.f n'
<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>n n' : ι<VAR>h : n = n'<GOAL>φ.f n' ≫ (L.XIsoOfEq h).inv = (K.XIsoOfEq h).inv ≫ φ.f n
<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 j' : ι<VAR>rij : c.Rel i j<VAR>rij' : c.Rel i j'<GOAL>C.d i j' ≫ CategoryTheory.eqToHom ⋯ = C.d i 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 : HomologicalComplex V c<VAR>i i' j : ι<VAR>rij : c.Rel i j<VAR>rij' : c.Rel i' j<GOAL>CategoryTheory.eqToHom ⋯ ≫ C.d i' j = C.d i 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 : HomologicalComplex V c<VAR>CategoryTheory.Limits.HasKernels V<VAR>i j j' : ι<VAR>r : c.Rel i j<VAR>r' : c.Rel i j'<GOAL>CategoryTheory.Limits.kernelSubobject (C.d i j) = CategoryTheory.Limits.kernelSubobject (C.d i 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 : HomologicalComplex V c<VAR>CategoryTheory.Limits.HasImages V<VAR>CategoryTheory.Limits.HasEqualizers V<VAR>i i' j : ι<VAR>r : c.Rel i j<VAR>r' : c.Rel i' j<GOAL>CategoryTheory.Limits.imageSubobject (C.d i j) = CategoryTheory.Limits.imageSubobject (C.d i' 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 : HomologicalComplex V c<VAR>i j : ι<VAR>r : c.Rel i j<GOAL>C.dTo j = (C.xPrevIso r).hom ≫ C.d i 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 : HomologicalComplex V c<VAR>j : ι<VAR>h : ¬c.Rel (c.prev j) j<GOAL>C.dTo 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 : ι<VAR>r : c.Rel i j<GOAL>C.dFrom i = C.d i j ≫ (C.xNextIso r).inv
<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 : ι<VAR>h : ¬c.Rel i (c.next i)<GOAL>C.dFrom 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>C : HomologicalComplex V c<VAR>i j : ι<VAR>r : c.Rel i j<GOAL>(C.xPrevIso r).inv ≫ C.dTo j = C.d i 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 : HomologicalComplex V c<VAR>j : ι<VAR>h : ¬c.Rel (c.prev j) j<GOAL>(C.xPrevIsoSelf h).inv ≫ C.dTo 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 : ι<VAR>r : c.Rel i j<GOAL>C.dFrom i ≫ (C.xNextIso r).hom = C.d i 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 : HomologicalComplex V c<VAR>i : ι<VAR>h : ¬c.Rel i (c.next i)<GOAL>C.dFrom i ≫ (C.xNextIsoSelf h).hom = 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>j : ι<GOAL>C.dTo j ≫ C.dFrom 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>CategoryTheory.Limits.HasKernels V<VAR>i j : ι<VAR>r : c.Rel i j<GOAL>CategoryTheory.Limits.kernelSubobject (C.dFrom i) = CategoryTheory.Limits.kernelSubobject (C.d i 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 : HomologicalComplex V c<VAR>CategoryTheory.Limits.HasImages V<VAR>CategoryTheory.Limits.HasEqualizers V<VAR>i j : ι<VAR>r : c.Rel i j<GOAL>CategoryTheory.Limits.imageSubobject (C.dTo j) = CategoryTheory.Limits.imageSubobject (C.d i 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₁ C₂ : HomologicalComplex V c<VAR>f : C₁ ≅ C₂<VAR>i : ι<GOAL>(HomologicalComplex.Hom.isoApp f i).hom = f.hom.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>f : C₁ ≅ C₂<VAR>i : ι<GOAL>(HomologicalComplex.Hom.isoApp f i).inv = f.inv.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>f : (i : ι) → C₁.X i ≅ C₂.X i<VAR>hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom := by aesop_cat<VAR>i : ι<GOAL>(HomologicalComplex.Hom.isoOfComponents f hf).hom.f i = (f i).hom
<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>f : (i : ι) → C₁.X i ≅ C₂.X i<VAR>hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom := by aesop_cat<VAR>i : ι<GOAL>(HomologicalComplex.Hom.isoOfComponents f hf).inv.f i = (f i).inv
<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>f : (i : ι) → C₁.X i ≅ C₂.X i<VAR>hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom<VAR>i : ι<GOAL>HomologicalComplex.Hom.isoApp (HomologicalComplex.Hom.isoOfComponents f hf) i = 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>f : C₁ ⟶ C₂<VAR>∀ (n : ι), CategoryTheory.IsIso (f.f n)<GOAL>CategoryTheory.IsIso 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₁ C₂ : HomologicalComplex V c<VAR>f : C₁.Hom C₂<VAR>i j : ι<VAR>w : c.Rel i j<GOAL>f.prev j = (C₁.xPrevIso w).hom ≫ f.f i ≫ (C₂.xPrevIso w).inv
<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>f : C₁.Hom C₂<VAR>i j : ι<VAR>w : c.Rel i j<GOAL>f.next i = (C₁.xNextIso w).hom ≫ f.f j ≫ (C₂.xNextIso w).inv
<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>f : C₁.Hom C₂<VAR>i : ι<GOAL>f.f i ≫ C₂.dFrom i = C₁.dFrom i ≫ f.next 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>f : C₁.Hom C₂<VAR>j : ι<GOAL>f.prev j ≫ C₂.dTo j = C₁.dTo 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₁ C₂ : HomologicalComplex V c<VAR>f : C₁.Hom C₂<VAR>i : ι<GOAL>(f.sqFrom i).left = f.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>f : C₁.Hom C₂<VAR>i : ι<GOAL>(f.sqFrom i).right = f.next 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₁ : HomologicalComplex V c<VAR>i : ι<GOAL>HomologicalComplex.Hom.sqFrom (𝟙 C₁) i = 𝟙 (CategoryTheory.Arrow.mk (C₁.dFrom 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>HomologicalComplex.Hom.sqFrom (f ≫ g) i = HomologicalComplex.Hom.sqFrom f i ≫ HomologicalComplex.Hom.sqFrom g 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>f : C₁.Hom C₂<VAR>j : ι<GOAL>(f.sqTo j).left = f.prev 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₁ C₂ : HomologicalComplex V c<VAR>f : C₁.Hom C₂<VAR>j : ι<GOAL>(f.sqTo j).right = f.f j
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>DecidableEq α<VAR>X : α → V<VAR>d : (n : α) → X (n + 1) ⟶ X n<VAR>sq : ∀ (n : α), d (n + 1) ≫ d n = 0<VAR>n : α<GOAL>(ChainComplex.of X d sq).X n = X n
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>DecidableEq α<VAR>X : α → V<VAR>d : (n : α) → X (n + 1) ⟶ X n<VAR>sq : ∀ (n : α), d (n + 1) ≫ d n = 0<VAR>j : α<GOAL>(ChainComplex.of X d sq).d (j + 1) j = d j
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>DecidableEq α<VAR>X : α → V<VAR>d : (n : α) → X (n + 1) ⟶ X n<VAR>sq : ∀ (n : α), d (n + 1) ≫ d n = 0<VAR>i j : α<VAR>h : i ≠ j + 1<GOAL>(ChainComplex.of X d sq).d i j = 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>DecidableEq α<VAR>X : α → V<VAR>d_X : (n : α) → X (n + 1) ⟶ X n<VAR>sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0<VAR>Y : α → V<VAR>d_Y : (n : α) → Y (n + 1) ⟶ Y n<VAR>sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0<VAR>f : (i : α) → X i ⟶ Y i<VAR>comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i<VAR>i : α<GOAL>(ChainComplex.ofHom X d_X sq_X Y d_Y sq_Y f comm).f i = f i
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₁ ⟶ X₀<VAR>d₁ : X₂ ⟶ X₁<VAR>s : d₁ ≫ d₀ = 0<VAR>succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0<GOAL>(ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 0 = X₀
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₁ ⟶ X₀<VAR>d₁ : X₂ ⟶ X₁<VAR>s : d₁ ≫ d₀ = 0<VAR>succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0<GOAL>(ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 1 = X₁
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₁ ⟶ X₀<VAR>d₁ : X₂ ⟶ X₁<VAR>s : d₁ ≫ d₀ = 0<VAR>succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0<GOAL>(ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 2 = X₂
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₁ ⟶ X₀<VAR>d₁ : X₂ ⟶ X₁<VAR>s : d₁ ≫ d₀ = 0<VAR>succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0<GOAL>(ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 0 = d₀
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₁ ⟶ X₀<VAR>d₁ : X₂ ⟶ X₁<VAR>s : d₁ ≫ d₀ = 0<VAR>succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0<GOAL>(ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ : V<VAR>d₀ : X₁ ⟶ X₀<VAR>succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0<GOAL>(ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').X 0 = X₀
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ : V<VAR>d₀ : X₁ ⟶ X₀<VAR>succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0<GOAL>(ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').X 1 = X₁
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ : V<VAR>d₀ : X₁ ⟶ X₀<VAR>succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0<GOAL>(ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').d 1 0 = d₀
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>P Q : ChainComplex V ℕ<VAR>zero : P.X 0 ⟶ Q.X 0<VAR>one : P.X 1 ⟶ Q.X 1<VAR>one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero<VAR>succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst<GOAL>(P.mkHom Q zero one one_zero_comm succ).f 0 = zero
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>P Q : ChainComplex V ℕ<VAR>zero : P.X 0 ⟶ Q.X 0<VAR>one : P.X 1 ⟶ Q.X 1<VAR>one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero<VAR>succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst<GOAL>(P.mkHom Q zero one one_zero_comm succ).f 1 = one
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>P Q : ChainComplex V ℕ<VAR>zero : P.X 0 ⟶ Q.X 0<VAR>one : P.X 1 ⟶ Q.X 1<VAR>one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero<VAR>succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst<VAR>n : ℕ<GOAL>(P.mkHom Q zero one one_zero_comm succ).f (n + 2) = (succ n ⟨(P.mkHom Q zero one one_zero_comm succ).f n, ⟨(P.mkHom Q zero one one_zero_comm succ).f (n + 1), ⋯⟩⟩).fst
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>DecidableEq α<VAR>X : α → V<VAR>d : (n : α) → X n ⟶ X (n + 1)<VAR>sq : ∀ (n : α), d n ≫ d (n + 1) = 0<VAR>n : α<GOAL>(CochainComplex.of X d sq).X n = X n
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>DecidableEq α<VAR>X : α → V<VAR>d : (n : α) → X n ⟶ X (n + 1)<VAR>sq : ∀ (n : α), d n ≫ d (n + 1) = 0<VAR>j : α<GOAL>(CochainComplex.of X d sq).d j (j + 1) = d j
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>DecidableEq α<VAR>X : α → V<VAR>d : (n : α) → X n ⟶ X (n + 1)<VAR>sq : ∀ (n : α), d n ≫ d (n + 1) = 0<VAR>i j : α<VAR>h : i + 1 ≠ j<GOAL>(CochainComplex.of X d sq).d i j = 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>DecidableEq α<VAR>X : α → V<VAR>d_X : (n : α) → X n ⟶ X (n + 1)<VAR>sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0<VAR>Y : α → V<VAR>d_Y : (n : α) → Y n ⟶ Y (n + 1)<VAR>sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0<VAR>f : (i : α) → X i ⟶ Y i<VAR>comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)<VAR>i : α<GOAL>(CochainComplex.ofHom X d_X sq_X Y d_Y sq_Y f comm).f i = f i
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₀ ⟶ X₁<VAR>d₁ : X₁ ⟶ X₂<VAR>s : d₀ ≫ d₁ = 0<VAR>succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0<GOAL>(CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 0 = X₀
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₀ ⟶ X₁<VAR>d₁ : X₁ ⟶ X₂<VAR>s : d₀ ≫ d₁ = 0<VAR>succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0<GOAL>(CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 1 = X₁
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₀ ⟶ X₁<VAR>d₁ : X₁ ⟶ X₂<VAR>s : d₀ ≫ d₁ = 0<VAR>succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0<GOAL>(CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 2 = X₂
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₀ ⟶ X₁<VAR>d₁ : X₁ ⟶ X₂<VAR>s : d₀ ≫ d₁ = 0<VAR>succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0<GOAL>(CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 0 1 = d₀
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₀ ⟶ X₁<VAR>d₁ : X₁ ⟶ X₂<VAR>s : d₀ ≫ d₁ = 0<VAR>succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0<GOAL>(CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 2 = d₁
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ : V<VAR>d₀ : X₀ ⟶ X₁<VAR>succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0<GOAL>(CochainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').X 0 = X₀
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ : V<VAR>d₀ : X₀ ⟶ X₁<VAR>succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0<GOAL>(CochainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').X 1 = X₁
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X₀ X₁ : V<VAR>d₀ : X₀ ⟶ X₁<VAR>succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0<GOAL>(CochainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').d 0 1 = d₀
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>P Q : CochainComplex V ℕ<VAR>zero : P.X 0 ⟶ Q.X 0<VAR>one : P.X 1 ⟶ Q.X 1<VAR>one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one<VAR>succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' p.snd.fst ≫ Q.d (n + 1) (n + 2) = P.d (n + 1) (n + 2) ≫ f''<GOAL>(P.mkHom Q zero one one_zero_comm succ).f 0 = zero
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>P Q : CochainComplex V ℕ<VAR>zero : P.X 0 ⟶ Q.X 0<VAR>one : P.X 1 ⟶ Q.X 1<VAR>one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one<VAR>succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' p.snd.fst ≫ Q.d (n + 1) (n + 2) = P.d (n + 1) (n + 2) ≫ f''<GOAL>(P.mkHom Q zero one one_zero_comm succ).f 1 = one
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>P Q : CochainComplex V ℕ<VAR>zero : P.X 0 ⟶ Q.X 0<VAR>one : P.X 1 ⟶ Q.X 1<VAR>one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one<VAR>succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' p.snd.fst ≫ Q.d (n + 1) (n + 2) = P.d (n + 1) (n + 2) ≫ f''<VAR>n : ℕ<GOAL>(P.mkHom Q zero one one_zero_comm succ).f (n + 2) = (succ n ⟨(P.mkHom Q zero one one_zero_comm succ).f n, ⟨(P.mkHom Q zero one one_zero_comm succ).f (n + 1), ⋯⟩⟩).fst
<VAR>S : CategoryTheory.ShortComplex Ab<VAR>x : ↑S.X₁<GOAL>S.g (S.f x) = 0
<VAR>S : CategoryTheory.ShortComplex Ab<VAR>x : ↑S.X₁<GOAL>↑(S.abToCycles x) = S.f x
<VAR>S : CategoryTheory.ShortComplex Ab<GOAL>S.abLeftHomologyData.i = (AddMonoidHom.ker S.g).subtype
<VAR>S : CategoryTheory.ShortComplex Ab<GOAL>S.abLeftHomologyData.H = AddCommGrp.of (↥(AddMonoidHom.ker S.g) ⧸ S.abToCycles.range)
<VAR>S : CategoryTheory.ShortComplex Ab<GOAL>S.abLeftHomologyData.K = AddCommGrp.of ↥(AddMonoidHom.ker S.g)
<VAR>S : CategoryTheory.ShortComplex Ab<GOAL>S.abLeftHomologyData.π = QuotientAddGroup.mk' S.abToCycles.range
<VAR>S : CategoryTheory.ShortComplex Ab<GOAL>S.abLeftHomologyData.f' = S.abToCycles
<VAR>S : CategoryTheory.ShortComplex Ab<VAR>x : ↥(AddMonoidHom.ker S.g)<GOAL>S.iCycles (S.abCyclesIso.inv x) = ↑x
<VAR>S : CategoryTheory.ShortComplex Ab<GOAL>S.Exact ↔ Function.Surjective ⇑S.abToCycles
<VAR>S : CategoryTheory.ShortComplex Ab<GOAL>S.Exact ↔ ∀ (x₂ : ↑S.X₂), S.g x₂ = 0 → ∃ x₁, S.f x₁ = x₂
<VAR>S : CategoryTheory.ShortComplex Ab<GOAL>S.Exact ↔ AddMonoidHom.ker S.g ≤ AddMonoidHom.range S.f
<VAR>S : CategoryTheory.ShortComplex Ab<GOAL>S.Exact ↔ AddMonoidHom.range S.f = AddMonoidHom.ker S.g
<VAR>S : CategoryTheory.ShortComplex Ab<VAR>hS : S.ShortExact<GOAL>Function.Injective ⇑S.f
<VAR>S : CategoryTheory.ShortComplex Ab<VAR>hS : S.ShortExact<GOAL>Function.Surjective ⇑S.g
<VAR>S : CategoryTheory.ShortComplex Ab<GOAL>S.Exact ↔ Function.Exact ⇑S.f ⇑S.g
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive 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.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f g : C ⟶ D<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.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : C ⟶ D<VAR>i : ι<GOAL>(-f).f i = -f.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>i : ι<GOAL>(f - g).f i = f.f i - g.f i