ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D<VAR>φ : F₁ ⟶ F₂<VAR>self : CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>X : Cᵒᵖ<VAR>x y : (CategoryTheory.forget D).obj (F₁.obj X)<VAR>h : (φ.app X) x = (φ.app X) y<GOAL>CategoryTheory.Presheaf.equalizerSieve x y ∈ J.sieves (Opposite.unop X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D<VAR>φ : F₁ ⟶ F₂<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>X : Cᵒᵖ<VAR>x y : (CategoryTheory.forget D).obj (F₁.obj X)<VAR>h : (φ.app X) x = (φ.app X) y<GOAL>CategoryTheory.Presheaf.equalizerSieve x y ∈ J.sieves (Opposite.unop X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D<VAR>φ : F₁ ⟶ F₂<VAR>hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.app X)<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D<VAR>φ : F₁ ⟶ F₂<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.whiskerRight φ (CategoryTheory.forget D)) ↔ CategoryTheory.Presheaf.IsLocallyInjective J φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D<VAR>φ : F₁ ⟶ F₂<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J φ ↔ ∀ ⦃X : Cᵒᵖ⦄ (x y : (CategoryTheory.forget D).obj (F₁.obj X)), CategoryTheory.Presheaf.equalizerSieve ((φ.app X) x) ((φ.app X) y) ∈ J.sieves (Opposite.unop X) → CategoryTheory.Presheaf.equalizerSieve x y ∈ J.sieves (Opposite.unop X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D<VAR>φ : F₁ ⟶ F₂<VAR>X : Cᵒᵖ<VAR>x y : (CategoryTheory.forget D).obj (F₁.obj X)<VAR>h : CategoryTheory.Presheaf.equalizerSieve ((φ.app X) x) ((φ.app X) y) ∈ J.sieves (Opposite.unop X)<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<GOAL>CategoryTheory.Presheaf.equalizerSieve x y ∈ J.sieves (Opposite.unop X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ D<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<VAR>CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.CategoryStruct.comp φ ψ)<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ D<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<VAR>φψ : F₁ ⟶ F₃<VAR>fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φψ<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ D<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<VAR>φψ : F₁ ⟶ F₃<VAR>fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ<VAR>CategoryTheory.Presheaf.IsLocallyInjective J ψ<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J φψ ↔ CategoryTheory.Presheaf.IsLocallyInjective J φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ D<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<VAR>CategoryTheory.Presheaf.IsLocallyInjective J ψ<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.CategoryStruct.comp φ ψ) ↔ CategoryTheory.Presheaf.IsLocallyInjective J φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D<VAR>φ : F₁ ⟶ F₂<VAR>hsep : CategoryTheory.Presieve.IsSeparated J (F₁.comp (CategoryTheory.forget D))<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J φ ↔ ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ : CategoryTheory.Sheaf J D<VAR>φ : F₁ ⟶ F₂<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J ((CategoryTheory.sheafToPresheaf J D).map φ) ↔ CategoryTheory.Sheaf.IsLocallyInjective φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ : CategoryTheory.Sheaf J D<VAR>φ : F₁ ⟶ F₂<VAR>J.HasSheafCompose (CategoryTheory.forget D)<GOAL>CategoryTheory.Sheaf.IsLocallyInjective φ ↔ ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.val.app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ : CategoryTheory.Sheaf J D<VAR>φ : F₁ ⟶ F₂<VAR>hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.val.app X)<GOAL>CategoryTheory.Mono φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F₁ F₂ : CategoryTheory.Sheaf J D<VAR>φ : F₁ ⟶ F₂<VAR>J.HasSheafCompose (CategoryTheory.forget D)<VAR>CategoryTheory.Sheaf.IsLocallyInjective φ<GOAL>CategoryTheory.Mono φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F G : CategoryTheory.Sheaf J (Type w)<VAR>f : F ⟶ G<GOAL>CategoryTheory.Sheaf.IsLocallyInjective f ∧ CategoryTheory.Sheaf.IsLocallySurjective f ↔ CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F G : CategoryTheory.Sheaf J A<VAR>f : F ⟶ G<VAR>(CategoryTheory.forget A).ReflectsIsomorphisms<VAR>J.HasSheafCompose (CategoryTheory.forget A)<GOAL>CategoryTheory.Sheaf.IsLocallyInjective f ∧ CategoryTheory.Sheaf.IsLocallySurjective f ↔ CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>self : J.WEqualsLocallyBijective A<VAR>X Y : CategoryTheory.Functor Cᵒᵖ A<VAR>f : X ⟶ Y<GOAL>J.W f ↔ CategoryTheory.Presheaf.IsLocallyInjective J f ∧ CategoryTheory.Presheaf.IsLocallySurjective J f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>J.WEqualsLocallyBijective A<VAR>X Y : CategoryTheory.Functor Cᵒᵖ A<VAR>f : X ⟶ Y<GOAL>J.W f ↔ CategoryTheory.Presheaf.IsLocallyInjective J f ∧ CategoryTheory.Presheaf.IsLocallySurjective J f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>J.WEqualsLocallyBijective A<VAR>X Y : CategoryTheory.Functor Cᵒᵖ A<VAR>f : X ⟶ Y<VAR>CategoryTheory.Presheaf.IsLocallyInjective J f<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f<GOAL>J.W f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>J.WEqualsLocallyBijective A<VAR>X Y : CategoryTheory.Functor Cᵒᵖ A<VAR>f : X ⟶ Y<VAR>hf : J.W f<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>J.WEqualsLocallyBijective A<VAR>X Y : CategoryTheory.Functor Cᵒᵖ A<VAR>f : X ⟶ Y<VAR>hf : J.W f<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>CategoryTheory.HasWeakSheafify J A<VAR>(CategoryTheory.forget A).ReflectsIsomorphisms<VAR>J.HasSheafCompose (CategoryTheory.forget A)<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)<GOAL>J.WEqualsLocallyBijective A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>CategoryTheory.HasWeakSheafify J A<VAR>J.WEqualsLocallyBijective A<VAR>P Q : CategoryTheory.Functor Cᵒᵖ A<VAR>φ : P ⟶ Q<GOAL>CategoryTheory.Sheaf.IsLocallyInjective ((CategoryTheory.presheafToSheaf J A).map φ) ↔ CategoryTheory.Presheaf.IsLocallyInjective J φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>CategoryTheory.HasWeakSheafify J A<VAR>J.WEqualsLocallyBijective A<VAR>P Q : CategoryTheory.Functor Cᵒᵖ A<VAR>φ : P ⟶ Q<GOAL>CategoryTheory.Sheaf.IsLocallySurjective ((CategoryTheory.presheafToSheaf J A).map φ) ↔ CategoryTheory.Presheaf.IsLocallySurjective J φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>U : C<VAR>s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))<VAR>V : C<VAR>i : V ⟶ U<GOAL>(CategoryTheory.Presheaf.imageSieve f s).arrows i = ∃ t, (f.app (Opposite.op V)) t = (G.map i.op) s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>U : C<VAR>s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))<GOAL>CategoryTheory.Presheaf.imageSieve f s = (CategoryTheory.GrothendieckTopology.imagePresheaf (CategoryTheory.whiskerRight f (CategoryTheory.forget A))).sieveOfSection s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>U : C<VAR>s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))<GOAL>CategoryTheory.Presheaf.imageSieve (CategoryTheory.whiskerRight f (CategoryTheory.forget A)) s = CategoryTheory.Presheaf.imageSieve f s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>U : C<VAR>s : (CategoryTheory.forget A).obj (F.obj (Opposite.op U))<GOAL>CategoryTheory.Presheaf.imageSieve f ((f.app (Opposite.op U)) s) = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>U : Cᵒᵖ<VAR>s : (CategoryTheory.forget A).obj (G.obj U)<VAR>V : C<VAR>g : V ⟶ Opposite.unop U<VAR>hg : (CategoryTheory.Presheaf.imageSieve f s).arrows g<GOAL>(f.app (Opposite.op V)) (CategoryTheory.Presheaf.localPreimage f s g hg) = (G.map g.op) s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>self : CategoryTheory.Presheaf.IsLocallySurjective J f<VAR>U : C<VAR>s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))<GOAL>CategoryTheory.Presheaf.imageSieve f s ∈ J.sieves U
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f<VAR>U : Cᵒᵖ<VAR>s : (CategoryTheory.forget A).obj (G.obj U)<GOAL>CategoryTheory.Presheaf.imageSieve f s ∈ J.sieves (Opposite.unop U)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J f ↔ CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf (CategoryTheory.whiskerRight f (CategoryTheory.forget A))) = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J f ↔ CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf f) = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J f ↔ CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.whiskerRight f (CategoryTheory.forget A))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(f.app U)<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>CategoryTheory.Presheaf.IsLocallySurjective J (f₁ ≫ f₂)<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>f₃ : F₁ ⟶ F₃<VAR>fac : f₁ ≫ f₂ = f₃<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f₃<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>f₃ : F₁ ⟶ F₃<VAR>fac : f₁ ≫ f₂ = f₃<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f₁<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J f₃ ↔ CategoryTheory.Presheaf.IsLocallySurjective J f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f₁<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J (f₁ ≫ f₂) ↔ CategoryTheory.Presheaf.IsLocallySurjective J f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>K : CategoryTheory.GrothendieckTopology C<VAR>hJK : J ≤ K<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>h : CategoryTheory.Presheaf.IsLocallySurjective J f<GOAL>CategoryTheory.Presheaf.IsLocallySurjective K f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>CategoryTheory.Presheaf.IsLocallyInjective J (f₁ ≫ f₂)<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f₁<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>f₃ : F₁ ⟶ F₃<VAR>fac : f₁ ≫ f₂ = f₃<VAR>CategoryTheory.Presheaf.IsLocallyInjective J f₃<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f₁<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>CategoryTheory.Presheaf.IsLocallySurjective J (f₁ ≫ f₂)<VAR>CategoryTheory.Presheaf.IsLocallyInjective J f₂<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J f₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>f₃ : F₁ ⟶ F₃<VAR>fac : f₁ ≫ f₂ = f₃<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f₃<VAR>CategoryTheory.Presheaf.IsLocallyInjective J f₂<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J f₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>CategoryTheory.Presheaf.IsLocallyInjective J f₁<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f₁<GOAL>CategoryTheory.Presheaf.IsLocallyInjective J (f₁ ≫ f₂) ↔ CategoryTheory.Presheaf.IsLocallyInjective J f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>CategoryTheory.Presheaf.IsLocallyInjective J f₂<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f₂<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J (f₁ ≫ f₂) ↔ CategoryTheory.Presheaf.IsLocallySurjective J f₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>F₁ F₂ : CategoryTheory.Sheaf J A<VAR>φ : F₁ ⟶ F₂<GOAL>CategoryTheory.Presheaf.IsLocallySurjective J ((CategoryTheory.sheafToPresheaf J A).map φ) ↔ CategoryTheory.Sheaf.IsLocallySurjective φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F G : CategoryTheory.Sheaf J (Type w)<VAR>f : F ⟶ G<GOAL>CategoryTheory.Sheaf.IsLocallySurjective f ↔ CategoryTheory.IsIso (CategoryTheory.GrothendieckTopology.imageSheafι f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F G : CategoryTheory.Sheaf J (Type w)<VAR>φ : F ⟶ G<VAR>CategoryTheory.HasSheafify J (Type w)<GOAL>CategoryTheory.Sheaf.IsLocallySurjective φ ↔ CategoryTheory.Epi φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>R R' : Cᵒᵖ ⥤ Type w<VAR>φ : R ⟶ R'<VAR>X : Cᵒᵖ<VAR>r' : R'.obj X<GOAL>((CategoryTheory.Presieve.FamilyOfElements.localPreimage φ r').map φ).IsAmalgamation r'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>self : R.regular<GOAL>∃ Y f, (R = CategoryTheory.Presieve.ofArrows (fun x => Y) fun x => f) ∧ CategoryTheory.EffectiveEpi f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>X B : C<VAR>π : X ⟶ B<VAR>c : CategoryTheory.Limits.PullbackCone π π<GOAL>CategoryTheory.CategoryStruct.comp (P.map π.op) (P.map c.fst.op) = CategoryTheory.CategoryStruct.comp (P.map π.op) (P.map c.snd.op)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>P P' : CategoryTheory.Functor Cᵒᵖ D<VAR>i : P ≅ P'<VAR>hP : CategoryTheory.regularTopology.EqualizerCondition P<GOAL>CategoryTheory.regularTopology.EqualizerCondition P'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : 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} E<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>F : CategoryTheory.Functor E C<VAR>{X B : E} → (π : X ⟶ B) → [inst : CategoryTheory.EffectiveEpi π] → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan π π) F<VAR>F.PreservesEffectiveEpis<VAR>hP : CategoryTheory.regularTopology.EqualizerCondition P<GOAL>CategoryTheory.regularTopology.EqualizerCondition (F.op.comp P)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type u_4)<VAR>hP : CategoryTheory.regularTopology.EqualizerCondition P<VAR>X B : C<VAR>π : X ⟶ B<VAR>CategoryTheory.EffectiveEpi π<VAR>CategoryTheory.Limits.HasPullback π π<GOAL>Function.Bijective (CategoryTheory.regularTopology.MapToEqualizer P π (CategoryTheory.Limits.pullback.fst π π) (CategoryTheory.Limits.pullback.snd π π) ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type u_4)<VAR>hP : ∀ (X B : C) (π : X ⟶ B) [inst : CategoryTheory.EffectiveEpi π] [inst : CategoryTheory.Limits.HasPullback π π], Function.Bijective (CategoryTheory.regularTopology.MapToEqualizer P π (CategoryTheory.Limits.pullback.fst π π) (CategoryTheory.Limits.pullback.snd π π) ⋯)<GOAL>CategoryTheory.regularTopology.EqualizerCondition P
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type u_4)<VAR>X B : C<VAR>π : X ⟶ B<VAR>CategoryTheory.Limits.HasPullback π π<GOAL>CategoryTheory.CategoryStruct.comp (P.map π.op) (P.map (CategoryTheory.Limits.pullback.fst π π).op) = CategoryTheory.CategoryStruct.comp (P.map π.op) (P.map (CategoryTheory.Limits.pullback.snd π π).op)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type u_4)<VAR>X B : C<VAR>π : X ⟶ B<VAR>CategoryTheory.Limits.HasPullback π π<GOAL>CategoryTheory.regularTopology.MapToEqualizer P π (CategoryTheory.Limits.pullback.fst π π) (CategoryTheory.Limits.pullback.snd π π) ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.lift (P.map π.op) ⋯) (CategoryTheory.Limits.Types.equalizerIso (P.map (CategoryTheory.Limits.pullback.fst π π).op) (P.map (CategoryTheory.Limits.pullback.snd π π).op)).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type u_4)<GOAL>CategoryTheory.regularTopology.EqualizerCondition P ↔ ∀ (X B : C) (π : X ⟶ B) [inst : CategoryTheory.EffectiveEpi π] [inst : CategoryTheory.Limits.HasPullback π π], CategoryTheory.IsIso (CategoryTheory.Limits.equalizer.lift (P.map π.op) ⋯)