ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Mono g<GOAL>(CategoryTheory.Limits.kernelCompMono f g).inv = CategoryTheory.Limits.kernel.lift (f ≫ g) (CategoryTheory.Limits.kernel.ι f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<VAR>CategoryTheory.Limits.HasKernel g<GOAL>(CategoryTheory.Limits.kernelIsIsoComp f g).hom = CategoryTheory.Limits.kernel.lift g (CategoryTheory.Limits.kernel.ι (f ≫ g) ≫ f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<VAR>CategoryTheory.Limits.HasKernel g<GOAL>(CategoryTheory.Limits.kernelIsIsoComp f g).inv = CategoryTheory.Limits.kernel.lift (f ≫ g) (CategoryTheory.Limits.kernel.ι g ≫ CategoryTheory.inv f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Limits.kernel.ι f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.kernel.ι 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>s : CategoryTheory.Limits.CokernelCofork f<GOAL>f ≫ CategoryTheory.Limits.Cofork.π s = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>s : CategoryTheory.Limits.CokernelCofork f<GOAL>s.ι.app CategoryTheory.Limits.WalkingParallelPair.zero = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y P : C<VAR>f : X ⟶ Y<VAR>π : Y ⟶ P<VAR>w : f ≫ π = 0<GOAL>CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.CokernelCofork.ofπ π w) = π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.CokernelCofork f<VAR>i : CategoryTheory.Limits.IsColimit c<VAR>W : C<VAR>g : W ⟶ X<VAR>hg : CategoryTheory.Epi g<VAR>h : W ⟶ Y<VAR>hh : h = g ≫ f<VAR>s : CategoryTheory.Limits.CokernelCofork h<GOAL>(CategoryTheory.Limits.isCokernelEpiComp i g hh).desc s = i.desc (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.Cofork.π s) ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.CokernelCofork f<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>hf : f = 0<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.Cofork.π c)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>cc : CategoryTheory.Limits.CokernelCofork f<VAR>hf : CategoryTheory.Limits.IsColimit cc<VAR>cc' : CategoryTheory.Limits.CokernelCofork f'<VAR>φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'<GOAL>CategoryTheory.Limits.Cofork.π cc ≫ CategoryTheory.Limits.CokernelCofork.mapOfIsColimit hf cc' φ = φ.right ≫ CategoryTheory.Limits.Cofork.π cc'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>cc : CategoryTheory.Limits.CokernelCofork f<VAR>cc' : CategoryTheory.Limits.CokernelCofork f'<VAR>hf : CategoryTheory.Limits.IsColimit cc<VAR>hf' : CategoryTheory.Limits.IsColimit cc'<VAR>φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'<GOAL>(CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit hf hf' φ).inv = CategoryTheory.Limits.CokernelCofork.mapOfIsColimit hf' cc φ.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>cc : CategoryTheory.Limits.CokernelCofork f<VAR>cc' : CategoryTheory.Limits.CokernelCofork f'<VAR>hf : CategoryTheory.Limits.IsColimit cc<VAR>hf' : CategoryTheory.Limits.IsColimit cc'<VAR>φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'<GOAL>(CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit hf hf' φ).hom = CategoryTheory.Limits.CokernelCofork.mapOfIsColimit hf cc' φ.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<GOAL>CategoryTheory.Limits.coequalizer.π f 0 = CategoryTheory.Limits.cokernel.π f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<GOAL>f ≫ CategoryTheory.Limits.cokernel.π f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>W : C<VAR>k : Y ⟶ W<VAR>h : f ≫ k = 0<GOAL>CategoryTheory.Limits.cokernel.π f ≫ CategoryTheory.Limits.cokernel.desc f k h = k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : f ≫ g = 0<VAR>CategoryTheory.Limits.HasCokernel f<GOAL>CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.parallelPair f 0) CategoryTheory.Limits.WalkingParallelPair.zero ≫ CategoryTheory.Limits.cokernel.desc f g h = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>W : C<VAR>h : f ≫ 0 = 0<GOAL>CategoryTheory.Limits.cokernel.desc f 0 h = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z X' Y' Z' : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<VAR>f' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasCokernel f'<VAR>g' : Y' ⟶ Z'<VAR>w' : f' ≫ g' = 0<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>r : Z ⟶ Z'<VAR>h₁ : f ≫ q = p ≫ f'<VAR>h₂ : g ≫ r = q ≫ g'<GOAL>CategoryTheory.Limits.cokernel.map f f' p q h₁ ≫ CategoryTheory.Limits.cokernel.desc f' g' w' = CategoryTheory.Limits.cokernel.desc f g w ≫ r
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasCokernel f'<VAR>p : X ≅ X'<VAR>q : Y ≅ Y'<VAR>w : f ≫ q.hom = p.hom ≫ f'<GOAL>(CategoryTheory.Limits.cokernel.mapIso f f' p q w).hom = CategoryTheory.Limits.cokernel.map f f' p.hom q.hom w
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasCokernel f'<VAR>p : X ≅ X'<VAR>q : Y ≅ Y'<VAR>w : f ≫ q.hom = p.hom ≫ f'<GOAL>(CategoryTheory.Limits.cokernel.mapIso f f' p q w).inv = CategoryTheory.Limits.cokernel.map f' f p.inv q.inv ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Mono (CategoryTheory.Limits.cokernel.π f)<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<GOAL>CategoryTheory.Limits.cokernelZeroIsoTarget.hom = CategoryTheory.Limits.cokernel.desc 0 (𝟙 Y) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<GOAL>CategoryTheory.Limits.cokernelZeroIsoTarget.inv = CategoryTheory.Limits.cokernel.π 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>h : f = f<GOAL>CategoryTheory.Limits.cokernelIsoOfEq h = CategoryTheory.Iso.refl (CategoryTheory.Limits.cokernel f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Limits.HasCokernel g<VAR>h : f = g<GOAL>CategoryTheory.Limits.cokernel.π f ≫ (CategoryTheory.Limits.cokernelIsoOfEq h).hom = CategoryTheory.Limits.cokernel.π g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Limits.HasCokernel g<VAR>h : f = g<GOAL>CategoryTheory.Limits.cokernel.π g ≫ (CategoryTheory.Limits.cokernelIsoOfEq h).inv = CategoryTheory.Limits.cokernel.π f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Limits.HasCokernel g<VAR>h : f = g<VAR>e : Y ⟶ Z<VAR>he : g ≫ e = 0<GOAL>(CategoryTheory.Limits.cokernelIsoOfEq h).hom ≫ CategoryTheory.Limits.cokernel.desc g e he = CategoryTheory.Limits.cokernel.desc f e ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Limits.HasCokernel g<VAR>h : f = g<VAR>e : Y ⟶ Z<VAR>he : f ≫ e = 0<GOAL>(CategoryTheory.Limits.cokernelIsoOfEq h).inv ≫ CategoryTheory.Limits.cokernel.desc f e he = CategoryTheory.Limits.cokernel.desc g e ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f g h : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Limits.HasCokernel g<VAR>CategoryTheory.Limits.HasCokernel h<VAR>w₁ : f = g<VAR>w₂ : g = h<GOAL>CategoryTheory.Limits.cokernelIsoOfEq w₁ ≪≫ CategoryTheory.Limits.cokernelIsoOfEq w₂ = CategoryTheory.Limits.cokernelIsoOfEq ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>w : f ≠ 0<GOAL>¬CategoryTheory.Mono (CategoryTheory.Limits.cokernel.π f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>w : f ≠ 0<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.π f) → False
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.cokernelCompIsIso f g).inv = CategoryTheory.Limits.cokernel.desc f (g ≫ CategoryTheory.Limits.cokernel.π (f ≫ g)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.IsIso g<GOAL>(CategoryTheory.Limits.cokernelCompIsIso f g).hom = CategoryTheory.Limits.cokernel.desc (f ≫ g) (CategoryTheory.inv g ≫ CategoryTheory.Limits.cokernel.π f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Epi f<VAR>CategoryTheory.Limits.HasCokernel g<GOAL>(CategoryTheory.Limits.cokernelEpiComp f g).hom = CategoryTheory.Limits.cokernel.desc (f ≫ g) (CategoryTheory.Limits.cokernel.π g) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Epi f<VAR>CategoryTheory.Limits.HasCokernel g<GOAL>(CategoryTheory.Limits.cokernelEpiComp f g).inv = CategoryTheory.Limits.cokernel.desc g (CategoryTheory.Limits.cokernel.π (f ≫ g)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.Limits.cokernel.π f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>F : CategoryTheory.Limits.MonoFactorisation f<GOAL>CategoryTheory.Limits.kernel.ι f ≫ F.e = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)<GOAL>(CategoryTheory.Limits.cokernelImageι f).hom = CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.image.ι f) (CategoryTheory.Limits.cokernel.π f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)<GOAL>(CategoryTheory.Limits.cokernelImageι f).inv = CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.image.ι f)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.π 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Limits.HasKernel (G.map f)<GOAL>CategoryTheory.Limits.kernelComparison f G ≫ CategoryTheory.Limits.kernel.ι (G.map f) = G.map (CategoryTheory.Limits.kernel.ι f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Limits.HasKernel (G.map f)<VAR>Z : C<VAR>h : Z ⟶ X<VAR>w : h ≫ f = 0<GOAL>G.map (CategoryTheory.Limits.kernel.lift f h w) ≫ CategoryTheory.Limits.kernelComparison f G = CategoryTheory.Limits.kernel.lift (G.map f) (G.map h) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>CategoryTheory.Limits.HasKernel f<VAR>CategoryTheory.Limits.HasKernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasKernel g<VAR>CategoryTheory.Limits.HasKernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>CategoryTheory.Limits.kernelComparison f G ≫ CategoryTheory.Limits.kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ = G.map (CategoryTheory.Limits.kernel.map f g p q hpq) ≫ CategoryTheory.Limits.kernelComparison g G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Limits.HasCokernel (G.map f)<GOAL>CategoryTheory.Limits.cokernel.π (G.map f) ≫ CategoryTheory.Limits.cokernelComparison f G = G.map (CategoryTheory.Limits.cokernel.π f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Limits.HasCokernel (G.map f)<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = 0<GOAL>CategoryTheory.Limits.cokernelComparison f G ≫ G.map (CategoryTheory.Limits.cokernel.desc f h w) = CategoryTheory.Limits.cokernel.desc (G.map f) (G.map h) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>CategoryTheory.Limits.HasCokernel f<VAR>CategoryTheory.Limits.HasCokernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasCokernel g<VAR>CategoryTheory.Limits.HasCokernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ ≫ CategoryTheory.Limits.cokernelComparison g G = CategoryTheory.Limits.cokernelComparison f G ≫ G.map (CategoryTheory.Limits.cokernel.map f g p q hpq)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>self : CategoryTheory.Limits.HasKernels C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Limits.HasKernel f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>self : CategoryTheory.Limits.HasCokernels C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Limits.HasCokernel f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>a : (CategoryTheory.Limits.Types.constPUnitFunctor C).obj X<GOAL>(CategoryTheory.Limits.Types.pUnitCocone C).ι.app X a = id a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.Limits.Types.pUnitCocone C).pt = PUnit.{w + 1}
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>c d : (j : C) × F.obj j<VAR>h : EqvGen (CategoryTheory.Limits.Types.Quot.Rel F) c d<GOAL>CategoryTheory.Zigzag c.fst d.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.Types.constPUnitFunctor C)<GOAL>CategoryTheory.IsConnected C ↔ Nonempty (CategoryTheory.Limits.colimit (CategoryTheory.Limits.Types.constPUnitFunctor C) ≅ PUnit.{w + 1})
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.IsConnected C ↔ Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.pUnitCocone C))
<VAR>C : Type u<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>F.Final<GOAL>CategoryTheory.IsConnected C ↔ CategoryTheory.IsConnected D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P : C<VAR>hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj (Opposite.op P))<GOAL>CategoryTheory.Projective P
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J × K ⥤ C<VAR>j : J<VAR>k k' : K<VAR>f : k ⟶ k'<GOAL>F.map (𝟙 j, f) = ((CategoryTheory.curry.obj F).obj j).map f
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J × K ⥤ C<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>k : K<GOAL>F.map (f, 𝟙 k) = ((CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ F)).obj k).map f
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J × K ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>j : J<VAR>k : K<GOAL>CategoryTheory.Limits.colimit.ι (CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ F) ⋙ CategoryTheory.Limits.lim) k ≫ CategoryTheory.Limits.colimitLimitToLimitColimit F ≫ CategoryTheory.Limits.limit.π (CategoryTheory.curry.obj F ⋙ CategoryTheory.Limits.colim) j = CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ F)).obj k) j ≫ CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj F).obj j) k
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>Small.{v, u₁} J<VAR>Small.{v, u₂} K<VAR>F : J × K ⥤ Type v<VAR>j : J<VAR>k : K<VAR>f : (CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ F) ⋙ CategoryTheory.Limits.lim).obj k<GOAL>CategoryTheory.Limits.limit.π (CategoryTheory.curry.obj F ⋙ CategoryTheory.Limits.colim) j (CategoryTheory.Limits.colimitLimitToLimitColimit F (CategoryTheory.Limits.colimit.ι (CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ F) ⋙ CategoryTheory.Limits.lim) k f)) = CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj F).obj j) k (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (CategoryTheory.Prod.swap K J ⋙ F)).obj k) j f)
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>G : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasLimit G<GOAL>(CategoryTheory.Limits.colimitLimitToLimitColimitCone G).hom = CategoryTheory.Limits.colim.map (CategoryTheory.Limits.limitIsoSwapCompLim G).hom ≫ CategoryTheory.Limits.colimitLimitToLimitColimit (CategoryTheory.uncurry.obj G) ≫ CategoryTheory.Limits.lim.map (CategoryTheory.whiskerRight (CategoryTheory.currying.unitIso.app G).inv CategoryTheory.Limits.colim)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>self : CategoryTheory.Limits.MonoCoprod C<VAR>A B : C<VAR>c : CategoryTheory.Limits.BinaryCofan A B<GOAL>CategoryTheory.Limits.IsColimit c → CategoryTheory.Mono c.inl
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B : C<VAR>CategoryTheory.Limits.MonoCoprod C<VAR>c : CategoryTheory.Limits.BinaryCofan A B<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.Mono c.inr
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B : C<VAR>c₁ c₂ : CategoryTheory.Limits.BinaryCofan A B<VAR>hc₁ : CategoryTheory.Limits.IsColimit c₁<VAR>hc₂ : CategoryTheory.Limits.IsColimit c₂<GOAL>CategoryTheory.Mono c₁.inl ↔ CategoryTheory.Mono c₂.inl
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>h : ∀ (A B : C), ∃ c x, CategoryTheory.Mono c.inl<GOAL>CategoryTheory.Limits.MonoCoprod C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>X : I₁ ⊕ I₂ → C<VAR>c : CategoryTheory.Limits.Cofan X<VAR>c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)<VAR>c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>hc₁ : CategoryTheory.Limits.IsColimit c₁<VAR>hc₂ : CategoryTheory.Limits.IsColimit c₂<VAR>CategoryTheory.Limits.MonoCoprod C<GOAL>CategoryTheory.Mono (CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>X : I₁ ⊕ I₂ → C<VAR>c : CategoryTheory.Limits.Cofan X<VAR>c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)<VAR>c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>hc₁ : CategoryTheory.Limits.IsColimit c₁<VAR>hc₂ : CategoryTheory.Limits.IsColimit c₂<VAR>CategoryTheory.Limits.MonoCoprod C<GOAL>CategoryTheory.Mono (CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>X : I₁ ⊕ I₂ → C<VAR>c : CategoryTheory.Limits.Cofan X<VAR>c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)<VAR>c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>hc₁ : CategoryTheory.Limits.IsColimit c₁<VAR>hc₂ : CategoryTheory.Limits.IsColimit c₂<VAR>CategoryTheory.Limits.MonoCoprod C<VAR>inl : c₁.pt ⟶ c.pt<VAR>hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)<GOAL>CategoryTheory.Mono inl