ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(CategoryTheory.Limits.cokernel.π g.unop).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.cokernelUnopOp g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.eqToHom ⋯))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(CategoryTheory.cokernelUnopUnop g).inv = (CategoryTheory.Limits.kernel.lift g (CategoryTheory.Limits.cokernel.π g.unop).op ⋯).unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(CategoryTheory.cokernelUnopUnop g).hom = CategoryTheory.Limits.cokernel.desc g.unop (CategoryTheory.Limits.kernel.ι g).unop ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι g.unop).op (CategoryTheory.imageUnopOp g).hom = CategoryTheory.Limits.factorThruImage g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.imageUnopOp g).hom (CategoryTheory.Limits.image.ι g) = (CategoryTheory.Limits.factorThruImage g.unop).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage g) (CategoryTheory.imageUnopOp g).inv = (CategoryTheory.Limits.image.ι g.unop).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.imageUnopOp g).inv (CategoryTheory.Limits.factorThruImage g.unop).op = CategoryTheory.Limits.image.ι g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.EnoughInjectives C<VAR>G : C<VAR>hG : CategoryTheory.IsSeparator G<GOAL>∃ G, CategoryTheory.Injective G ∧ CategoryTheory.IsCoseparator G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Limits.HasColimits C<VAR>CategoryTheory.EnoughProjectives C<VAR>G : C<VAR>hG : CategoryTheory.IsCoseparator G<GOAL>∃ G, CategoryTheory.Projective G ∧ CategoryTheory.IsSeparator G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>CategoryTheory.Abelian.factorThruImage f ≫ CategoryTheory.Abelian.image.ι f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>CategoryTheory.Abelian.coimage.π f ≫ CategoryTheory.Abelian.factorThruCoimage f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>CategoryTheory.Abelian.coimageImageComparison f = CategoryTheory.Abelian.coimageImageComparison' f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>CategoryTheory.Abelian.coimage.π f ≫ CategoryTheory.Abelian.coimageImageComparison f ≫ CategoryTheory.Abelian.image.ι f = f
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : CategoryTheory.Epi π), ∃ x, CategoryTheory.CategoryStruct.comp π y = CategoryTheory.CategoryStruct.comp x f
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<VAR>A : C<VAR>y : A ⟶ Y<GOAL>∃ A' π, ∃ (_ : CategoryTheory.Epi π), ∃ x, CategoryTheory.CategoryStruct.comp π y = CategoryTheory.CategoryStruct.comp x f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.Exact ↔ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), CategoryTheory.CategoryStruct.comp x₂ S.g = 0 → ∃ A' π, ∃ (_ : CategoryTheory.Epi π), ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ S.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>A : C<VAR>x₂ : A ⟶ S.X₂<VAR>hx₂ : CategoryTheory.CategoryStruct.comp x₂ S.g = 0<GOAL>∃ A' π, ∃ (_ : CategoryTheory.Epi π), ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ S.f
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<VAR>A : C<VAR>γ : A ⟶ S.homology<GOAL>∃ A' π, ∃ (_ : CategoryTheory.Epi π), ∃ z, ∃ (hz : CategoryTheory.CategoryStruct.comp z S.g = 0), CategoryTheory.CategoryStruct.comp π γ = CategoryTheory.CategoryStruct.comp (S.liftCycles z hz) S.homologyπ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>g : X ⟶ Y<GOAL>CategoryTheory.Abelian.epiWithInjectiveKernel g ↔ ∃ I, ∃ (_ : CategoryTheory.Injective I), ∃ f, ∃ (w : CategoryTheory.CategoryStruct.comp f g = 0), Nonempty (CategoryTheory.ShortComplex.mk f g w).Splitting
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.Abelian.epiWithInjectiveKernel f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>G : CategoryTheory.Functor D C<VAR>G.IsRightAdjoint<GOAL>CategoryTheory.SolutionSetCondition G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u<VAR>CategoryTheory.Category.{v, u} D<VAR>G : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasLimits D<VAR>CategoryTheory.Limits.PreservesLimits G<VAR>hG : CategoryTheory.SolutionSetCondition G<GOAL>G.IsRightAdjoint
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u'} D<VAR>CategoryTheory.Limits.HasLimits D<VAR>CategoryTheory.WellPowered D<VAR>𝒢 : Set D<VAR>Small.{v, u'} ↑𝒢<VAR>h𝒢 : CategoryTheory.IsCoseparating 𝒢<VAR>G : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.PreservesLimits G<GOAL>G.IsRightAdjoint
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u'} D<VAR>CategoryTheory.Limits.HasColimits C<VAR>CategoryTheory.WellPowered Cᵒᵖ<VAR>𝒢 : Set C<VAR>Small.{v, u} ↑𝒢<VAR>h𝒢 : CategoryTheory.IsSeparating 𝒢<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.PreservesColimits F<GOAL>F.IsLeftAdjoint
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.WellPowered C<VAR>𝒢 : Set C<VAR>Small.{v, u} ↑𝒢<VAR>h𝒢 : CategoryTheory.IsCoseparating 𝒢<GOAL>CategoryTheory.Limits.HasColimits C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>CategoryTheory.WellPowered Cᵒᵖ<VAR>𝒢 : Set C<VAR>Small.{v, u} ↑𝒢<VAR>h𝒢 : CategoryTheory.IsSeparating 𝒢<GOAL>CategoryTheory.Limits.HasLimits C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type w<VAR>CategoryTheory.Category.{z, w} D<VAR>CategoryTheory.Abelian D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map (CategoryTheory.Limits.kernel.ι (α.app X)) ((CategoryTheory.Limits.kernel.ι α).app X) (CategoryTheory.Limits.PreservesKernel.iso ((CategoryTheory.evaluation C D).obj X) α).inv (CategoryTheory.CategoryStruct.id (F.obj X)) ⋯) (CategoryTheory.Limits.cokernelComparison (CategoryTheory.Limits.kernel.ι α) ((CategoryTheory.evaluation C D).obj X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type w<VAR>CategoryTheory.Category.{z, w} D<VAR>CategoryTheory.Abelian D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso ((CategoryTheory.evaluation C D).obj X) (CategoryTheory.Limits.kernel.ι α)).hom (CategoryTheory.Limits.cokernel.map ((CategoryTheory.Limits.kernel.ι α).app X) (CategoryTheory.Limits.kernel.ι (α.app X)) (CategoryTheory.Limits.kernelComparison α ((CategoryTheory.evaluation C D).obj X)) (CategoryTheory.CategoryStruct.id (F.obj X)) ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type w<VAR>CategoryTheory.Category.{z, w} D<VAR>CategoryTheory.Abelian D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(CategoryTheory.Abelian.FunctorCategory.imageObjIso α X).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map (CategoryTheory.Limits.cokernel.π (α.app X)) ((CategoryTheory.Limits.cokernel.π α).app X) (CategoryTheory.CategoryStruct.id (G.obj X)) (CategoryTheory.Limits.cokernelComparison α ((CategoryTheory.evaluation C D).obj X)) ⋯) (CategoryTheory.Limits.PreservesKernel.iso ((CategoryTheory.evaluation C D).obj X) (CategoryTheory.Limits.cokernel.π α)).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type w<VAR>CategoryTheory.Category.{z, w} D<VAR>CategoryTheory.Abelian D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(CategoryTheory.Abelian.FunctorCategory.imageObjIso α X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison (CategoryTheory.Limits.cokernel.π α) ((CategoryTheory.evaluation C D).obj X)) (CategoryTheory.Limits.kernel.map ((CategoryTheory.Limits.cokernel.π α).app X) (CategoryTheory.Limits.cokernel.π (α.app X)) (CategoryTheory.CategoryStruct.id (G.obj X)) (CategoryTheory.Limits.PreservesCokernel.iso ((CategoryTheory.evaluation C D).obj X) α).hom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type w<VAR>CategoryTheory.Category.{z, w} D<VAR>CategoryTheory.Abelian D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>X : C<GOAL>CategoryTheory.Abelian.coimageImageComparison (α.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Abelian.coimageImageComparison α).app X) (CategoryTheory.Abelian.FunctorCategory.imageObjIso α X).hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type w<VAR>CategoryTheory.Category.{z, w} D<VAR>CategoryTheory.Abelian D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(CategoryTheory.Abelian.coimageImageComparison α).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimageImageComparison (α.app X)) (CategoryTheory.Abelian.FunctorCategory.imageObjIso α X).inv)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.Exact ↔ CategoryTheory.Epi (imageToKernel' S.f S.g ⋯)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.Exact ↔ CategoryTheory.Epi (imageToKernel S.f S.g ⋯)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.Exact ↔ CategoryTheory.IsIso (imageToKernel S.f S.g ⋯)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.Exact ↔ CategoryTheory.Limits.imageSubobject S.f = CategoryTheory.Limits.kernelSubobject S.g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<VAR>cg : CategoryTheory.Limits.KernelFork S.g<VAR>hg : CategoryTheory.Limits.IsLimit cg<VAR>cf : CategoryTheory.Limits.CokernelCofork S.f<VAR>hf : CategoryTheory.Limits.IsColimit cf<GOAL>S.Exact ↔ CategoryTheory.Limits.Fork.ι cg ≫ CategoryTheory.Limits.Cofork.π cf = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.ShortComplex.mk (CategoryTheory.Limits.kernel.ι f) f ⋯).Exact
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.ShortComplex.mk f (CategoryTheory.Limits.cokernel.π f) ⋯).Exact
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.Exact ↔ (CategoryTheory.ShortComplex.mk (CategoryTheory.Abelian.image.ι S.f) S.g ⋯).Exact
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>S.Exact ↔ (CategoryTheory.ShortComplex.mk S.f (CategoryTheory.Abelian.coimage.π S.g) ⋯).Exact
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>[CategoryTheory.Mono f, CategoryTheory.Limits.kernel.ι f = 0, (CategoryTheory.ShortComplex.mk 0 f ⋯).Exact].TFAE
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>[CategoryTheory.Epi f, CategoryTheory.Limits.cokernel.π f = 0, (CategoryTheory.ShortComplex.mk f 0 ⋯).Exact].TFAE
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Abelian C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Abelian D<VAR>F : C ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>F.Faithful<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : (S.map F).Exact<GOAL>S.Exact
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Abelian A<VAR>CategoryTheory.Abelian B<VAR>L : A ⥤ B<VAR>L.PreservesZeroMorphisms<VAR>hL : ∀ (S : CategoryTheory.ShortComplex A), S.Exact → (S.map L).Exact<GOAL>L.PreservesMonomorphisms
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Abelian A<VAR>CategoryTheory.Abelian B<VAR>L : A ⥤ B<VAR>L.PreservesZeroMorphisms<VAR>hL : ∀ (S : CategoryTheory.ShortComplex A), S.Exact → (S.map L).Exact<GOAL>L.PreservesEpimorphisms
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Z : C<VAR>P : CategoryTheory.ProjectiveResolution Z<GOAL>(CategoryTheory.ShortComplex.mk (P.complex.d 1 0) (P.π.f 0) ⋯).Exact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>f : Y ⟶ Z<VAR>P : CategoryTheory.ProjectiveResolution Y<VAR>Q : CategoryTheory.ProjectiveResolution Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftFOne f P Q) (Q.complex.d 1 0) = CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (CategoryTheory.ProjectiveResolution.liftFZero f P Q)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>f : Y ⟶ Z<VAR>P : CategoryTheory.ProjectiveResolution Y<VAR>Q : CategoryTheory.ProjectiveResolution Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.lift f P Q) Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>f : Y ⟶ Z<VAR>P : CategoryTheory.ProjectiveResolution Y<VAR>Q : CategoryTheory.ProjectiveResolution Z<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.ProjectiveResolution.lift f P Q).f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>P : CategoryTheory.ProjectiveResolution Y<VAR>Q : CategoryTheory.ProjectiveResolution Z<VAR>f : P.complex ⟶ Q.complex<VAR>comm : CategoryTheory.CategoryStruct.comp f Q.π = 0<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm) (Q.complex.d 1 0) = f.f 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>P : CategoryTheory.ProjectiveResolution Y<VAR>Q : CategoryTheory.ProjectiveResolution Z<VAR>f : P.complex ⟶ Q.complex<VAR>comm : CategoryTheory.CategoryStruct.comp f Q.π = 0<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne f comm) (Q.complex.d 2 1) = f.f 1 - CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>P : CategoryTheory.ProjectiveResolution Y<VAR>Q : CategoryTheory.ProjectiveResolution Z<VAR>f : P.complex ⟶ Q.complex<VAR>n : ℕ<VAR>g : P.complex.X n ⟶ Q.complex.X (n + 1)<VAR>g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)<VAR>w : f.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g + CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc f n g g' w) (Q.complex.d (n + 3) (n + 2)) = f.f (n + 2) - CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X : C<VAR>P Q : CategoryTheory.ProjectiveResolution X<GOAL>CategoryTheory.CategoryStruct.comp (P.homotopyEquiv Q).hom Q.π = P.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X : C<VAR>P Q : CategoryTheory.ProjectiveResolution X<GOAL>CategoryTheory.CategoryStruct.comp (P.homotopyEquiv Q).inv P.π = Q.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasProjectiveResolutions C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : CategoryTheory.ProjectiveResolution X<VAR>Q : CategoryTheory.ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f<GOAL>CategoryTheory.CategoryStruct.comp P.iso.inv ((CategoryTheory.projectiveResolutions C).map f) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) Q.iso.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasProjectiveResolutions C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : CategoryTheory.ProjectiveResolution X<VAR>Q : CategoryTheory.ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.projectiveResolutions C).map f) Q.iso.hom = CategoryTheory.CategoryStruct.comp P.iso.hom ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.EnoughProjectives C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.ShortComplex.mk (CategoryTheory.Projective.d f) f ⋯).Exact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.EnoughProjectives C<VAR>Z : C<GOAL>(CategoryTheory.ProjectiveResolution.ofComplex Z).d 1 0 = CategoryTheory.Projective.d (CategoryTheory.Projective.π Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.EnoughProjectives C<VAR>Z : C<VAR>n : ℕ<GOAL>HomologicalComplex.ExactAt (CategoryTheory.ProjectiveResolution.ofComplex Z) (n + 1)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.EnoughProjectives C<VAR>Z : C<GOAL>CategoryTheory.ProjectiveResolution.of Z = CategoryTheory.ProjectiveResolution.mk (CategoryTheory.ProjectiveResolution.ofComplex Z) ⋯ (((CategoryTheory.ProjectiveResolution.ofComplex Z).toSingle₀Equiv Z).symm ⟨CategoryTheory.Projective.π Z, ⋯⟩) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>H : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasLimit H<VAR>c : CategoryTheory.Limits.Cone H<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.limit.lift H c).app k ≫ (CategoryTheory.Limits.limit.π H j).app k = (c.π.app j).app k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>H : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasColimit H<VAR>c : CategoryTheory.Limits.Cocone H<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.colimit.ι H j).app k ≫ (CategoryTheory.Limits.colimit.desc H c).app k = (c.ι.app j).app k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>F : J ⥤ K ⥤ C<VAR>c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)<VAR>j : J<VAR>k : K<GOAL>((CategoryTheory.Limits.combineCones F c).π.app j).app k = (c k).cone.π.app j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>F : J ⥤ K ⥤ C<VAR>c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)<VAR>k₁ k₂ : K<VAR>f : k₁ ⟶ k₂<GOAL>(CategoryTheory.Limits.combineCones F c).pt.map f = (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>F : J ⥤ K ⥤ C<VAR>c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)<VAR>k : K<GOAL>(CategoryTheory.Limits.combineCones F c).pt.obj k = (c k).cone.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>F : J ⥤ K ⥤ C<VAR>c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)<VAR>k : K<GOAL>(CategoryTheory.Limits.combineCocones F c).pt.obj k = (c k).cocone.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>F : J ⥤ K ⥤ C<VAR>c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)<VAR>j : J<VAR>k : K<GOAL>((CategoryTheory.Limits.combineCocones F c).ι.app j).app k = (c k).cocone.ι.app j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>F : J ⥤ K ⥤ C<VAR>c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)<VAR>k₁ k₂ : K<VAR>f : k₁ ⟶ k₂<GOAL>(CategoryTheory.Limits.combineCocones F c).pt.map f = (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := F.flip.map f ≫ (c k₂).cocone.ι }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F k).hom ≫ CategoryTheory.Limits.limit.π (F ⋙ (CategoryTheory.evaluation K C).obj k) j = (CategoryTheory.Limits.limit.π F j).app k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F k).inv ≫ (CategoryTheory.Limits.limit.π F j).app k = CategoryTheory.Limits.limit.π (F ⋙ (CategoryTheory.evaluation K C).obj k) j