C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S E.pt))
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ Presheaf.IsSheaf J E.pt
rw [Presheaf.isSheaf_iff_multifork]
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
S : GrothendieckTopology.Cover J X
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S E.pt))
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S E.pt))
intro X S
no goals
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
K : Type z
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
S : GrothendieckTopology.Cover J X
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S E.pt))
exact ⟨isLimitMultiforkOfIsLimit _ _ hE _ _⟩