C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ Presieve.IsSheafFor P S.arrows
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
⊢ Presieve.IsSheafFor P S.arrows
have : (bind R fun Y f _ => S.pullback f : Presieve X) ≤ S := by
  rintro Z f ⟨W, f, g, hg, hf : S _, rfl⟩
  apply hf
case hS
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ Presieve.IsSheafFor P (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows

case trans
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S)).arrows
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ Presieve.IsSheafFor P S.arrows
apply Presieve.isSheafFor_subsieve_aux P this
case hS
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows

case trans
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S)).arrows
case hS
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ Presieve.IsSheafFor P (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows

case trans
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S)).arrows
apply isSheafFor_bind _ _ _ hR hS
case intro.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
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
Z W : C
f : Z ⟶ W
g : W ⟶ X
hg : R.arrows g
hf : S.arrows (f ≫ g)
⊢ f ≫ g ∈ S.arrows
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
⊢ (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
rintro Z f ⟨W, f, g, hg, hf : S _, rfl⟩
no goals
case intro.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
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
Z W : C
f : Z ⟶ W
g : W ⟶ X
hg : R.arrows g
hf : S.arrows (f ≫ g)
⊢ f ≫ g ∈ S.arrows
apply hf
case hS
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows
case hS
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows
intro Y f hf Z g
case hS
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows
case hS
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows
dsimp
case hS
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSeparatedFor P (Sieve.pullback (g ≫ f) S).arrows
case hS
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows
rw [← pullback_comp]
no goals
case hS
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSeparatedFor P (Sieve.pullback (g ≫ f) S).arrows
apply (hS (R.downward_closed hf _)).isSeparatedFor
case trans
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S)).arrows
case trans
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S)).arrows
intro Y f hf
case trans
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this✝ : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this : Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S) = Sieve.pullback f R
⊢ Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
case trans
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this✝ : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this : Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S) = Sieve.pullback f R
⊢ Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S)).arrows
rw [this]
no goals
case trans
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this✝ : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this : Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S) = Sieve.pullback f R
⊢ Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
apply hR' hf
case h
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
⊢ ∀ (f_1 : Z ⟶ Y),
    (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows f_1 ↔
      (Sieve.pullback f R).arrows f_1
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S) = Sieve.pullback f R
ext Z
case h
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows g ↔ (Sieve.pullback f R).arrows g
case h
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
⊢ ∀ (f_1 : Z ⟶ Y),
    (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows f_1 ↔
      (Sieve.pullback f R).arrows f_1
intro g
case h.mp
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows g → (Sieve.pullback f R).arrows g

case h.mpr
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f R).arrows g → (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows g
case h
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows g ↔ (Sieve.pullback f R).arrows g
constructor
case h.mp.intro.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
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
W : C
k : Z ⟶ W
l : W ⟶ X
hl : R.arrows l
left✝ : ((fun T k x => Sieve.pullback k S) W l hl).arrows k
comm : k ≫ l = g ≫ f
⊢ (Sieve.pullback f R).arrows g
case h.mp
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows g → (Sieve.pullback f R).arrows g
rintro ⟨W, k, l, hl, _, comm⟩
case h.mp.intro.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
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
W : C
k : Z ⟶ W
l : W ⟶ X
hl : R.arrows l
left✝ : ((fun T k x => Sieve.pullback k S) W l hl).arrows k
comm : k ≫ l = g ≫ f
⊢ R.arrows (k ≫ l)
case h.mp.intro.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
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
W : C
k : Z ⟶ W
l : W ⟶ X
hl : R.arrows l
left✝ : ((fun T k x => Sieve.pullback k S) W l hl).arrows k
comm : k ≫ l = g ≫ f
⊢ (Sieve.pullback f R).arrows g
rw [pullback_apply, ← comm]
no goals
case h.mp.intro.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
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
W : C
k : Z ⟶ W
l : W ⟶ X
hl : R.arrows l
left✝ : ((fun T k x => Sieve.pullback k S) W l hl).arrows k
comm : k ≫ l = g ≫ f
⊢ R.arrows (k ≫ l)
simp [hl]
case h.mpr
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
a : (Sieve.pullback f R).arrows g
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows g
case h.mpr
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f R).arrows g → (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows g
intro a
case h.mpr
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
a : (Sieve.pullback f R).arrows g
⊢ (fun Y f h => ((fun T k x => Sieve.pullback k S) Y f h).arrows) Z (g ≫ f) a (𝟙 Z) ∧ 𝟙 Z ≫ g ≫ f = g ≫ f
case h.mpr
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
a : (Sieve.pullback f R).arrows g
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun T k x => Sieve.pullback k S)).arrows g
refine' ⟨Z, 𝟙 Z, _, a, _⟩
no goals
case h.mpr
C : Type u
inst✝ : Category C
P✝ : Cᵒᵖ ⥤ Type v
X Y✝ : C
S✝ : Sieve X
R✝ : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v
R S : Sieve X
hR : Presieve.IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
a : (Sieve.pullback f R).arrows g
⊢ (fun Y f h => ((fun T k x => Sieve.pullback k S) Y f h).arrows) Z (g ≫ f) a (𝟙 Z) ∧ 𝟙 Z ≫ g ≫ f = g ≫ f
simp [hf]