C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (generate (singleton (𝟙 X))).arrows
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P ⊤.arrows
rw [← generate_of_singleton_isSplitEpi (𝟙 X)]
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (generate (singleton (𝟙 X))).arrows
rw [← isSheafFor_iff_generate]
no goals
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))
apply isSheafFor_singleton_iso