ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X Y Z : Pointed<VAR>f : X.Hom Y<VAR>g : Y.Hom Z<GOAL>∀ (a : X.X), (f.comp g).toFun a = (g.toFun ∘ f.toFun) a
<VAR>X : Pointed<GOAL>(𝟙 X).toFun = id
<VAR>X Y Z : Pointed<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).toFun = g.toFun ∘ f.toFun
<VAR>α β : Pointed<VAR>e : α.X ≃ β.X<VAR>he : e α.point = β.point<VAR>a : α.X<GOAL>(Pointed.Iso.mk e he).hom.toFun a = e a
<VAR>α β : Pointed<VAR>e : α.X ≃ β.X<VAR>he : e α.point = β.point<VAR>a : β.X<GOAL>(Pointed.Iso.mk e he).inv.toFun a = e.symm a
<VAR>X : Type u<GOAL>(typeToPointed.obj X).X = Option X
<VAR>X : Type u<GOAL>(typeToPointed.obj X).point = none
<GOAL>∀ {X Y : Type u} (f : X ⟶ Y) (a : Option X), (typeToPointed.map f).toFun a = Option.map f a
<VAR>α β : PartialFun<VAR>e : α ≃ β<VAR>x : β<GOAL>(PartialFun.Iso.mk e).inv x = ↑(some (e.symm x))
<VAR>α β : PartialFun<VAR>e : α ≃ β<VAR>x : α<GOAL>(PartialFun.Iso.mk e).hom x = ↑(some (e x))
<GOAL>∀ {X Y : Pointed} (f : X ⟶ Y) (a : { x // x ≠ X.point }), pointedToPartialFun.map f a = (PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val) a
<VAR>X : Pointed<GOAL>pointedToPartialFun.obj X = { x // x ≠ X.point }
<VAR>X : PartialFun<GOAL>partialFunToPointed.obj X = { X := Option X, point := none }
<GOAL>∀ {X Y : PartialFun} (f : X ⟶ Y), partialFunToPointed.map f = { toFun := Option.elim' none fun a => (f a).toOption, map_point := ⋯ }
<GOAL>∀ {X Y : Pointed} (f : X ⟶ Y) (a : { x // x ≠ X.point }) (property : f.toFun ↑a ≠ Y.point), ↑((partialFunEquivPointed.inverse.map f a).get property) = f.toFun ↑a
<VAR>X : PartialFun<GOAL>(partialFunEquivPointed.functor.obj X).X = Option X
<GOAL>∀ {X Y : PartialFun} (f : X ⟶ Y) (a : Option X), (partialFunEquivPointed.functor.map f).toFun a = Option.elim' none (fun a => (f a).toOption) a
<VAR>X : PartialFun<GOAL>(partialFunEquivPointed.functor.obj X).point = none
<GOAL>∀ {X Y : Pointed} (f : X ⟶ Y) (a : { x // x ≠ X.point }), (partialFunEquivPointed.inverse.map f a).Dom = ¬f.toFun ↑a = Y.point
<VAR>X : PartialFun<GOAL>partialFunEquivPointed.unitIso.hom.app X = (PartialFun.Iso.mk { toFun := fun a => ⟨some a, ⋯⟩, invFun := fun a => (↑a).get ⋯, left_inv := ⋯, right_inv := ⋯ }).hom ≫ pointedToPartialFun.map (Pointed.Iso.mk (Equiv.optionSubtypeNe none) ⋯).inv ≫ pointedToPartialFun.map { toFun := Option.elim' none fun a => ↑a, map_point := ⋯ }
<VAR>X : Pointed<VAR>a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X<GOAL>(partialFunEquivPointed.counitIso.hom.app X).toFun a = Option.casesOn' a X.point Subtype.val
<VAR>X : Pointed<GOAL>partialFunEquivPointed.inverse.obj X = { x // ¬x = X.point }
<VAR>X : PartialFun<GOAL>partialFunEquivPointed.unitIso.inv.app X = pointedToPartialFun.map { toFun := Option.elim' none fun a => some ⟨some a, ⋯⟩, map_point := ⋯ } ≫ pointedToPartialFun.map (Pointed.Iso.mk (Equiv.optionSubtypeNe none) ⋯).hom ≫ (PartialFun.Iso.mk { toFun := fun a => ⟨some a, ⋯⟩, invFun := fun a => (↑a).get ⋯, left_inv := ⋯, right_inv := ⋯ }).inv
<VAR>X : Pointed<VAR>a : ((𝟭 Pointed).obj X).X<GOAL>(partialFunEquivPointed.counitIso.inv.app X).toFun a = if h : a = X.point then none else some ⟨a, h⟩
<VAR>X : Type u_3<VAR>a : ((typeToPartialFun ⋙ partialFunToPointed).obj X).X<GOAL>(typeToPartialFunIsoPartialFunToPointed.hom.app X).toFun a = a
<VAR>X : Type u_3<VAR>a : (typeToPointed.obj X).X<GOAL>(typeToPartialFunIsoPartialFunToPointed.inv.app X).toFun a = a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.Factorisation f<GOAL>CategoryTheory.CategoryStruct.comp self.ι self.π = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>d e : CategoryTheory.Factorisation f<VAR>self : d.Hom e<GOAL>CategoryTheory.CategoryStruct.comp d.ι self.h = e.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>d e : CategoryTheory.Factorisation f<VAR>self : d.Hom e<GOAL>CategoryTheory.CategoryStruct.comp self.h e.π = d.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>d : CategoryTheory.Factorisation f<GOAL>(CategoryTheory.Factorisation.Hom.id d).h = CategoryTheory.CategoryStruct.id d.mid
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>d₁ d₂ d₃ : CategoryTheory.Factorisation f<GOAL>∀ (f_1 : d₁.Hom d₂) (g : d₂.Hom d₃), (f_1.comp g).h = CategoryTheory.CategoryStruct.comp f_1.h g.h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Factorisation.initial.ι = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Factorisation.initial.π = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Factorisation.initial.mid = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>d : CategoryTheory.Factorisation f<GOAL>d.initialHom.h = d.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Factorisation.terminal.mid = Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Factorisation.terminal.ι = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Factorisation.terminal.π = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>d : CategoryTheory.Factorisation f<GOAL>d.terminalHom.h = d.π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>∀ {X_1 Y_1 : CategoryTheory.Factorisation f} (f_1 : X_1 ⟶ Y_1), CategoryTheory.Factorisation.forget.map f_1 = f_1.h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>self : CategoryTheory.Factorisation f<GOAL>CategoryTheory.Factorisation.forget.obj self = self.mid
<VAR>C : CategoryTheory.Cat<VAR>X Y : ↑C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.CategoryStruct.id C).map f = f
<VAR>C D E : CategoryTheory.Cat<VAR>F : C ⟶ D<VAR>G : D ⟶ E<VAR>X : ↑C<GOAL>(CategoryTheory.CategoryStruct.comp F G).obj X = G.obj (F.obj X)
<VAR>C D E : CategoryTheory.Cat<VAR>F : C ⟶ D<VAR>G : D ⟶ E<VAR>X Y : ↑C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.CategoryStruct.comp F G).map f = G.map (F.map f)
<VAR>C D E : CategoryTheory.Cat<VAR>F : C ⟶ D<VAR>G H : D ⟶ E<VAR>η : G ⟶ H<VAR>X : ↑C<GOAL>(CategoryTheory.Bicategory.whiskerLeft F η).app X = η.app (F.obj X)
<VAR>C D E : CategoryTheory.Cat<VAR>F G : C ⟶ D<VAR>H : D ⟶ E<VAR>η : F ⟶ G<VAR>X : ↑C<GOAL>(CategoryTheory.Bicategory.whiskerRight η H).app X = H.map (η.app X)
<VAR>B C : CategoryTheory.Cat<VAR>F : B ⟶ C<VAR>X : ↑B<GOAL>(CategoryTheory.Bicategory.leftUnitor F).hom.app X = CategoryTheory.eqToHom ⋯
<VAR>B C : CategoryTheory.Cat<VAR>F : B ⟶ C<VAR>X : ↑B<GOAL>(CategoryTheory.Bicategory.leftUnitor F).inv.app X = CategoryTheory.eqToHom ⋯
<VAR>B C : CategoryTheory.Cat<VAR>F : B ⟶ C<VAR>X : ↑B<GOAL>(CategoryTheory.Bicategory.rightUnitor F).hom.app X = CategoryTheory.eqToHom ⋯
<VAR>B C : CategoryTheory.Cat<VAR>F : B ⟶ C<VAR>X : ↑B<GOAL>(CategoryTheory.Bicategory.rightUnitor F).inv.app X = CategoryTheory.eqToHom ⋯
<VAR>B C D E : CategoryTheory.Cat<VAR>F : B ⟶ C<VAR>G : C ⟶ D<VAR>H : D ⟶ E<VAR>X : ↑B<GOAL>(CategoryTheory.Bicategory.associator F G H).hom.app X = CategoryTheory.eqToHom ⋯
<VAR>B C D E : CategoryTheory.Cat<VAR>F : B ⟶ C<VAR>G : C ⟶ D<VAR>H : D ⟶ E<VAR>X : ↑B<GOAL>(CategoryTheory.Bicategory.associator F G H).inv.app X = CategoryTheory.eqToHom ⋯
<VAR>X : Type u<GOAL>CategoryTheory.typeToCat.obj X = CategoryTheory.Cat.of (CategoryTheory.Discrete X)
<VAR>X Y : Type u<VAR>f : X ⟶ Y<GOAL>CategoryTheory.typeToCat.map f = id (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ f))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.IsFilteredOrEmpty C<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>∃ Z h, CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.IsFilteredOrEmpty C<VAR>X Y : C<GOAL>∃ Z x x, True
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.IsFiltered C<GOAL>Nonempty C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>j j' : C<VAR>f f' : j ⟶ j'<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeqHom f f') = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.IsFiltered.coeqHom f f')
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>L : CategoryTheory.Functor D C<VAR>R : CategoryTheory.Functor C D<VAR>h : L ⊣ R<GOAL>CategoryTheory.IsFilteredOrEmpty D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>R : CategoryTheory.Functor C D<VAR>R.IsRightAdjoint<GOAL>CategoryTheory.IsFilteredOrEmpty D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>h : C ≌ D<GOAL>CategoryTheory.IsFilteredOrEmpty D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFiltered C<VAR>O : Finset C<GOAL>∃ S, ∀ {X : C}, X ∈ O → Nonempty (X ⟶ S)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFiltered C<VAR>O : Finset C<VAR>H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))<GOAL>∃ S T, ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → CategoryTheory.CategoryStruct.comp f (T mY) = T mX
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFiltered C<VAR>O : Finset C<VAR>H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))<VAR>X Y : C<VAR>mX : X ∈ O<VAR>mY : Y ∈ O<VAR>f : X ⟶ Y<VAR>mf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.toSup O H mY) = CategoryTheory.IsFiltered.toSup O H mX
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFiltered C<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.FinCategory J<VAR>F : CategoryTheory.Functor J C<GOAL>Nonempty (CategoryTheory.Limits.Cocone F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFiltered C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>L : CategoryTheory.Functor D C<VAR>R : CategoryTheory.Functor C D<VAR>h : L ⊣ R<GOAL>CategoryTheory.IsFiltered D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFiltered C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>R : CategoryTheory.Functor C D<VAR>R.IsRightAdjoint<GOAL>CategoryTheory.IsFiltered D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFiltered C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>h : C ≌ D<GOAL>CategoryTheory.IsFiltered D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>h : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cocone F)<GOAL>CategoryTheory.IsFiltered C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteColimits C<GOAL>CategoryTheory.IsFiltered C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>h : CategoryTheory.Limits.IsTerminal X<GOAL>CategoryTheory.IsFiltered C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.IsFiltered C ↔ ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cocone F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>j₁ j₂ : C<VAR>f g h : j₁ ⟶ j₂<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeq₃Hom f g h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.IsFiltered.coeq₃Hom f g h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>j₁ j₂ : C<VAR>f g h : j₁ ⟶ j₂<GOAL>CategoryTheory.CategoryStruct.comp g (CategoryTheory.IsFiltered.coeq₃Hom f g h) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.IsFiltered.coeq₃Hom f g h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>j₁ j₂ : C<VAR>f g h : j₁ ⟶ j₂<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeq₃Hom f g h) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.IsFiltered.coeq₃Hom f g h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>i j j' : C<VAR>f : i ⟶ j<VAR>f' : i ⟶ j'<GOAL>∃ k g g', CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>j₁ j₂ k₁ k₂ : C<VAR>f₁ : j₁ ⟶ k₁<VAR>g₁ : j₁ ⟶ k₂<VAR>f₂ : j₂ ⟶ k₁<VAR>g₂ : j₂ ⟶ k₂<GOAL>∃ s α β, CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧ CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp g₂ β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>j₁ j₂ j₃ k₁ k₂ l : C<VAR>f₁ : j₁ ⟶ k₁<VAR>f₂ : j₂ ⟶ k₁<VAR>f₃ : j₂ ⟶ k₂<VAR>f₄ : j₃ ⟶ k₂<VAR>g₁ : j₁ ⟶ l<VAR>g₂ : j₃ ⟶ l<GOAL>∃ s α β γ, CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧ CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp f₃ γ ∧ CategoryTheory.CategoryStruct.comp f₄ γ = CategoryTheory.CategoryStruct.comp g₂ β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.IsCofilteredOrEmpty C<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>∃ W h, CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.IsCofilteredOrEmpty C<VAR>X Y : C<GOAL>∃ W x x, True
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.IsCofiltered C<GOAL>Nonempty C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofilteredOrEmpty C<VAR>j j' : C<VAR>f f' : j ⟶ j'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') f = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') f'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofilteredOrEmpty C<VAR>i j j' : C<VAR>f : j ⟶ i<VAR>f' : j' ⟶ i<GOAL>∃ k g g', CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp g' f'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofilteredOrEmpty C<VAR>F : CategoryTheory.Functor C (Type u_1)<VAR>j : C<GOAL>Directed (fun x x_1 => x ⊇ x_1) fun f => Set.range (F.map f.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofilteredOrEmpty C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>CategoryTheory.IsCofilteredOrEmpty D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofilteredOrEmpty C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLeftAdjoint<GOAL>CategoryTheory.IsCofilteredOrEmpty D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofilteredOrEmpty C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>h : C ≌ D<GOAL>CategoryTheory.IsCofilteredOrEmpty D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofiltered C<VAR>O : Finset C<GOAL>∃ S, ∀ {X : C}, X ∈ O → Nonempty (S ⟶ X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofiltered C<VAR>O : Finset C<VAR>H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))<GOAL>∃ S T, ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → CategoryTheory.CategoryStruct.comp (T mX) f = T mY
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofiltered C<VAR>O : Finset C<VAR>H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))<VAR>X Y : C<VAR>mX : X ∈ O<VAR>mY : Y ∈ O<VAR>f : X ⟶ Y<VAR>mf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.infTo O H mX) f = CategoryTheory.IsCofiltered.infTo O H mY
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofiltered C<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.FinCategory J<VAR>F : CategoryTheory.Functor J C<GOAL>Nonempty (CategoryTheory.Limits.Cone F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofiltered C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>CategoryTheory.IsCofiltered D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofiltered C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLeftAdjoint<GOAL>CategoryTheory.IsCofiltered D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofiltered C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>h : C ≌ D<GOAL>CategoryTheory.IsCofiltered D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>h : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cone F)<GOAL>CategoryTheory.IsCofiltered C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteLimits C<GOAL>CategoryTheory.IsCofiltered C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>h : CategoryTheory.Limits.IsInitial X<GOAL>CategoryTheory.IsCofiltered C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.IsCofiltered C ↔ ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cone F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFilteredOrEmpty Cᵒᵖ<GOAL>CategoryTheory.IsCofilteredOrEmpty C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofilteredOrEmpty Cᵒᵖ<GOAL>CategoryTheory.IsFilteredOrEmpty C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsFiltered Cᵒᵖ<GOAL>CategoryTheory.IsCofiltered C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsCofiltered Cᵒᵖ<GOAL>CategoryTheory.IsFiltered C
<VAR>X Y : CategoryTheory.RelCat<VAR>f g : X ⟶ Y<VAR>h : ∀ (a : X) (b : Y), f a b ↔ g a b<GOAL>f = g
<VAR>X : CategoryTheory.RelCat<GOAL>CategoryTheory.CategoryStruct.id X = fun x x_1 => x = x_1
<VAR>X Y Z : CategoryTheory.RelCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f g = Rel.comp f g
<VAR>X : CategoryTheory.RelCat<VAR>x y : X<GOAL>CategoryTheory.CategoryStruct.id X x y ↔ x = y
<VAR>X Y Z : CategoryTheory.RelCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : X<VAR>z : Z<GOAL>CategoryTheory.CategoryStruct.comp f g x z ↔ ∃ y, f x y ∧ g y z
<VAR>X Y : Type u<VAR>f : X ⟶ Y<VAR>x : X<VAR>y : Y<GOAL>CategoryTheory.RelCat.graphFunctor.map f x y ↔ f x = y
<VAR>X Y : CategoryTheory.RelCat<VAR>r : X ⟶ Y<GOAL>CategoryTheory.IsIso r ↔ ∃ f, CategoryTheory.RelCat.graphFunctor.map f.hom = r
<GOAL>CategoryTheory.RelCat.opFunctor.comp CategoryTheory.RelCat.unopFunctor = CategoryTheory.Functor.id CategoryTheory.RelCat
<GOAL>CategoryTheory.RelCat.unopFunctor.comp CategoryTheory.RelCat.opFunctor = CategoryTheory.Functor.id CategoryTheory.RelCatᵒᵖ
<GOAL>CategoryTheory.RelCat.opEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id CategoryTheory.RelCat)
<GOAL>CategoryTheory.RelCat.opEquivalence.counitIso = CategoryTheory.Iso.refl (CategoryTheory.RelCat.unopFunctor.comp CategoryTheory.RelCat.opFunctor)
<GOAL>CategoryTheory.RelCat.opEquivalence.functor = CategoryTheory.RelCat.opFunctor
<GOAL>CategoryTheory.RelCat.opEquivalence.inverse = CategoryTheory.RelCat.unopFunctor
<VAR>ι α : Type v<VAR>U : ι → α<VAR>CompleteLattice α<VAR>o : CategoryTheory.Pairwise ι<GOAL>(CategoryTheory.Pairwise.cocone U).ι.app o = CategoryTheory.Pairwise.coconeιApp U o
<VAR>ι α : Type v<VAR>U : ι → α<VAR>CompleteLattice α<GOAL>(CategoryTheory.Pairwise.cocone U).pt = iSup U
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>down : C<GOAL>(CategoryTheory.ULift.upFunctor.obj down).down = down
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.ULift.upFunctor.map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : ULift.{u₂, u₁} C} (f : X ⟶ Y), CategoryTheory.ULift.downFunctor.map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : ULift.{u₂, u₁} C<GOAL>CategoryTheory.ULift.downFunctor.obj self = self.down
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : ULift.{u₂, u₁} C<GOAL>CategoryTheory.ULift.equivalence.counitIso.hom.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.ULift.downFunctor.comp CategoryTheory.ULift.upFunctor).obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.ULift.equivalence.functor = CategoryTheory.ULift.upFunctor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.ULift.equivalence.inverse = CategoryTheory.ULift.downFunctor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.ULift.equivalence.unitIso.inv = CategoryTheory.CategoryStruct.id (CategoryTheory.ULift.upFunctor.comp CategoryTheory.ULift.downFunctor)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.ULift.equivalence.unitIso.hom = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.id C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : ULift.{u₂, u₁} C<GOAL>CategoryTheory.ULift.equivalence.counitIso.inv.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (ULift.{u₂, u₁} C)).obj X)
<VAR>C : Type u_1<VAR>A : C<GOAL>(CategoryTheory.ULiftHom.objUp A).objDown = A
<VAR>C : Type u_1<VAR>A : CategoryTheory.ULiftHom C<GOAL>CategoryTheory.ULiftHom.objUp A.objDown = A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : C<GOAL>CategoryTheory.ULiftHom.up.obj A = CategoryTheory.ULiftHom.objUp A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.ULiftHom.up.map f).down = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : CategoryTheory.ULiftHom C} (f : X ⟶ Y), CategoryTheory.ULiftHom.down.map f = f.down
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : CategoryTheory.ULiftHom C<GOAL>CategoryTheory.ULiftHom.down.obj A = A.objDown
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.AsSmall.up.obj X).down = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.AsSmall.up.map f).down = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : CategoryTheory.AsSmall C<GOAL>CategoryTheory.AsSmall.down.obj X = X.down
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : CategoryTheory.AsSmall C} (f : X ⟶ Y), CategoryTheory.AsSmall.down.map f = f.down
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.AsSmall.equiv.counitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.eqToIso ⋯) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.AsSmall.equiv.unitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.eqToIso ⋯) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.AsSmall.equiv.functor = CategoryTheory.AsSmall.up
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.AsSmall.equiv.inverse = CategoryTheory.AsSmall.down
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>self : CategoryTheory.HasLiftingProperty i p<VAR>f : A ⟶ X<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<GOAL>sq.HasLift