ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ComposableArrows C 1<GOAL>S.IsComplex
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S : CategoryTheory.ComposableArrows C n<VAR>self : S.Exact<VAR>i : ℕ<VAR>hi : i + 2 ≤ n := by omega<GOAL>(S.sc ⋯ i ⋯).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S : CategoryTheory.ComposableArrows C n<VAR>hS : S.Exact<VAR>i j k : ℕ<VAR>hij : i + 1 = j := by omega<VAR>hjk : j + 1 = k := by omega<VAR>hk : k ≤ n := by omega<GOAL>(S.sc' ⋯ i j k ⋯ ⋯ ⋯).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.IsComplex<VAR>h₂ : S₂.IsComplex<VAR>i j k : ℕ<VAR>hij : i + 1 = j := by omega<VAR>hjk : j + 1 = k := by omega<VAR>hk : k ≤ n := by omega<GOAL>(CategoryTheory.ComposableArrows.sc'Map φ h₁ h₂ i j k hij hjk hk).τ₂ = φ.app ⟨j, ⋯⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.IsComplex<VAR>h₂ : S₂.IsComplex<VAR>i j k : ℕ<VAR>hij : i + 1 = j := by omega<VAR>hjk : j + 1 = k := by omega<VAR>hk : k ≤ n := by omega<GOAL>(CategoryTheory.ComposableArrows.sc'Map φ h₁ h₂ i j k hij hjk hk).τ₁ = φ.app ⟨i, ⋯⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.IsComplex<VAR>h₂ : S₂.IsComplex<VAR>i j k : ℕ<VAR>hij : i + 1 = j := by omega<VAR>hjk : j + 1 = k := by omega<VAR>hk : k ≤ n := by omega<GOAL>(CategoryTheory.ComposableArrows.sc'Map φ h₁ h₂ i j k hij hjk hk).τ₃ = φ.app ⟨k, ⋯⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.IsComplex<VAR>h₂ : S₂.IsComplex<VAR>i : ℕ<VAR>hi : i + 2 ≤ n := by omega<GOAL>(CategoryTheory.ComposableArrows.scMap φ h₁ h₂ i hi).τ₁ = φ.app ⟨i, ⋯⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.IsComplex<VAR>h₂ : S₂.IsComplex<VAR>i : ℕ<VAR>hi : i + 2 ≤ n := by omega<GOAL>(CategoryTheory.ComposableArrows.scMap φ h₁ h₂ i hi).τ₃ = φ.app ⟨i + 2, ⋯⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.IsComplex<VAR>h₂ : S₂.IsComplex<VAR>i : ℕ<VAR>hi : i + 2 ≤ n := by omega<GOAL>(CategoryTheory.ComposableArrows.scMap φ h₁ h₂ i hi).τ₂ = φ.app ⟨i + 1, ⋯⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.IsComplex<VAR>h₂ : S₂.IsComplex<VAR>i j k : ℕ<VAR>hij : i + 1 = j := by omega<VAR>hjk : j + 1 = k := by omega<VAR>hk : k ≤ n := by omega<GOAL>(CategoryTheory.ComposableArrows.sc'MapIso e h₁ h₂ i j k hij hjk hk).hom = CategoryTheory.ComposableArrows.sc'Map e.hom h₁ h₂ i j k ⋯ ⋯ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.IsComplex<VAR>h₂ : S₂.IsComplex<VAR>i j k : ℕ<VAR>hij : i + 1 = j := by omega<VAR>hjk : j + 1 = k := by omega<VAR>hk : k ≤ n := by omega<GOAL>(CategoryTheory.ComposableArrows.sc'MapIso e h₁ h₂ i j k hij hjk hk).inv = CategoryTheory.ComposableArrows.sc'Map e.inv h₂ h₁ i j k ⋯ ⋯ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.IsComplex<VAR>h₂ : S₂.IsComplex<VAR>i : ℕ<VAR>hi : i + 2 ≤ n := by omega<GOAL>(CategoryTheory.ComposableArrows.scMapIso e h₁ h₂ i hi).inv = CategoryTheory.ComposableArrows.scMap e.inv h₂ h₁ i ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.IsComplex<VAR>h₂ : S₂.IsComplex<VAR>i : ℕ<VAR>hi : i + 2 ≤ n := by omega<GOAL>(CategoryTheory.ComposableArrows.scMapIso e h₁ h₂ i hi).hom = CategoryTheory.ComposableArrows.scMap e.hom h₁ h₂ i ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.Exact<GOAL>S₂.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S₁ S₂ : CategoryTheory.ComposableArrows C n<VAR>e : S₁ ≅ S₂<GOAL>S₁.Exact ↔ S₂.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ComposableArrows C 0<GOAL>S.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ComposableArrows C 1<GOAL>S.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ComposableArrows C 2<GOAL>S.IsComplex ↔ CategoryTheory.CategoryStruct.comp (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ComposableArrows C 2<VAR>w : CategoryTheory.CategoryStruct.comp (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯) = 0<GOAL>S.IsComplex
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.toComposableArrows.IsComplex
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ComposableArrows C 2<VAR>hS : S.IsComplex<GOAL>S.Exact ↔ (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ComposableArrows C 2<VAR>w : CategoryTheory.CategoryStruct.comp (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯) = 0<VAR>h : (CategoryTheory.ShortComplex.mk (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯) w).Exact<GOAL>S.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<GOAL>S.toComposableArrows.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.Exact ↔ S.toComposableArrows.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S : CategoryTheory.ComposableArrows C (n + 2)<GOAL>S.Exact ↔ (CategoryTheory.ComposableArrows.mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S : CategoryTheory.ComposableArrows C (n + 2)<VAR>hS : S.Exact<GOAL>S.δ₀.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S : CategoryTheory.ComposableArrows C (n + 2)<VAR>h : (CategoryTheory.ComposableArrows.mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : S.δ₀.Exact<GOAL>S.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S : CategoryTheory.ComposableArrows C (n + 2)<GOAL>S.Exact ↔ S.δlast.Exact ∧ (CategoryTheory.ComposableArrows.mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S : CategoryTheory.ComposableArrows C (n + 2)<VAR>hS : S.Exact<GOAL>S.δlast.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>n : ℕ<VAR>S : CategoryTheory.ComposableArrows C (n + 2)<VAR>h₁ : S.δlast.Exact<VAR>h₂ : (CategoryTheory.ComposableArrows.mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact<GOAL>S.Exact
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} T<VAR>C : HomologicalComplex (T ⥤ V) c<VAR>t : T<GOAL>C.asFunctor.obj t = { X := fun i => (C.X i).obj t, d := fun i j => (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ }
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} T<VAR>C : HomologicalComplex (T ⥤ V) c<GOAL>∀ {X Y : T} (h : X ⟶ Y), C.asFunctor.map h = { f := fun i => (C.X i).map h, comm' := ⋯ }
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} T<GOAL>∀ {X Y : HomologicalComplex (T ⥤ V) c} (f : X ⟶ Y) (t : T) (i : ι), ((HomologicalComplex.complexOfFunctorsToFunctorToComplex.map f).app t).f i = (f.f i).app t
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} T<VAR>C : HomologicalComplex (T ⥤ V) c<GOAL>HomologicalComplex.complexOfFunctorsToFunctorToComplex.obj C = C.asFunctor
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp self.ι (self.hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp S.f self.p = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasCokernel S.f<VAR>CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel S).ι = CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasCokernel S.f<VAR>CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel S).Q = CategoryTheory.Limits.cokernel S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasCokernel S.f<VAR>CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel S).p = CategoryTheory.Limits.cokernel.π S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasCokernel S.f<VAR>CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel S).H = CategoryTheory.Limits.kernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : CategoryTheory.CategoryStruct.comp S.f k = 0<GOAL>CategoryTheory.CategoryStruct.comp h.p (h.descQ k hk) = k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h.p h.g' = S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<GOAL>CategoryTheory.CategoryStruct.comp h.ι h.g' = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>x : S.X₃ ⟶ A<VAR>hx : k = CategoryTheory.CategoryStruct.comp S.g x<GOAL>CategoryTheory.CategoryStruct.comp h.ι (h.descQ k ⋯) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : A ⟶ h.Q<VAR>hk : CategoryTheory.CategoryStruct.comp k h.g' = 0<GOAL>CategoryTheory.CategoryStruct.comp (h.liftH k hk) h.ι = k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>hf : S.f = 0<GOAL>CategoryTheory.IsIso h.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<VAR>hg : S.g = 0<GOAL>CategoryTheory.IsIso h.ι
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).ι = CategoryTheory.Limits.Fork.ι c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).p = CategoryTheory.CategoryStruct.id S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).Q = S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).H = c.pt
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>c : CategoryTheory.Limits.KernelFork S.g<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).g' = S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasKernel S.g<VAR>hf : S.f = 0<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf).p = CategoryTheory.CategoryStruct.id S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasKernel S.g<VAR>hf : S.f = 0<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf).ι = CategoryTheory.Limits.kernel.ι S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasKernel S.g<VAR>hf : S.f = 0<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf).Q = S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>CategoryTheory.Limits.HasKernel S.g<VAR>hf : S.f = 0<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf).H = CategoryTheory.Limits.kernel S.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).H = c.pt
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).Q = c.pt
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).p = CategoryTheory.Limits.Cofork.π c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).ι = CategoryTheory.CategoryStruct.id c.pt
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hg : S.g = 0<VAR>c : CategoryTheory.Limits.CokernelCofork S.f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).g' = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg).H = S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg).p = CategoryTheory.CategoryStruct.id S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg).ι = CategoryTheory.CategoryStruct.id S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg).Q = S.X₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg).g' = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.HasRightHomology<GOAL>Nonempty S.RightHomologyData
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<GOAL>S.HasRightHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<GOAL>h.op.H = Opposite.op h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<GOAL>h.op.π = h.ι.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<GOAL>h.op.i = h.p.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<GOAL>h.op.K = Opposite.op h.Q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.RightHomologyData<GOAL>h.op.f' = h.g'.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.RightHomologyData<GOAL>h.unop.π = h.ι.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.RightHomologyData<GOAL>h.unop.i = h.p.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.RightHomologyData<GOAL>h.unop.K = Opposite.unop h.Q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.RightHomologyData<GOAL>h.unop.H = Opposite.unop h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.RightHomologyData<GOAL>h.unop.f' = h.g'.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<GOAL>h.op.Q = Opposite.op h.K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<GOAL>h.op.ι = h.π.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<GOAL>h.op.p = h.i.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<GOAL>h.op.H = Opposite.op h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.LeftHomologyData<GOAL>h.op.g' = h.f'.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.LeftHomologyData<GOAL>h.unop.p = h.i.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.LeftHomologyData<GOAL>h.unop.Q = Opposite.unop h.K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.LeftHomologyData<GOAL>h.unop.ι = h.π.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.LeftHomologyData<GOAL>h.unop.H = Opposite.unop h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<VAR>h : S.LeftHomologyData<GOAL>h.unop.g' = h.f'.unop