ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernels V<VAR>CategoryTheory.Limits.HasImages V<VAR>Z : V<VAR>h : Z ⟶ A<VAR>CategoryTheory.Epi h<VAR>w : (h ≫ f) ≫ g = 0<GOAL>imageToKernel (h ≫ f) g w = (CategoryTheory.Limits.imageSubobject (h ≫ f)).ofLE (CategoryTheory.Limits.imageSubobject f) ⋯ ≫ imageToKernel f g ⋯
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasEqualizers V<VAR>CategoryTheory.Limits.HasImages V<VAR>Z : V<VAR>i : B ≅ Z<VAR>w : (f ≫ i.hom) ≫ i.inv ≫ g = 0<GOAL>imageToKernel (f ≫ i.hom) (i.inv ≫ g) w = (CategoryTheory.Limits.imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g ⋯ ≫ (CategoryTheory.Limits.kernelSubobjectIsoComp i.inv g).inv
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernels V<VAR>CategoryTheory.Limits.HasImages V<VAR>w : f ≫ g = 0<GOAL>(CategoryTheory.Limits.imageSubobjectIso f).hom ≫ imageToKernel' f g w = imageToKernel f g w ≫ (CategoryTheory.Limits.kernelSubobjectIso g).hom
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernels V<VAR>CategoryTheory.Limits.HasImages V<VAR>w : f ≫ g = 0<GOAL>imageToKernel' f g w ≫ (CategoryTheory.Limits.kernelSubobjectIso g).inv = (CategoryTheory.Limits.imageSubobjectIso f).inv ≫ imageToKernel f g w
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₂ = (HomologicalComplex.cyclesFunctor C c j).mapShortComplex.map φ
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₃ = (HomologicalComplex.homologyFunctor C c j).mapShortComplex.map φ
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₁ = (HomologicalComplex.opcyclesFunctor C c i).mapShortComplex.map φ
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₀ = (HomologicalComplex.homologyFunctor C c i).mapShortComplex.map φ
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>hS₁.δ i j hij ≫ HomologicalComplex.homologyMap φ.τ₁ j = HomologicalComplex.homologyMap φ.τ₃ i ≫ hS₂.δ i j hij
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS₁ : S₁.ShortExact<VAR>i : ι<GOAL>(HomologicalComplex.HomologySequence.composableArrows₂ S₁ i).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS₁ : S₁.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(HomologicalComplex.HomologySequence.composableArrows₅ hS₁ i j hij).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>i : ι<VAR>h₁ : CategoryTheory.Epi (HomologicalComplex.homologyMap φ.τ₁ i)<VAR>h₂ : CategoryTheory.Mono (HomologicalComplex.homologyMap φ.τ₂ i)<VAR>h₃ : ∀ (j : ι), c.Rel i j → CategoryTheory.Mono (HomologicalComplex.homologyMap φ.τ₁ j)<GOAL>CategoryTheory.Mono (HomologicalComplex.homologyMap φ.τ₃ i)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>i : ι<VAR>h₁ : CategoryTheory.Epi (HomologicalComplex.homologyMap φ.τ₂ i)<VAR>h₂ : ∀ (j : ι), c.Rel i j → CategoryTheory.Epi (HomologicalComplex.homologyMap φ.τ₁ j)<VAR>h₃ : ∀ (j : ι), c.Rel i j → CategoryTheory.Mono (HomologicalComplex.homologyMap φ.τ₂ j)<GOAL>CategoryTheory.Epi (HomologicalComplex.homologyMap φ.τ₃ i)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>i : ι<VAR>h₁ : CategoryTheory.Epi (HomologicalComplex.homologyMap φ.τ₁ i)<VAR>h₂ : CategoryTheory.IsIso (HomologicalComplex.homologyMap φ.τ₂ i)<VAR>h₃ : ∀ (j : ι), c.Rel i j → CategoryTheory.IsIso (HomologicalComplex.homologyMap φ.τ₁ j)<VAR>h₄ : ∀ (j : ι), c.Rel i j → CategoryTheory.Mono (HomologicalComplex.homologyMap φ.τ₂ j)<GOAL>CategoryTheory.IsIso (HomologicalComplex.homologyMap φ.τ₃ i)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>c : ComplexShape ι<VAR>S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>h₁ : QuasiIso φ.τ₁<VAR>h₂ : QuasiIso φ.τ₂<GOAL>QuasiIso φ.τ₃
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)<VAR>i : β<GOAL>X.objEqToHom ⋯ = 𝟙 (X.obj i)
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)<VAR>x y : β<VAR>h : x = y<GOAL>X.objEqToHom h ≫ X.d y = X.d x ≫ X.objEqToHom ⋯
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)<VAR>x : β<GOAL>X.d x ≫ X.d ((fun b_1 => b_1 + { as := 1 }.as • b) x) = 0
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)<VAR>f : X ⟶ Y<VAR>x y : β<VAR>h : x = y<GOAL>X.objEqToHom h ≫ f.f y = f.f x ≫ Y.objEqToHom h
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex V (ComplexShape.up' b)<VAR>x y z : β<VAR>h : y = z<GOAL>X.d x y ≫ CategoryTheory.eqToHom ⋯ = X.d x z
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)<VAR>i j : β<GOAL>((HomologicalComplex.dgoToHomologicalComplex b V).obj X).d i j = if h : i + b = j then X.d i ≫ X.objEqToHom ⋯ else 0
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)<VAR>i : β<GOAL>((HomologicalComplex.dgoToHomologicalComplex b V).obj X).X i = X.obj i
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)<VAR>f : X ⟶ Y<VAR>i : β<GOAL>((HomologicalComplex.dgoToHomologicalComplex b V).map f).f i = f.f i
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex V (ComplexShape.up' b)<VAR>i : β<GOAL>((HomologicalComplex.homologicalComplexToDGO b V).obj X).obj i = X.X i
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex V (ComplexShape.up' b)<VAR>i : β<GOAL>((HomologicalComplex.homologicalComplexToDGO b V).obj X).d i = X.d i ((fun b_1 => b_1 + { as := 1 }.as • b) i)
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X Y : HomologicalComplex V (ComplexShape.up' b)<VAR>f : X ⟶ Y<VAR>i : β<GOAL>((HomologicalComplex.homologicalComplexToDGO b V).map f).f i = f.f i
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)<VAR>i : β<GOAL>((HomologicalComplex.dgoEquivHomologicalComplexUnitIso b V).inv.app X).f i = 𝟙 (X.obj i)
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)<VAR>i : β<GOAL>((HomologicalComplex.dgoEquivHomologicalComplexUnitIso b V).hom.app X).f i = 𝟙 (X.obj i)
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex V (ComplexShape.up' b)<VAR>i : β<GOAL>((HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V).hom.app X).f i = 𝟙 (X.X i)
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex V (ComplexShape.up' b)<VAR>i : β<GOAL>((HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V).inv.app X).f i = 𝟙 (X.X i)
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.dgoEquivHomologicalComplex b V).unitIso = HomologicalComplex.dgoEquivHomologicalComplexUnitIso b V
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.dgoEquivHomologicalComplex b V).counitIso = HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.dgoEquivHomologicalComplex b V).inverse = HomologicalComplex.homologicalComplexToDGO b V
<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>(HomologicalComplex.dgoEquivHomologicalComplex b V).functor = HomologicalComplex.dgoToHomologicalComplex b V
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>self : CategoryTheory.ShortComplex.SnakeInput C<GOAL>self.L₁.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>self : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.Epi self.L₁.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>self : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp self.v₁₂ self.v₂₃ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>self : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.Mono self.L₂.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>self : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp self.v₀₁ self.v₁₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>self : CategoryTheory.ShortComplex.SnakeInput C<GOAL>self.L₂.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.op.L₃ = S.L₀.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.op.v₁₂ = CategoryTheory.ShortComplex.opMap S.v₁₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.op.L₁ = S.L₂.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.op.L₀ = S.L₃.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.op.v₂₃ = CategoryTheory.ShortComplex.opMap S.v₀₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.op.v₀₁ = CategoryTheory.ShortComplex.opMap S.v₂₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.op.L₂ = S.L₁.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.v₀₁.τ₁ S.v₁₂.τ₁ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.v₀₁.τ₂ S.v₁₂.τ₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.v₀₁.τ₃ S.v₁₂.τ₃ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.v₁₂.τ₁ S.v₂₃.τ₁ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ S.v₂₃.τ₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.v₁₂.τ₃ S.v₂₃.τ₃ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.ShortComplex.mk S.v₀₁.τ₁ S.v₁₂.τ₁ ⋯).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.ShortComplex.mk S.v₀₁.τ₂ S.v₁₂.τ₂ ⋯).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.ShortComplex.mk S.v₀₁.τ₃ S.v₁₂.τ₃ ⋯).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.ShortComplex.mk S.v₁₂.τ₁ S.v₂₃.τ₁ ⋯).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.ShortComplex.mk S.v₁₂.τ₂ S.v₂₃.τ₂ ⋯).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.ShortComplex.mk S.v₁₂.τ₃ S.v₂₃.τ₃ ⋯).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₀.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₃.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<VAR>A : C<VAR>a : A ⟶ S.L₁.X₂<VAR>b : A ⟶ S.L₀.X₃<VAR>h : CategoryTheory.CategoryStruct.comp a S.L₁.g = CategoryTheory.CategoryStruct.comp b S.v₀₁.τ₃<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift a b h) S.φ₂ = CategoryTheory.CategoryStruct.comp a S.v₁₂.τ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.φ₁ S.L₂.f = S.φ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.L₀'.f S.φ₁ = S.v₁₂.τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₀'.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) S.δ = CategoryTheory.CategoryStruct.comp S.φ₁ S.v₂₃.τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) (CategoryTheory.CategoryStruct.comp S.δ (CategoryTheory.Limits.pushout.inr S.L₂.f S.v₂₃.τ₁)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.L₁.g S.v₀₁.τ₃) (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ (CategoryTheory.Limits.pushout.inl S.L₂.f S.v₂₃.τ₁))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.L₀X₂ToP (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) = S.L₀.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.L₀X₂ToP S.φ₁ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.L₀.g S.δ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>CategoryTheory.CategoryStruct.comp S.δ S.L₃.f = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₁'.g = S.δ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₁'.X₁ = S.L₀.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₁'.X₃ = S.L₃.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₁'.X₂ = S.L₀.X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₁'.f = S.L₀.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₂'.X₃ = S.L₃.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₂'.X₂ = S.L₃.X₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₂'.f = S.δ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₂'.X₁ = S.L₀.X₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₂'.g = S.L₃.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₁'.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.op.δ = S.δ.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.L₂'.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>S.composableArrows.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<VAR>A : C<VAR>x₃ : A ⟶ S.L₀.X₃<VAR>x₂ : A ⟶ S.L₁.X₂<VAR>x₁ : A ⟶ S.L₂.X₁<VAR>h₂ : CategoryTheory.CategoryStruct.comp x₂ S.L₁.g = CategoryTheory.CategoryStruct.comp x₃ S.v₀₁.τ₃<VAR>h₁ : CategoryTheory.CategoryStruct.comp x₁ S.L₂.f = CategoryTheory.CategoryStruct.comp x₂ S.v₁₂.τ₂<GOAL>CategoryTheory.CategoryStruct.comp x₃ S.δ = CategoryTheory.CategoryStruct.comp x₁ S.v₂₃.τ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C<VAR>self : S₁.Hom S₂<GOAL>CategoryTheory.CategoryStruct.comp self.f₁ S₂.v₁₂ = CategoryTheory.CategoryStruct.comp S₁.v₁₂ self.f₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C<VAR>self : S₁.Hom S₂<GOAL>CategoryTheory.CategoryStruct.comp self.f₀ S₂.v₀₁ = CategoryTheory.CategoryStruct.comp S₁.v₀₁ self.f₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C<VAR>self : S₁.Hom S₂<GOAL>CategoryTheory.CategoryStruct.comp self.f₂ S₂.v₂₃ = CategoryTheory.CategoryStruct.comp S₁.v₂₃ self.f₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₀ = CategoryTheory.CategoryStruct.id S.L₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₁ = CategoryTheory.CategoryStruct.id S.L₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex.SnakeInput C<GOAL>(CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₃ = CategoryTheory.CategoryStruct.id S.L₃