ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>α : Type<VAR>X : α → C<VAR>c : CategoryTheory.Limits.Cofan X<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>(CategoryTheory.Presieve.ofArrows X c.inj).hasPullbacks<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F<GOAL>CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : CategoryTheory.Limits.IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : CategoryTheory.Limits.Cofan X<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>(CategoryTheory.Presieve.ofArrows X c.inj).hasPullbacks<VAR>CategoryTheory.Limits.HasInitial C<VAR>∀ (i : α), CategoryTheory.Mono (c.inj i)<VAR>hd : Pairwise fun i j => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)<GOAL>CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj) ↔ Nonempty (CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_7, u_3} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>CategoryTheory.ConcreteCategory A<VAR>H.IsCocontinuous J K<VAR>CategoryTheory.Presheaf.IsLocallyInjective K f<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.whiskerLeft H.op f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_7, u_3} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>CategoryTheory.ConcreteCategory A<VAR>hH : CategoryTheory.CoverPreserving J K H<VAR>H.IsCoverDense K<VAR>CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.whiskerLeft H.op f)<GOAL>CategoryTheory.Presheaf.IsLocallyInjective K f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_7, u_3} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>CategoryTheory.ConcreteCategory A<VAR>hH : CategoryTheory.CoverPreserving J K H<VAR>H.IsCocontinuous J K<VAR>H.IsCoverDense K<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.whiskerLeft H.op f) ↔ CategoryTheory.Presheaf.IsLocallyInjective K f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>CategoryTheory.ConcreteCategory A<VAR>H.IsCocontinuous J K<VAR>CategoryTheory.Presheaf.IsLocallySurjective K f<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.whiskerLeft H.op f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>CategoryTheory.ConcreteCategory A<VAR>hH : CategoryTheory.CoverPreserving J K H<VAR>H.IsCoverDense K<VAR>CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.whiskerLeft H.op f)<GOAL>CategoryTheory.Presheaf.IsLocallySurjective K f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>CategoryTheory.ConcreteCategory A<VAR>hH : CategoryTheory.CoverPreserving J K H<VAR>H.IsCocontinuous J K<VAR>H.IsCoverDense K<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.whiskerLeft H.op f) ↔ CategoryTheory.Presheaf.IsLocallySurjective K f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>CategoryTheory.HasWeakSheafify J (Type v)<VAR>self : J.MayerVietorisSquare<GOAL>CategoryTheory.Mono self.f₁₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>CategoryTheory.HasWeakSheafify J (Type v)<VAR>self : J.MayerVietorisSquare<GOAL>(self.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<VAR>E : CategoryTheory.PreOneHypercover X<VAR>F : CategoryTheory.Functor C D<VAR>i : E.I₀<GOAL>(E.map F).X i = F.obj (E.X i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<VAR>E : CategoryTheory.PreOneHypercover X<VAR>F : CategoryTheory.Functor C D<GOAL>∀ (x x_1 : E.I₀) (j : E.I₁ x x_1), (E.map F).p₂ j = F.map (E.p₂ j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<VAR>E : CategoryTheory.PreOneHypercover X<VAR>F : CategoryTheory.Functor C D<GOAL>∀ (x x_1 : E.I₀) (j : E.I₁ x x_1), (E.map F).p₁ j = F.map (E.p₁ j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<VAR>E : CategoryTheory.PreOneHypercover X<VAR>F : CategoryTheory.Functor C D<GOAL>(E.map F).I₀ = E.I₀
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<VAR>E : CategoryTheory.PreOneHypercover X<VAR>F : CategoryTheory.Functor C D<VAR>i : E.I₀<GOAL>(E.map F).f i = F.map (E.f i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<VAR>E : CategoryTheory.PreOneHypercover X<VAR>F : CategoryTheory.Functor C D<GOAL>∀ (x x_1 : E.I₀) (j : E.I₁ x x_1), (E.map F).Y j = F.obj (E.Y j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<VAR>E : CategoryTheory.PreOneHypercover X<VAR>F : CategoryTheory.Functor C D<VAR>i₁ i₂ : E.I₀<GOAL>(E.map F).I₁ i₁ i₂ = E.I₁ i₁ i₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>E : J.OneHypercover X<VAR>F : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>self : E.IsPreservedBy F K<VAR>i₁ i₂ : E.I₀<VAR>W : D<VAR>p₁ : W ⟶ F.obj (E.X i₁)<VAR>p₂ : W ⟶ F.obj (E.X i₂)<VAR>w : CategoryTheory.CategoryStruct.comp p₁ (F.map (E.f i₁)) = CategoryTheory.CategoryStruct.comp p₂ (F.map (E.f i₂))<GOAL>(E.map F).sieve₁ p₁ p₂ ∈ K.sieves W
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>E : J.OneHypercover X<VAR>F : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>self : E.IsPreservedBy F K<GOAL>(E.map F).sieve₀ ∈ K.sieves (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>E : J.OneHypercover X<VAR>F : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>E.IsPreservedBy F K<GOAL>(E.map F K).toPreOneHypercover = E.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>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>self : F.IsContinuous J K<VAR>G : CategoryTheory.SheafOfTypes K<GOAL>CategoryTheory.Presieve.IsSheaf J (F.op.comp G.val)
<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>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F.IsContinuous J K<VAR>G : CategoryTheory.SheafOfTypes K<GOAL>CategoryTheory.Presieve.IsSheaf J (F.op.comp G.val)
<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>A : Type u<VAR>CategoryTheory.Category.{t, u} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F.IsContinuous J K<VAR>G : CategoryTheory.Sheaf K A<GOAL>CategoryTheory.Presheaf.IsSheaf J (F.op.comp G.val)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>e : F₁ ≅ F₂<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F₁.IsContinuous J K<GOAL>F₂.IsContinuous J K
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F₁ : CategoryTheory.Functor C D<VAR>F₂ : CategoryTheory.Functor D E<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>L : CategoryTheory.GrothendieckTopology E<VAR>F₁.IsContinuous J K<VAR>F₂.IsContinuous K L<GOAL>(F₁.comp F₂).IsContinuous J L
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F₁ : CategoryTheory.Functor C D<VAR>F₂ : CategoryTheory.Functor D E<VAR>F₁₂ : CategoryTheory.Functor C E<VAR>e : F₁.comp F₂ ≅ F₁₂<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>L : CategoryTheory.GrothendieckTopology E<VAR>F₁.IsContinuous J K<VAR>F₂.IsContinuous K L<GOAL>F₁₂.IsContinuous J L
<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>A : Type u<VAR>CategoryTheory.Category.{t, u} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F.PreservesOneHypercovers J K<VAR>J.IsGeneratedByOneHypercovers<VAR>P : CategoryTheory.Functor Dᵒᵖ A<VAR>hP : CategoryTheory.Presheaf.IsSheaf K P<GOAL>CategoryTheory.Presheaf.IsSheaf J (F.op.comp P)
<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>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F.PreservesOneHypercovers J K<VAR>J.IsGeneratedByOneHypercovers<GOAL>F.IsContinuous J K
<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>A : Type u<VAR>CategoryTheory.Category.{t, u} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F.IsContinuous J K<VAR>ℱ : CategoryTheory.Sheaf K A<VAR>X : Cᵒᵖ<GOAL>((F.sheafPushforwardContinuous A J K).obj ℱ).val.obj X = ℱ.val.obj (Opposite.op (F.obj (Opposite.unop X)))
<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>A : Type u<VAR>CategoryTheory.Category.{t, u} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F.IsContinuous J K<VAR>ℱ : CategoryTheory.Sheaf K A<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), ((F.sheafPushforwardContinuous A J K).obj ℱ).val.map f = ℱ.val.map (F.map f.unop).op
<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>A : Type u<VAR>CategoryTheory.Category.{t, u} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F.IsContinuous J K<GOAL>∀ {X Y : CategoryTheory.Sheaf K A} (f : X ⟶ Y) (X_1 : Cᵒᵖ), ((F.sheafPushforwardContinuous A J K).map f).val.app X_1 = f.val.app (Opposite.op (F.obj (Opposite.unop X_1)))
<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>A : Type u<VAR>CategoryTheory.Category.{t, u} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F.IsContinuous J K<VAR>X : CategoryTheory.Sheaf K A<GOAL>∀ (X_1 : Cᵒᵖ), ((F.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.val.obj (Opposite.op (F.obj (Opposite.unop X_1))))
<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>A : Type u<VAR>CategoryTheory.Category.{t, u} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F.IsContinuous J K<VAR>X : CategoryTheory.Sheaf K A<GOAL>∀ (X_1 : Cᵒᵖ), ((F.sheafPushforwardContinuousCompSheafToPresheafIso A J K).hom.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.val.obj (Opposite.op (F.obj (Opposite.unop X_1))))
<VAR>C : Type uC<VAR>CategoryTheory.Category.{vC, uC} C<VAR>D : Type uD<VAR>CategoryTheory.Category.{vD, uD} D<VAR>G : CategoryTheory.Functor C D<VAR>U V : C<VAR>f : U ⟶ V<GOAL>G.imageSieve (G.map f) = ⊤
<VAR>C : Type uC<VAR>CategoryTheory.Category.{vC, uC} C<VAR>U V : C<VAR>f₁ f₂ : U ⟶ V<VAR>Y : C<VAR>i : Y ⟶ U<GOAL>(CategoryTheory.Sieve.equalizer f₁ f₂).arrows i = (CategoryTheory.CategoryStruct.comp i f₁ = CategoryTheory.CategoryStruct.comp i f₂)
<VAR>C : Type uC<VAR>CategoryTheory.Category.{vC, uC} C<VAR>U V : C<VAR>f : U ⟶ V<GOAL>CategoryTheory.Sieve.equalizer f f = ⊤
<VAR>C : Type uC<VAR>CategoryTheory.Category.{vC, uC} C<VAR>U V : C<VAR>f₁ f₂ : U ⟶ V<GOAL>CategoryTheory.Sieve.equalizer f₁ f₂ = CategoryTheory.Presheaf.equalizerSieve f₁ f₂
<VAR>C : Type uC<VAR>CategoryTheory.Category.{vC, uC} C<VAR>D : Type uD<VAR>CategoryTheory.Category.{vC, uD} D<VAR>G : CategoryTheory.Functor C D<VAR>U V : C<VAR>f : G.obj U ⟶ G.obj V<GOAL>G.imageSieve f = CategoryTheory.Presheaf.imageSieve (CategoryTheory.yonedaMap G V) f
<VAR>C : Type uC<VAR>CategoryTheory.Category.{vC, uC} C<VAR>D : Type uD<VAR>CategoryTheory.Category.{vD, uD} D<VAR>G : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>self : G.IsLocallyFull K<VAR>U V : C<VAR>f : G.obj U ⟶ G.obj V<GOAL>CategoryTheory.Sieve.functorPushforward G (G.imageSieve f) ∈ K.sieves (G.obj U)
<VAR>C : Type uC<VAR>CategoryTheory.Category.{vC, uC} C<VAR>D : Type uD<VAR>CategoryTheory.Category.{vD, uD} D<VAR>G : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>self : G.IsLocallyFaithful K<VAR>U V : C<VAR>f₁ f₂ : U ⟶ V<GOAL>G.map f₁ = G.map f₂ → CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.equalizer f₁ f₂) ∈ K.sieves (G.obj U)
<VAR>C : Type uC<VAR>CategoryTheory.Category.{vC, uC} C<VAR>D : Type uD<VAR>CategoryTheory.Category.{vD, uD} D<VAR>G : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsLocallyFull K<VAR>U V : C<VAR>f : G.obj U ⟶ G.obj V<GOAL>CategoryTheory.Sieve.functorPushforward G (G.imageSieve f) ∈ K.sieves (G.obj U)
<VAR>C : Type uC<VAR>CategoryTheory.Category.{vC, uC} C<VAR>D : Type uD<VAR>CategoryTheory.Category.{vD, uD} D<VAR>G : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsLocallyFaithful K<VAR>U V : C<VAR>f₁ f₂ : U ⟶ V<VAR>e : G.map f₁ = G.map f₂<GOAL>CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.equalizer f₁ f₂) ∈ K.sieves (G.obj U)
<VAR>C : Type uC<VAR>CategoryTheory.Category.{vC, uC} C<VAR>D : Type uD<VAR>CategoryTheory.Category.{vD, uD} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsLocallyFull K<VAR>ℱ : CategoryTheory.SheafOfTypes K<VAR>X Y : C<VAR>i : G.obj X ⟶ G.obj Y<VAR>s t : ℱ.val.obj (Opposite.op (G.obj X))<VAR>h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = CategoryTheory.CategoryStruct.comp (G.map j) i → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t<GOAL>s = t
<VAR>C : Type uC<VAR>CategoryTheory.Category.{vC, uC} C<VAR>D : Type uD<VAR>CategoryTheory.Category.{vD, uD} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsLocallyFaithful K<VAR>ℱ : CategoryTheory.SheafOfTypes K<VAR>X Y : C<VAR>i₁ i₂ : X ⟶ Y<VAR>e : G.map i₁ = G.map i₂<VAR>s t : ℱ.val.obj (Opposite.op (G.obj X))<VAR>h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), CategoryTheory.CategoryStruct.comp j i₁ = CategoryTheory.CategoryStruct.comp j i₂ → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t<GOAL>s = t
<VAR>T : Type u<VAR>TopologicalSpace T<GOAL>CategoryTheory.Pretopology.ofGrothendieck (TopologicalSpace.Opens T) (Opens.grothendieckTopology T) = Opens.pretopology T
<VAR>T : Type u<VAR>TopologicalSpace T<GOAL>CategoryTheory.Pretopology.toGrothendieck (TopologicalSpace.Opens T) (Opens.pretopology T) = Opens.grothendieckTopology T
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>⊤.obj.left = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>⊤.arrow = 𝟙 X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.InitialMonoClass C<VAR>X : C<GOAL>⊥.obj.left = ⊥_ C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.InitialMonoClass C<VAR>X : C<GOAL>⊥.arrow = CategoryTheory.Limits.initial.to X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>B : C<GOAL>⊥.arrow = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A : C<GOAL>∀ {X Y : CategoryTheory.MonoOver A} (k : X ⟶ Y) (g : CategoryTheory.MonoOver A), (CategoryTheory.MonoOver.inf.map k).app g = CategoryTheory.MonoOver.homMk (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.fst ((CategoryTheory.MonoOver.forget A).obj g).hom X.arrow) (CategoryTheory.Limits.pullback.snd ((CategoryTheory.MonoOver.forget A).obj g).hom X.arrow ≫ k.left) ⋯) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A : C<VAR>f : CategoryTheory.MonoOver A<GOAL>CategoryTheory.MonoOver.inf.obj f = CategoryTheory.MonoOver.pullback f.arrow ⋙ CategoryTheory.MonoOver.map f.arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B : C<GOAL>⊤ = CategoryTheory.Subobject.mk (𝟙 B)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B : C<GOAL>(CategoryTheory.Subobject.underlyingIso (𝟙 B)).hom = ⊤.arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B : C<GOAL>(CategoryTheory.Subobject.underlyingIso (𝟙 B)).inv ≫ ⊤.arrow = 𝟙 B
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>(CategoryTheory.Subobject.map f).obj ⊤ = CategoryTheory.Subobject.mk f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A B : C<VAR>f : A ⟶ B<GOAL>⊤.Factors f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.IsIso f ↔ CategoryTheory.Subobject.mk f = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Y : C<VAR>P : CategoryTheory.Subobject Y<GOAL>CategoryTheory.IsIso P.arrow ↔ P = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.Subobject.mk f = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>CategoryTheory.IsIso P.arrow<GOAL>P = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Subobject.pullback f).obj ⊤ = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A B : C<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<GOAL>(CategoryTheory.Subobject.pullback f).obj (CategoryTheory.Subobject.mk f) = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.InitialMonoClass C<VAR>B : C<GOAL>⊥ = CategoryTheory.Subobject.mk (CategoryTheory.Limits.initial.to B)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.InitialMonoClass C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>(CategoryTheory.Subobject.map f).obj ⊥ = ⊥
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>B : C<GOAL>⊥ = CategoryTheory.Subobject.mk 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>A B : C<VAR>f : A ⟶ B<GOAL>⊥.Factors f ↔ f = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Subobject.mk f = ⊥ ↔ f = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.Subobject.functor C).obj X = CategoryTheory.Subobject (Opposite.unop X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (a : CategoryTheory.Subobject (Opposite.unop X)), (CategoryTheory.Subobject.functor C).map f a = (CategoryTheory.Subobject.pullback f.unop).obj a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A : C<VAR>f g : CategoryTheory.Subobject A<GOAL>(CategoryTheory.Subobject.inf.obj f).obj g ≤ f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A : C<VAR>f g : CategoryTheory.Subobject A<GOAL>(CategoryTheory.Subobject.inf.obj f).obj g ≤ g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A : C<VAR>h f g : CategoryTheory.Subobject A<GOAL>h ≤ f → h ≤ g → h ≤ (CategoryTheory.Subobject.inf.obj f).obj g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A B : C<VAR>X Y : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>h : (X ⊓ Y).Factors f<GOAL>X.Factors f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A B : C<VAR>X Y : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>h : (X ⊓ Y).Factors f<GOAL>Y.Factors f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A B : C<VAR>X Y : CategoryTheory.Subobject B<VAR>f : A ⟶ B<GOAL>(X ⊓ Y).Factors f ↔ X.Factors f ∧ Y.Factors f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>B : C<VAR>X Y : CategoryTheory.Subobject B<GOAL>X.Factors (X ⊓ Y).arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>B : C<VAR>X Y : CategoryTheory.Subobject B<GOAL>Y.Factors (X ⊓ Y).arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>I : Type u_1<VAR>A B : C<VAR>s : Finset I<VAR>P : I → CategoryTheory.Subobject B<VAR>f : A ⟶ B<GOAL>(s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f