case intro.mk.intro.intro.intro.intro
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X✝ Y : C
S✝ : Sieve X✝
R : Presieve X✝
J✝ J₂ : GrothendieckTopology C
Ps : Set (Cᵒᵖ ⥤ Type v)
J : GrothendieckTopology C
hJ : ∀ (P : Cᵒᵖ ⥤ Type v), P ∈ Ps → Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
P : Cᵒᵖ ⥤ Type v
hP : P ∈ Ps
⊢ S ∈
    (fun f => ↑f X)
      { val := (finestTopologySingle P).sieves,
        property := (_ : ∃ a, a ∈ finestTopologySingle '' Ps ∧ a.sieves = (finestTopologySingle P).sieves) }
C : Type u
inst✝ : Category C
P : Cᵒᵖ ⥤ Type v
X Y : C
S : Sieve X
R : Presieve X
J✝ J₂ : GrothendieckTopology C
Ps : Set (Cᵒᵖ ⥤ Type v)
J : GrothendieckTopology C
hJ : ∀ (P : Cᵒᵖ ⥤ Type v), P ∈ Ps → Presieve.IsSheaf J P
⊢ J ≤ finestTopology Ps
rintro X S hS _ ⟨⟨_, _, ⟨P, hP, rfl⟩, rfl⟩, rfl⟩
case intro.mk.intro.intro.intro.intro
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X✝ Y✝ : C
S✝ : Sieve X✝
R : Presieve X✝
J✝ J₂ : GrothendieckTopology C
Ps : Set (Cᵒᵖ ⥤ Type v)
J : GrothendieckTopology C
hJ : ∀ (P : Cᵒᵖ ⥤ Type v), P ∈ Ps → Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
P : Cᵒᵖ ⥤ Type v
hP : P ∈ Ps
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f S).arrows
case intro.mk.intro.intro.intro.intro
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X✝ Y : C
S✝ : Sieve X✝
R : Presieve X✝
J✝ J₂ : GrothendieckTopology C
Ps : Set (Cᵒᵖ ⥤ Type v)
J : GrothendieckTopology C
hJ : ∀ (P : Cᵒᵖ ⥤ Type v), P ∈ Ps → Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
P : Cᵒᵖ ⥤ Type v
hP : P ∈ Ps
⊢ S ∈
    (fun f => ↑f X)
      { val := (finestTopologySingle P).sieves,
        property := (_ : ∃ a, a ∈ finestTopologySingle '' Ps ∧ a.sieves = (finestTopologySingle P).sieves) }
intro Y f
no goals
case intro.mk.intro.intro.intro.intro
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X✝ Y✝ : C
S✝ : Sieve X✝
R : Presieve X✝
J✝ J₂ : GrothendieckTopology C
Ps : Set (Cᵒᵖ ⥤ Type v)
J : GrothendieckTopology C
hJ : ∀ (P : Cᵒᵖ ⥤ Type v), P ∈ Ps → Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
P : Cᵒᵖ ⥤ Type v
hP : P ∈ Ps
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f S).arrows
exact hJ P hP (S.pullback f) (J.pullback_stable f hS)