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>∀ (α β : 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), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>F : CategoryTheory.Functor D E<VAR>(F : CategoryTheory.Functor D E) → (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>(F : CategoryTheory.Functor D E) → (X : C) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<GOAL>(J.sheafificationWhiskerLeftIso P).inv.app F = (J.sheafifyCompIso F P).inv
<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), 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>(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<GOAL>(J.sheafificationWhiskerRightIso F).hom.app P = (J.sheafifyCompIso F P).hom
<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), 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>(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<GOAL>(J.sheafificationWhiskerRightIso F).inv.app P = (J.sheafifyCompIso F P).inv
<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), 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>(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<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (J.toSheafify P) F) (J.sheafifyCompIso F P).hom = J.toSheafify (P.comp F)
<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), 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>(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<GOAL>CategoryTheory.CategoryStruct.comp (J.toSheafify (P.comp F)) (J.sheafifyCompIso F P).inv = CategoryTheory.whiskerRight (J.toSheafify P) F
<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), 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>(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>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<GOAL>(J.sheafifyCompIso F P).inv = J.sheafifyLift (CategoryTheory.whiskerRight (J.toSheafify P) F) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Groupoid C<GOAL>Quiver.IsThin C ↔ ∀ (c : C), Subsingleton (c ⟶ c)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : CategoryTheory.End X<GOAL>α.conj f = CategoryTheory.CategoryStruct.comp α.inv (CategoryTheory.CategoryStruct.comp f α.hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f g : CategoryTheory.End X<GOAL>α.conj (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (α.conj f) (α.conj g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<GOAL>α.conj (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>f : CategoryTheory.End X<GOAL>(CategoryTheory.Iso.refl X).conj f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>Z : C<VAR>β : Y ≅ Z<VAR>f : CategoryTheory.End X<GOAL>(α ≪≫ β).conj f = β.conj (α.conj f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : CategoryTheory.End X<GOAL>α.symm.conj (α.conj f) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : CategoryTheory.End Y<GOAL>α.conj (α.symm.conj f) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : CategoryTheory.End X<VAR>n : ℕ<GOAL>α.conj (f ^ n) = α.conj f ^ n
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : CategoryTheory.Aut X<GOAL>α.conjAut f = α.symm ≪≫ f ≪≫ α
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : CategoryTheory.Aut X<GOAL>(α.conjAut f).hom = α.conj f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>Z : C<VAR>β : Y ≅ Z<VAR>f : CategoryTheory.Aut X<GOAL>(α ≪≫ β).conjAut f = β.conjAut (α.conjAut f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f g : CategoryTheory.Aut X<GOAL>α.conjAut (f * g) = α.conjAut f * α.conjAut g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f g : CategoryTheory.Aut X<GOAL>α.conjAut (f ≪≫ g) = α.conjAut f ≪≫ α.conjAut g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : CategoryTheory.Aut X<VAR>n : ℕ<GOAL>α.conjAut (f ^ n) = α.conjAut f ^ n
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : CategoryTheory.Aut X<VAR>n : ℤ<GOAL>α.conjAut (f ^ n) = α.conjAut f ^ n
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : CategoryTheory.End X<GOAL>F.map (α.conj f) = (F.mapIso α).conj (F.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : CategoryTheory.Aut X<GOAL>F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>S : CategoryTheory.Presieve X<VAR>R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y<VAR>g : Z ⟶ Y<VAR>h₁ : S f<VAR>h₂ : R h₁ g<GOAL>S.bind R (CategoryTheory.CategoryStruct.comp g f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<GOAL>CategoryTheory.Presieve.singleton f f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f g : Y ⟶ X<GOAL>CategoryTheory.Presieve.singleton f g ↔ f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>g : Z ⟶ X<GOAL>CategoryTheory.Presieve.pullbackArrows f (CategoryTheory.Presieve.singleton g) = CategoryTheory.Presieve.singleton (CategoryTheory.Limits.pullback.snd g f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<GOAL>(CategoryTheory.Presieve.ofArrows (fun x => Y) fun x => f) = CategoryTheory.Presieve.singleton f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>ι : Type u_1<VAR>Z : ι → C<VAR>g : (i : ι) → Z i ⟶ X<GOAL>(CategoryTheory.Presieve.ofArrows (fun i => CategoryTheory.Limits.pullback (g i) f) fun i => CategoryTheory.Limits.pullback.snd (g i) f) = CategoryTheory.Presieve.pullbackArrows f (CategoryTheory.Presieve.ofArrows Z g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>ι : Type u_1<VAR>Z : ι → C<VAR>g : (i : ι) → Z i ⟶ X<VAR>j : ⦃Y : C⦄ → (f : Y ⟶ X) → CategoryTheory.Presieve.ofArrows Z g f → Type u_2<VAR>W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : CategoryTheory.Presieve.ofArrows Z g f) → j f H → C<VAR>k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : CategoryTheory.Presieve.ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y<GOAL>((CategoryTheory.Presieve.ofArrows Z g).bind fun Y f H => CategoryTheory.Presieve.ofArrows (W f H) (k f H)) = CategoryTheory.Presieve.ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => CategoryTheory.CategoryStruct.comp (k (g ij.fst) ⋯ ij.snd) (g ij.fst)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>ι : Type u_1<VAR>Y : ι → C<VAR>f : (i : ι) → Y i ⟶ X<VAR>Z : C<VAR>g : Z ⟶ X<VAR>hg : CategoryTheory.Presieve.ofArrows Y f g<GOAL>∃ i, ∃ (h : Y i = Z), g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (f i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>R : CategoryTheory.Presieve (F.obj X)<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>CategoryTheory.Presieve.functorPullback F R f ↔ R (F.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R : CategoryTheory.Presieve X<GOAL>CategoryTheory.Presieve.functorPullback (CategoryTheory.Functor.id C) R = R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>self : R.hasPullbacks<VAR>Y Z : C<VAR>f : Y ⟶ X<GOAL>R f → ∀ {g : Z ⟶ X}, R g → CategoryTheory.Limits.HasPullback f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>S : CategoryTheory.Presieve X<VAR>Y : D<VAR>f : Y ⟶ F.obj X<VAR>self : CategoryTheory.Presieve.FunctorPushforwardStructure F S f<GOAL>S self.premap
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>S : CategoryTheory.Presieve X<VAR>Y : D<VAR>f : Y ⟶ F.obj X<VAR>self : CategoryTheory.Presieve.FunctorPushforwardStructure F S f<GOAL>f = CategoryTheory.CategoryStruct.comp self.lift (F.map self.premap)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>R : CategoryTheory.Presieve X<GOAL>CategoryTheory.Presieve.functorPushforward (F.comp G) R = CategoryTheory.Presieve.functorPushforward G (CategoryTheory.Presieve.functorPushforward F R)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>R : CategoryTheory.Presieve X<VAR>f : Y ⟶ X<VAR>h : R f<GOAL>CategoryTheory.Presieve.functorPushforward F R (F.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>self : CategoryTheory.Sieve X<VAR>Y Z : C<VAR>f : Y ⟶ X<GOAL>self.arrows f → ∀ (g : Z ⟶ Y), self.arrows (CategoryTheory.CategoryStruct.comp g f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R S : CategoryTheory.Sieve X<GOAL>R.arrows = S.arrows → R = S
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R S : CategoryTheory.Sieve X<VAR>h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), R.arrows f ↔ S.arrows f<GOAL>R = S
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R S : CategoryTheory.Sieve X<GOAL>R = S ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X), R.arrows f ↔ S.arrows f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>Ss : Set (CategoryTheory.Sieve X)<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>(sInf Ss).arrows f ↔ ∀ S ∈ Ss, S.arrows f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>Ss : Set (CategoryTheory.Sieve X)<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>(sSup Ss).arrows f ↔ ∃ S, ∃ (_ : S ∈ Ss), S.arrows f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R S : CategoryTheory.Sieve X<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>(R ⊓ S).arrows f ↔ R.arrows f ∧ S.arrows f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R S : CategoryTheory.Sieve X<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>(R ⊔ S).arrows f ↔ R.arrows f ∨ S.arrows f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<GOAL>⊤.arrows f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>Z : C<VAR>f : Z ⟶ X<GOAL>(CategoryTheory.Sieve.generate R).arrows f = ∃ Y h g, R g ∧ CategoryTheory.CategoryStruct.comp h g = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Presieve X<VAR>R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y<GOAL>(CategoryTheory.Sieve.bind S R).arrows = S.bind fun Y f h => (R h).arrows
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>S : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.generate R ≤ S ↔ R ≤ S.arrows
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R : CategoryTheory.Presieve X<GOAL>R ≤ (CategoryTheory.Sieve.generate R).arrows
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.generate S.arrows = S
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>S.arrows (CategoryTheory.CategoryStruct.id X) ↔ S = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>R : CategoryTheory.Presieve X<VAR>f : Y ⟶ X<VAR>CategoryTheory.IsSplitEpi f<VAR>hf : R f<GOAL>CategoryTheory.Sieve.generate R = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>CategoryTheory.IsSplitEpi f<GOAL>CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton f) = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>CategoryTheory.Sieve.generate ⊤ = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>i : X ⟶ Y<VAR>f : Y ⟶ Z<VAR>CategoryTheory.IsIso i<VAR>S : CategoryTheory.Sieve Z<GOAL>S.arrows (CategoryTheory.CategoryStruct.comp i f) ↔ S.arrows f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>I : Type u_1<VAR>X : C<VAR>Y : I → C<VAR>f : (i : I) → Y i ⟶ X<VAR>i : I<GOAL>(CategoryTheory.Sieve.ofArrows Y f).arrows (f i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>I : Type u_1<VAR>X : C<VAR>Y : I → C<VAR>f : (i : I) → Y i ⟶ X<VAR>W : C<VAR>g : W ⟶ X<GOAL>(CategoryTheory.Sieve.ofArrows Y f).arrows g ↔ ∃ i a, g = CategoryTheory.CategoryStruct.comp a (f i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>I : Type u_1<VAR>Y : I → C<VAR>Z X : C<VAR>g : Z ⟶ X<GOAL>(CategoryTheory.Sieve.ofObjects Y X).arrows g ↔ ∃ i, Nonempty (Z ⟶ Y i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>I : Type u_1<VAR>Y : I → C<VAR>X : C<VAR>f : (i : I) → Y i ⟶ X<GOAL>CategoryTheory.Sieve.ofArrows Y f ≤ CategoryTheory.Sieve.ofObjects Y X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>hX : CategoryTheory.Limits.IsTerminal X<VAR>I : Type u_1<VAR>Y : I → C<VAR>f : (i : I) → Y i ⟶ X<GOAL>CategoryTheory.Sieve.ofArrows Y f = CategoryTheory.Sieve.ofObjects Y X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>h : Y ⟶ X<VAR>S : CategoryTheory.Sieve X<GOAL>∀ (Y_1 : C) (sl : Y_1 ⟶ Y), (CategoryTheory.Sieve.pullback h S).arrows sl = S.arrows (CategoryTheory.CategoryStruct.comp sl h)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.id X) S = S
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<GOAL>CategoryTheory.Sieve.pullback f ⊤ = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>g : Z ⟶ Y<VAR>S : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp g f) S = CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.pullback f S)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>S R : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.pullback f (S ⊓ R) = CategoryTheory.Sieve.pullback f S ⊓ CategoryTheory.Sieve.pullback f R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>S : CategoryTheory.Sieve X<VAR>f : Y ⟶ X<GOAL>S.arrows f ↔ CategoryTheory.Sieve.pullback f S = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>S : CategoryTheory.Sieve X<VAR>f : Y ⟶ X<GOAL>S.arrows f → CategoryTheory.Sieve.pullback f S = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>I : Type u_1<VAR>Y : I → C<VAR>X : C<VAR>i : I<VAR>g : X ⟶ Y i<GOAL>CategoryTheory.Sieve.ofObjects Y X = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>R : CategoryTheory.Sieve Y<VAR>Z : C<VAR>gf : Z ⟶ X<GOAL>(CategoryTheory.Sieve.pushforward f R).arrows gf = ∃ g, CategoryTheory.CategoryStruct.comp g f = gf ∧ R.arrows g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>R : CategoryTheory.Sieve Y<VAR>Z : C<VAR>g : Z ⟶ Y<VAR>hg : R.arrows g<VAR>f : Y ⟶ X<GOAL>(CategoryTheory.Sieve.pushforward f R).arrows (CategoryTheory.CategoryStruct.comp g f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>g : Z ⟶ Y<VAR>R : CategoryTheory.Sieve Z<GOAL>CategoryTheory.Sieve.pushforward (CategoryTheory.CategoryStruct.comp g f) R = CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.pushforward g R)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<GOAL>GaloisConnection (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<GOAL>Monotone (CategoryTheory.Sieve.pullback f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<GOAL>Monotone (CategoryTheory.Sieve.pushforward f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>R : CategoryTheory.Sieve Y<GOAL>R ≤ CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.pushforward f R)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>R : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.pullback f R) ≤ R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>S R : CategoryTheory.Sieve Y<GOAL>CategoryTheory.Sieve.pushforward f (S ⊔ R) = CategoryTheory.Sieve.pushforward f S ⊔ CategoryTheory.Sieve.pushforward f R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>S : CategoryTheory.Presieve X<VAR>R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y<VAR>f : Y ⟶ X<VAR>h : S f<GOAL>CategoryTheory.Sieve.pushforward f (R h) ≤ CategoryTheory.Sieve.bind S R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>S : CategoryTheory.Presieve X<VAR>R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y<VAR>f : Y ⟶ X<VAR>h : S f<GOAL>R h ≤ CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.bind S R)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>R : CategoryTheory.Presieve X<GOAL>CategoryTheory.Sieve.generate (CategoryTheory.Presieve.pullbackArrows f R) = CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.generate R)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>R : CategoryTheory.Sieve (F.obj X)<GOAL>(CategoryTheory.Sieve.functorPullback F R).arrows = CategoryTheory.Presieve.functorPullback F R.arrows
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.functorPullback (CategoryTheory.Functor.id C) R = R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>R : CategoryTheory.Sieve ((F.comp G).obj X)<GOAL>CategoryTheory.Sieve.functorPullback (F.comp G) R = CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.functorPullback G R)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>R : CategoryTheory.Presieve X<GOAL>CategoryTheory.Presieve.functorPushforward F (CategoryTheory.Sieve.generate R).arrows = CategoryTheory.Presieve.functorPushforward F R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>R : CategoryTheory.Sieve X<GOAL>(CategoryTheory.Sieve.functorPushforward F R).arrows = CategoryTheory.Presieve.functorPushforward F R.arrows
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.functorPushforward (CategoryTheory.Functor.id C) R = R