ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>G.IsLocallyFaithful K<VAR>Hp : CategoryTheory.CoverPreserving J K G<GOAL>G.IsContinuous J K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_7, u_4} A<VAR>P Q : CategoryTheory.Functor Dᵒᵖ A<VAR>hQ : CategoryTheory.Presheaf.IsSheaf K Q<GOAL>Function.Bijective ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>self : CategoryTheory.Functor.IsDenseSubsite J K G<GOAL>G.IsCoverDense K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>self : CategoryTheory.Functor.IsDenseSubsite J K G<GOAL>G.IsLocallyFull K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>self : CategoryTheory.Functor.IsDenseSubsite J K G<GOAL>G.IsLocallyFaithful K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>self : CategoryTheory.Functor.IsDenseSubsite J K G<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.functorPushforward G S ∈ K.sieves (G.obj X) ↔ S ∈ J.sieves X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>CategoryTheory.Functor.IsDenseSubsite J K G<GOAL>G.IsCoverDense K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>CategoryTheory.Functor.IsDenseSubsite J K G<GOAL>G.IsLocallyFull K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>CategoryTheory.Functor.IsDenseSubsite J K G<GOAL>G.IsLocallyFaithful K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>CategoryTheory.Functor.IsDenseSubsite J K G<GOAL>CategoryTheory.CoverPreserving J K G
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>CategoryTheory.Functor.IsDenseSubsite J K G<VAR>U V : C<VAR>f : G.obj U ⟶ G.obj V<GOAL>G.imageSieve f ∈ J.sieves U
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>CategoryTheory.Functor.IsDenseSubsite J K G<VAR>U V : C<VAR>f₁ f₂ : U ⟶ V<VAR>e : G.map f₁ = G.map f₂<GOAL>CategoryTheory.Sieve.equalizer f₁ f₂ ∈ J.sieves U
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A<VAR>CategoryTheory.Functor.IsDenseSubsite J K G<VAR>Y : CategoryTheory.Sheaf J A<VAR>U : C<VAR>X : A<GOAL>CategoryTheory.IsIso ((CategoryTheory.yoneda.map ((G.op.ranCounit.app Y.val).app (Opposite.op U))).app (Opposite.op X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A<VAR>CategoryTheory.Functor.IsDenseSubsite J K G<GOAL>(CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K A).functor = G.sheafPushforwardCocontinuous A J K
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A<VAR>CategoryTheory.Functor.IsDenseSubsite J K G<GOAL>(CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K A).inverse = G.sheafPushforwardContinuous A J K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>J : Type u<VAR>LinearOrder J<VAR>j : J<VAR>F : CategoryTheory.Functor { i // i ≤ j } C<VAR>i : J<VAR>hi : i ≤ j<VAR>k : J<VAR>hk : k < i<GOAL>(CategoryTheory.Functor.Iteration.restrictionLT F hi).obj ⟨k, hk⟩ = F.obj ⟨k, ⋯⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>J : Type u<VAR>LinearOrder J<VAR>j : J<VAR>F : CategoryTheory.Functor { i // i ≤ j } C<VAR>i : J<VAR>hi : i ≤ j<VAR>k₁ k₂ : { k // k < i }<VAR>φ : k₁ ⟶ k₂<GOAL>(CategoryTheory.Functor.Iteration.restrictionLT F hi).map φ = F.map (CategoryTheory.homOfLE ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>J : Type u<VAR>LinearOrder J<VAR>j : J<VAR>F : CategoryTheory.Functor { i // i ≤ j } C<VAR>i : J<VAR>hi : i ≤ j<GOAL>∀ (x : { k // k < i }), (CategoryTheory.Functor.Iteration.coconeOfLE F hi).ι.app x = match x with | ⟨k, hk⟩ => F.map (CategoryTheory.homOfLE ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>J : Type u<VAR>LinearOrder J<VAR>j : J<VAR>F : CategoryTheory.Functor { i // i ≤ j } C<VAR>i : J<VAR>hi : i ≤ j<GOAL>(CategoryTheory.Functor.Iteration.coconeOfLE F hi).pt = F.obj ⟨i, hi⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>Φ : CategoryTheory.Functor C C<VAR>ε : CategoryTheory.Functor.id C ⟶ Φ<VAR>J : Type u<VAR>LinearOrder J<VAR>IsWellOrder J fun x x_1 => x < x_1<VAR>OrderBot J<VAR>j : J<VAR>self : CategoryTheory.Functor.Iteration ε j<VAR>i : J<VAR>hi : i < j<GOAL>CategoryTheory.Functor.Iteration.mapSucc' self.F i hi = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (self.F.obj ⟨i, ⋯⟩) ε) (self.isoSucc i hi).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>Φ : CategoryTheory.Functor C C<VAR>ε : CategoryTheory.Functor.id C ⟶ Φ<VAR>J : Type u<VAR>LinearOrder J<VAR>IsWellOrder J fun x x_1 => x < x_1<VAR>OrderBot J<VAR>j : J<VAR>iter : CategoryTheory.Functor.Iteration ε j<VAR>i : J<VAR>hi : i < j<GOAL>iter.mapSucc i hi = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (iter.F.obj ⟨i, ⋯⟩) ε) (iter.isoSucc i hi).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>Φ : CategoryTheory.Functor C C<VAR>ε : CategoryTheory.Functor.id C ⟶ Φ<VAR>J : Type u<VAR>LinearOrder J<VAR>IsWellOrder J fun x x_1 => x < x_1<VAR>OrderBot J<VAR>j : J<VAR>iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j<VAR>self : iter₁.Hom iter₂<VAR>i : J<VAR>hi : i < j<GOAL>self.natTrans.app ⟨wellOrderSucc i, ⋯⟩ = CategoryTheory.CategoryStruct.comp (iter₁.isoSucc i hi).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (self.natTrans.app ⟨i, ⋯⟩) Φ) (iter₂.isoSucc i hi).inv)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>Φ : CategoryTheory.Functor C C<VAR>ε : CategoryTheory.Functor.id C ⟶ Φ<VAR>J : Type u<VAR>LinearOrder J<VAR>IsWellOrder J fun x x_1 => x < x_1<VAR>OrderBot J<VAR>j : J<VAR>iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j<VAR>self : iter₁.Hom iter₂<GOAL>self.natTrans.app ⟨⊥, ⋯⟩ = CategoryTheory.CategoryStruct.comp iter₁.isoZero.hom iter₂.isoZero.inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>Φ : CategoryTheory.Functor C C<VAR>ε : CategoryTheory.Functor.id C ⟶ Φ<VAR>J : Type u<VAR>LinearOrder J<VAR>IsWellOrder J fun x x_1 => x < x_1<VAR>OrderBot J<VAR>j : J<VAR>iter₁ : CategoryTheory.Functor.Iteration ε j<GOAL>(CategoryTheory.Functor.Iteration.Hom.id iter₁).natTrans = CategoryTheory.CategoryStruct.id iter₁.F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>Φ : CategoryTheory.Functor C C<VAR>ε : CategoryTheory.Functor.id C ⟶ Φ<VAR>J : Type u<VAR>LinearOrder J<VAR>IsWellOrder J fun x x_1 => x < x_1<VAR>OrderBot J<VAR>j : J<VAR>iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j<VAR>f g : iter₁.Hom iter₂<VAR>h : f.natTrans = g.natTrans<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>Φ : CategoryTheory.Functor C C<VAR>ε : CategoryTheory.Functor.id C ⟶ Φ<VAR>J : Type u<VAR>LinearOrder J<VAR>IsWellOrder J fun x x_1 => x < x_1<VAR>OrderBot J<VAR>j : J<VAR>iter₁ iter₂ iter₃ : CategoryTheory.Functor.Iteration ε j<VAR>f : iter₁.Hom iter₂<VAR>g : iter₂.Hom iter₃<GOAL>(f.comp g).natTrans = CategoryTheory.CategoryStruct.comp f.natTrans g.natTrans
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>P : C<GOAL>CategoryTheory.Projective P ↔ (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op P)).PreservesEpimorphisms
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : C<GOAL>CategoryTheory.Injective J ↔ (CategoryTheory.preadditiveYoneda.obj J).PreservesEpimorphisms
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>J : C<GOAL>CategoryTheory.Injective J ↔ (CategoryTheory.preadditiveYonedaObj J).PreservesEpimorphisms
<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>∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>X : C<VAR>K : Type (max v u)<VAR>CategoryTheory.SmallCategory K<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>W : J.Cover X<VAR>i : W.Arrow<VAR>E : CategoryTheory.Limits.Cone (F ⋙ J.diagramFunctor D X ⋙ (CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W))<GOAL>(CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation i E).pt = E.pt
<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>∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>X : C<VAR>K : Type (max v u)<VAR>CategoryTheory.SmallCategory K<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>W : J.Cover X<VAR>i : W.Arrow<VAR>E : CategoryTheory.Limits.Cone (F ⋙ J.diagramFunctor D X ⋙ (CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W))<VAR>k : K<GOAL>(CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation i E).π.app k = E.π.app k ≫ CategoryTheory.Limits.Multiequalizer.ι (W.index (F.obj k)) i
<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>∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>CategoryTheory.ConcreteCategory D<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>K : Type (max v u)<VAR>CategoryTheory.SmallCategory K<VAR>CategoryTheory.FinCategory K<VAR>CategoryTheory.Limits.HasLimitsOfShape K D<VAR>CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.forget D)<VAR>CategoryTheory.Limits.ReflectsLimitsOfShape K (CategoryTheory.forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : CategoryTheory.Limits.Cone (F ⋙ J.plusFunctor D ⋙ (CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X))<VAR>k : K<GOAL>CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj F X S ≫ (J.plusMap (CategoryTheory.Limits.limit.π F k)).app (Opposite.op X) = S.π.app k
<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>∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>CategoryTheory.ConcreteCategory D<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<GOAL>J.toSheafify P ≫ (CategoryTheory.plusPlusIsoSheafify J D P).hom = CategoryTheory.toSheafify J P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>U : CategoryTheory.Sieve X<VAR>B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → CategoryTheory.Sieve Y<VAR>hU : CategoryTheory.Presieve.IsSheafFor P U.arrows<VAR>hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), CategoryTheory.Presieve.IsSheafFor P (B hf).arrows<VAR>hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback g (B h)).arrows<GOAL>CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.bind U.arrows B).arrows
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>R S : CategoryTheory.Sieve X<VAR>hR : CategoryTheory.Presieve.IsSheafFor P R.arrows<VAR>hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f R).arrows<VAR>hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows<GOAL>CategoryTheory.Presieve.IsSheafFor P S.arrows
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type v))<VAR>h : P ∈ Ps<GOAL>CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.finestTopology Ps) P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type v))<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>hJ : ∀ P ∈ Ps, CategoryTheory.Presieve.IsSheaf J P<GOAL>J ≤ CategoryTheory.Sheaf.finestTopology Ps
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.canonicalTopology C) (CategoryTheory.yoneda.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P.Representable<GOAL>CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.canonicalTopology C) P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>h : ∀ (X : C), CategoryTheory.Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)<GOAL>CategoryTheory.Sheaf.Subcanonical J
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>hJ : CategoryTheory.Sheaf.Subcanonical J<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P.Representable<GOAL>CategoryTheory.Presieve.IsSheaf J P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>hJ : CategoryTheory.Sheaf.Subcanonical J<GOAL>∀ {X Y : C} (f : X ⟶ Y), (hJ.yoneda.map f).val = CategoryTheory.yoneda.map f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>hJ : CategoryTheory.Sheaf.Subcanonical J<VAR>X : C<GOAL>(hJ.yoneda.obj X).val = CategoryTheory.yoneda.obj X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} A<VAR>CategoryTheory.HasWeakSheafify J A<VAR>(CategoryTheory.constantSheaf J A).Faithful<VAR>(CategoryTheory.constantSheaf J A).Full<VAR>t : C<VAR>ht : CategoryTheory.Limits.IsTerminal t<VAR>F : CategoryTheory.Sheaf J A<VAR>X : A<VAR>i : F ≅ (CategoryTheory.constantSheaf J A).obj X<GOAL>CategoryTheory.Sheaf.IsDiscrete J ht F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} A<VAR>CategoryTheory.HasWeakSheafify J A<VAR>(CategoryTheory.constantSheaf J A).Faithful<VAR>(CategoryTheory.constantSheaf J A).Full<VAR>t : C<VAR>ht : CategoryTheory.Limits.IsTerminal t<VAR>F : CategoryTheory.Sheaf J A<GOAL>CategoryTheory.Sheaf.IsDiscrete J ht F ↔ F ∈ (CategoryTheory.constantSheaf J A).essImage
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} A<VAR>CategoryTheory.HasWeakSheafify J A<VAR>(CategoryTheory.constantSheaf J A).Faithful<VAR>(CategoryTheory.constantSheaf J A).Full<VAR>t : C<VAR>ht : CategoryTheory.Limits.IsTerminal t<VAR>L : A ⥤ CategoryTheory.Sheaf J A<VAR>adj : L ⊣ (CategoryTheory.sheafSections J A).obj (Opposite.op t)<VAR>F : CategoryTheory.Sheaf J A<GOAL>CategoryTheory.Sheaf.IsDiscrete J ht F ↔ F ∈ L.essImage
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} A<VAR>CategoryTheory.HasWeakSheafify J A<VAR>(CategoryTheory.constantSheaf J A).Faithful<VAR>(CategoryTheory.constantSheaf J A).Full<VAR>t : C<VAR>ht : CategoryTheory.Limits.IsTerminal t<VAR>L : A ⥤ CategoryTheory.Sheaf J A<VAR>adj : L ⊣ (CategoryTheory.sheafSections J A).obj (Opposite.op t)<VAR>F : CategoryTheory.Sheaf J A<GOAL>CategoryTheory.Sheaf.IsDiscrete J ht F ↔ CategoryTheory.IsIso (adj.counit.app F)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>CategoryTheory.HasWeakSheafify J A<VAR>t : C<VAR>ht : CategoryTheory.Limits.IsTerminal t<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>CategoryTheory.HasWeakSheafify K A<VAR>G : C ⥤ D<VAR>∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A<VAR>CategoryTheory.Functor.IsDenseSubsite J K G<VAR>ht' : CategoryTheory.Limits.IsTerminal (G.obj t)<VAR>(CategoryTheory.constantSheaf J A).Faithful<VAR>(CategoryTheory.constantSheaf J A).Full<VAR>F : CategoryTheory.Sheaf K A<GOAL>let e := CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K A;
CategoryTheory.Sheaf.IsDiscrete J ht (e.inverse.obj F) ↔ CategoryTheory.Sheaf.IsDiscrete K ht' F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>B : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify J B<VAR>J.PreservesSheafification U<VAR>J.HasSheafCompose U<VAR>X : A<GOAL>∀ (X_1 : Cᵒᵖ), ((CategoryTheory.Sheaf.constantCommuteCompose J U).inv.app X).val.app X_1 = ((CategoryTheory.presheafToSheaf J B).map ((CategoryTheory.Functor.compConstIso Cᵒᵖ U).hom.app X)).val.app X_1 ≫ ((CategoryTheory.sheafComposeNatIso J U (CategoryTheory.sheafificationAdjunction J A) (CategoryTheory.sheafificationAdjunction J B)).hom.app ((CategoryTheory.Functor.const Cᵒᵖ).obj X)).val.app X_1
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>B : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify J B<VAR>J.PreservesSheafification U<VAR>J.HasSheafCompose U<VAR>X : A<GOAL>∀ (X_1 : Cᵒᵖ), ((CategoryTheory.Sheaf.constantCommuteCompose J U).hom.app X).val.app X_1 = ((CategoryTheory.sheafComposeNatIso J U (CategoryTheory.sheafificationAdjunction J A) (CategoryTheory.sheafificationAdjunction J B)).inv.app ((CategoryTheory.Functor.const Cᵒᵖ).obj X)).val.app X_1 ≫ ((CategoryTheory.presheafToSheaf J B).map ((CategoryTheory.Functor.compConstIso Cᵒᵖ U).inv.app X)).val.app X_1
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>B : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify J B<VAR>J.PreservesSheafification U<VAR>J.HasSheafCompose U<VAR>P : CategoryTheory.Sheaf J A<GOAL>(CategoryTheory.sheafComposeNatIso J U (CategoryTheory.sheafificationAdjunction J A) (CategoryTheory.sheafificationAdjunction J B)).hom.app ((CategoryTheory.sheafToPresheaf J A).obj P) ≫ (CategoryTheory.sheafCompose J U).map ((CategoryTheory.sheafificationAdjunction J A).counit.app P) = (CategoryTheory.sheafificationAdjunction J B).counit.app ((CategoryTheory.sheafCompose J U).obj P)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>t : C<VAR>ht : CategoryTheory.Limits.IsTerminal t<VAR>B : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify J B<VAR>J.PreservesSheafification U<VAR>J.HasSheafCompose U<VAR>F : CategoryTheory.Sheaf J A<GOAL>((CategoryTheory.Sheaf.constantCommuteCompose J U).app (F.val.obj (Opposite.op t))).hom ≫ (CategoryTheory.constantSheafAdj J B ht).counit.app ((CategoryTheory.sheafCompose J U).obj F) = (CategoryTheory.sheafCompose J U).map ((CategoryTheory.constantSheafAdj J A ht).counit.app F)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>t : C<VAR>ht : CategoryTheory.Limits.IsTerminal t<VAR>B : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify J B<VAR>J.PreservesSheafification U<VAR>J.HasSheafCompose U<VAR>F : CategoryTheory.Sheaf J A<GOAL>(CategoryTheory.sheafifyComposeIso J U ((CategoryTheory.Functor.const Cᵒᵖ).obj (F.val.obj (Opposite.op t)))).hom ≫ ((CategoryTheory.sheafCompose J U).map ((CategoryTheory.constantSheafAdj J A ht).counit.app F)).val = ((CategoryTheory.presheafToSheaf J B ⋙ CategoryTheory.sheafToPresheaf J B).mapIso (CategoryTheory.Functor.constComp Cᵒᵖ (F.val.obj (Opposite.op t)) U)).hom ≫ ((CategoryTheory.constantSheafAdj J B ht).counit.app ((CategoryTheory.sheafCompose J U).obj F)).val