ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w₁<VAR>CategoryTheory.Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} E<VAR>F : CategoryTheory.Functor D E<VAR>∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D<VAR>∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E<VAR>(X : C) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>hP : CategoryTheory.Presheaf.IsSheaf J ((J.plusObj P).comp F)<GOAL>(J.plusCompIso F P).inv = J.plusLift (CategoryTheory.whiskerRight (J.toPlus P) F) hP
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>o : CategoryTheory.HomOrthogonal s<VAR>i j : ι<VAR>w : i ≠ j<VAR>f : s i ⟶ s j<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>o : CategoryTheory.HomOrthogonal s<VAR>α β : Type<VAR>Finite α<VAR>Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)<VAR>i : ι<VAR>j : ↑(g ⁻¹' {i})<VAR>k : ↑(f ⁻¹' {i})<GOAL>o.matrixDecomposition z i j k = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.components z ↑k ↑j) (CategoryTheory.eqToHom ⋯))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>o : CategoryTheory.HomOrthogonal s<VAR>α β : Type<VAR>Finite α<VAR>Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))<GOAL>o.matrixDecomposition.symm z = CategoryTheory.Limits.biproduct.matrix fun j k => if h : f j = g k then CategoryTheory.CategoryStruct.comp (z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩) (CategoryTheory.eqToHom ⋯) else 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>o : CategoryTheory.HomOrthogonal s<VAR>α β : Type<VAR>Finite α<VAR>Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)<VAR>i : ι<VAR>j : ↑(g ⁻¹' {i})<VAR>k : ↑(f ⁻¹' {i})<GOAL>o.matrixDecompositionAddEquiv z i j k = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.components z ↑k ↑j) (CategoryTheory.eqToHom ⋯))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>o : CategoryTheory.HomOrthogonal s<VAR>α β : Type<VAR>Finite α<VAR>Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))<GOAL>o.matrixDecompositionAddEquiv.symm z = CategoryTheory.Limits.biproduct.matrix fun j k => if h : f j = g k then CategoryTheory.CategoryStruct.comp (z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩) (CategoryTheory.eqToHom ⋯) else 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>o : CategoryTheory.HomOrthogonal s<VAR>α : Type<VAR>Finite α<VAR>f : α → ι<VAR>i : ι<GOAL>o.matrixDecomposition (CategoryTheory.CategoryStruct.id (⨁ fun a => s (f a))) i = 1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>o : CategoryTheory.HomOrthogonal s<VAR>α β γ : Type<VAR>Finite α<VAR>Fintype β<VAR>Finite γ<VAR>f : α → ι<VAR>g : β → ι<VAR>h : γ → ι<VAR>z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)<VAR>w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)<VAR>i : ι<GOAL>o.matrixDecomposition (CategoryTheory.CategoryStruct.comp z w) i = o.matrixDecomposition w i * o.matrixDecomposition z i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>R : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Linear R C<VAR>o : CategoryTheory.HomOrthogonal s<VAR>α β : Type<VAR>Finite α<VAR>Finite β<VAR>f : α → ι<VAR>g : β → ι<GOAL>∀ (a : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))), o.matrixDecompositionLinearEquiv.symm a = o.matrixDecompositionAddEquiv.invFun a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>R : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Linear R C<VAR>o : CategoryTheory.HomOrthogonal s<VAR>α β : Type<VAR>Finite α<VAR>Finite β<VAR>f : α → ι<VAR>g : β → ι<GOAL>∀ (a : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) (i : ι), o.matrixDecompositionLinearEquiv a i = o.matrixDecompositionAddEquiv.toFun a i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>∀ (i : ι), InvariantBasisNumber (CategoryTheory.End (s i))<VAR>o : CategoryTheory.HomOrthogonal s<VAR>α β : Type<VAR>Finite α<VAR>Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)<GOAL>∃ e, ∀ (a : α), g (e a) = f a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>𝒢 : Set C<GOAL>CategoryTheory.IsSeparating 𝒢 ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>𝒢 : Set C<GOAL>CategoryTheory.IsCoseparating 𝒢 ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>G : C<GOAL>CategoryTheory.IsSeparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>G : C<GOAL>CategoryTheory.IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>G : C<GOAL>CategoryTheory.IsSeparator G ↔ (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op G)).Faithful
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>G : C<GOAL>CategoryTheory.IsSeparator G ↔ (CategoryTheory.preadditiveCoyonedaObj (Opposite.op G)).Faithful
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>G : C<GOAL>CategoryTheory.IsCoseparator G ↔ (CategoryTheory.preadditiveYoneda.obj G).Faithful
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>G : C<GOAL>CategoryTheory.IsCoseparator G ↔ (CategoryTheory.preadditiveYonedaObj G).Faithful
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f f' : P ⟶ Q<VAR>g : Q ⟶ R<GOAL>(f + f') ≫ g = f ≫ g + f' ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g g' : Q ⟶ R<GOAL>f ≫ (g + g') = f ≫ g + f ≫ g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f f' : P ⟶ Q<VAR>g : Q ⟶ R<GOAL>(f - f') ≫ g = f ≫ g - f' ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g g' : Q ⟶ R<GOAL>f ≫ (g - g') = f ≫ g - f ≫ g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<GOAL>(-f) ≫ g = -f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<GOAL>f ≫ (-g) = -f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<GOAL>(-f) ≫ (-g) = f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>n : ℕ<GOAL>(n • f) ≫ g = n • f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>n : ℕ<GOAL>f ≫ (n • g) = n • f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>n : ℤ<GOAL>(n • f) ≫ g = n • f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>n : ℤ<GOAL>f ≫ (n • g) = n • f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>J : Type u_1<VAR>s : Finset J<VAR>f : P ⟶ Q<VAR>g : J → (Q ⟶ R)<GOAL>f ≫ ∑ j ∈ s, g j = ∑ j ∈ s, f ≫ g j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>J : Type u_1<VAR>s : Finset J<VAR>f : J → (P ⟶ Q)<VAR>g : Q ⟶ R<GOAL>(∑ j ∈ s, f j) ≫ g = ∑ j ∈ s, f j ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>Q R : C<VAR>f : Q ⟶ R<VAR>h : ∀ {P : C} (g : P ⟶ Q), g ≫ f = 0 → g = 0<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>Q R : C<VAR>f : Q ⟶ R<GOAL>CategoryTheory.Mono f ↔ ∀ (P : C) (g : P ⟶ Q), g ≫ f = 0 → g = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f 0)<VAR>w : CategoryTheory.Limits.kernel.ι f = 0<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.KernelFork f<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>h : CategoryTheory.Limits.IsZero c.pt<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>h : CategoryTheory.Limits.IsZero (CategoryTheory.Limits.kernel f)<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : ∀ {R : C} (g : Q ⟶ R), f ≫ g = 0 → g = 0<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>CategoryTheory.Epi f ↔ ∀ (R : C) (g : Q ⟶ R), f ≫ g = 0 → g = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f 0)<VAR>w : CategoryTheory.Limits.cokernel.π f = 0<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.CokernelCofork f<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>h : CategoryTheory.Limits.IsZero c.pt<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel f<VAR>h : CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel f)<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>CategoryTheory.IsIso f<GOAL>f ≫ g = 0 ↔ g = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>CategoryTheory.IsIso g<GOAL>f ≫ g = 0 ↔ f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f 0)<VAR>w : CategoryTheory.Limits.kernel f ≅ 0<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f 0)<VAR>w : CategoryTheory.Limits.cokernel f ≅ 0<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.KernelFork (f - g)<GOAL>(CategoryTheory.Preadditive.forkOfKernelFork c).pt = c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.KernelFork (f - g)<GOAL>(CategoryTheory.Preadditive.forkOfKernelFork c).ι = CategoryTheory.Limits.Fork.ι c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.Fork f g<GOAL>CategoryTheory.Limits.Fork.ι (CategoryTheory.Preadditive.kernelForkOfFork c) = c.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>P : C<VAR>ι : P ⟶ X<VAR>w : ι ≫ f = ι ≫ g<GOAL>CategoryTheory.Preadditive.kernelForkOfFork (CategoryTheory.Limits.Fork.ofι ι w) = CategoryTheory.Limits.KernelFork.ofι ι ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.KernelFork (f - g)<VAR>i : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Fork f g<GOAL>(CategoryTheory.Preadditive.isLimitForkOfKernelFork i).lift s = i.lift (CategoryTheory.Preadditive.kernelForkOfFork s)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel (f - g)<GOAL>CategoryTheory.Limits.HasEqualizer f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<GOAL>CategoryTheory.Limits.HasKernel (f - g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.CokernelCofork (f - g)<GOAL>(CategoryTheory.Preadditive.coforkOfCokernelCofork c).pt = c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.CokernelCofork (f - g)<GOAL>(CategoryTheory.Preadditive.coforkOfCokernelCofork c).π = CategoryTheory.Limits.Cofork.π c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.Cofork f g<GOAL>CategoryTheory.Limits.Cofork.π (CategoryTheory.Preadditive.cokernelCoforkOfCofork c) = c.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>P : C<VAR>π : Y ⟶ P<VAR>w : f ≫ π = g ≫ π<GOAL>CategoryTheory.Preadditive.cokernelCoforkOfCofork (CategoryTheory.Limits.Cofork.ofπ π w) = CategoryTheory.Limits.CokernelCofork.ofπ π ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CategoryTheory.Limits.CokernelCofork (f - g)<VAR>i : CategoryTheory.Limits.IsColimit c<VAR>s : CategoryTheory.Limits.Cofork f g<GOAL>(CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork i).desc s = i.desc (CategoryTheory.Preadditive.cokernelCoforkOfCofork s)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCokernel (f - g)<GOAL>CategoryTheory.Limits.HasCoequalizer f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasCoequalizer f g<GOAL>CategoryTheory.Limits.HasCokernel (f - g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasKernels C<GOAL>CategoryTheory.Limits.HasEqualizers C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasCokernels C<GOAL>CategoryTheory.Limits.HasCoequalizers C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>a : ℤˣ<VAR>e : X ≅ Y<GOAL>(a • e).hom = a • e.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>a : ℤˣ<VAR>e : X ≅ Y<GOAL>(a • e).inv = a⁻¹ • e.inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>e : X ≅ Y<GOAL>(-e).hom = -e.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : C<VAR>e : X ≅ Y<GOAL>(-e).inv = -e.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : C<VAR>self : CategoryTheory.Injective J<VAR>X Y : C<VAR>g : X ⟶ J<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>∃ h, f ≫ h = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>h : CategoryTheory.Limits.IsZero X<GOAL>CategoryTheory.Injective X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>self : CategoryTheory.InjectivePresentation X<GOAL>CategoryTheory.Mono self.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>self : CategoryTheory.InjectivePresentation X<GOAL>CategoryTheory.Injective self.J
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : CategoryTheory.EnoughInjectives C<VAR>X : C<GOAL>Nonempty (CategoryTheory.InjectivePresentation X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J X Y : C<VAR>CategoryTheory.Injective J<VAR>g : X ⟶ J<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>f ≫ CategoryTheory.Injective.factorThru g f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P Q : C<VAR>i : P ≅ Q<VAR>hP : CategoryTheory.Injective P<GOAL>CategoryTheory.Injective Q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P Q : C<VAR>i : P ≅ Q<GOAL>CategoryTheory.Injective P ↔ CategoryTheory.Injective Q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : C<GOAL>CategoryTheory.Injective J ↔ CategoryTheory.Projective (Opposite.op J)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : C<GOAL>CategoryTheory.Projective P ↔ CategoryTheory.Injective (Opposite.op P)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : C<GOAL>CategoryTheory.Injective J ↔ (CategoryTheory.yoneda.obj J).PreservesEpimorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>L.PreservesMonomorphisms<VAR>adj : L ⊣ R<VAR>J : D<VAR>CategoryTheory.Injective J<GOAL>CategoryTheory.Injective (R.obj J)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.EnoughInjectives Cᵒᵖ<GOAL>CategoryTheory.EnoughProjectives C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.EnoughProjectives Cᵒᵖ<GOAL>CategoryTheory.EnoughInjectives C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>F.PreservesMonomorphisms<VAR>I : D<VAR>hI : CategoryTheory.Injective I<GOAL>CategoryTheory.Injective (G.obj I)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>G.Full<VAR>G.Faithful<VAR>I : D<VAR>hI : CategoryTheory.Injective (G.obj I)<GOAL>CategoryTheory.Injective I
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>adj : L ⊣ R<VAR>L.PreservesMonomorphisms<VAR>L.ReflectsMonomorphisms<VAR>CategoryTheory.EnoughInjectives D<GOAL>CategoryTheory.EnoughInjectives C
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ⥤ D<VAR>e.IsEquivalence<VAR>CategoryTheory.EnoughInjectives D<GOAL>CategoryTheory.EnoughInjectives C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : C ≌ D<VAR>P : C<GOAL>CategoryTheory.Injective (F.functor.obj P) ↔ CategoryTheory.Injective P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : C ≌ D<GOAL>CategoryTheory.EnoughInjectives C ↔ CategoryTheory.EnoughInjectives D
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>X : C<VAR>S T : CategoryTheory.Presieve X<GOAL>S.FactorsThruAlong T (CategoryTheory.CategoryStruct.id X) ↔ S.FactorsThru T
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>X : C<VAR>S T : CategoryTheory.Presieve X<VAR>h : S ≤ T<GOAL>S.FactorsThru T
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>X : C<VAR>S : CategoryTheory.Presieve X<VAR>T : CategoryTheory.Sieve X<VAR>h : S.FactorsThru T.arrows<GOAL>S ≤ T.arrows
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>X : C<VAR>S : CategoryTheory.Presieve X<GOAL>S.FactorsThru ⊤
<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_2, u_3} C<VAR>X : C<VAR>S T : CategoryTheory.Presieve X<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type u_1)<VAR>H : S.FactorsThru T<VAR>hS : CategoryTheory.Presieve.IsSheafFor P S<VAR>h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, CategoryTheory.Presieve.IsSeparatedFor P R ∧ R.FactorsThruAlong S f<GOAL>CategoryTheory.Presieve.IsSheafFor P T
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>self : CategoryTheory.Coverage C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>S : CategoryTheory.Presieve X<GOAL>S ∈ self.covering X → ∃ T ∈ self.covering Y, T.FactorsThruAlong S f
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>X : C<VAR>S : CategoryTheory.Presieve X<VAR>J : CategoryTheory.GrothendieckTopology C<GOAL>S ∈ (CategoryTheory.Coverage.ofGrothendieck C J).covering X ↔ CategoryTheory.Sieve.generate S ∈ J.sieves X
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>X Y : C<VAR>S T : CategoryTheory.Sieve X<VAR>h : S ≤ T<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<GOAL>CategoryTheory.Sieve.pullback f T = ⊤
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>K : CategoryTheory.Coverage C<VAR>X : C<VAR>S T : CategoryTheory.Sieve X<VAR>h : S ≤ T<VAR>hS : K.Saturate X S<GOAL>K.Saturate X T
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>K : CategoryTheory.Coverage C<GOAL>CategoryTheory.Coverage.toGrothendieck C K = sInf {J | K ≤ CategoryTheory.Coverage.ofGrothendieck C J}
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>x y : CategoryTheory.Coverage C<VAR>B : C<GOAL>(x ⊔ y).covering B = x.covering B ∪ y.covering B
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>K : CategoryTheory.Coverage C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>R : CategoryTheory.Presieve X<VAR>h : R ≤ S.arrows<VAR>hR : R ∈ K.covering X<GOAL>S ∈ (CategoryTheory.Coverage.toGrothendieck C K).sieves X
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>K : CategoryTheory.Coverage C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type u_1)<GOAL>CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C K) P ↔ ∀ {X : C}, ∀ R ∈ K.covering X, CategoryTheory.Presieve.IsSheafFor P R