case h.h.h
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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ X
hf : R f
⊢ FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) (FamilyOfElements.sieveExtend x) f hf = x f hf
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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
⊢ FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) (FamilyOfElements.sieveExtend x) = x
funext Y f hf
no goals
case h.h.h
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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ X
hf : R f
⊢ FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) (FamilyOfElements.sieveExtend x) f hf = x f hf
exact extend_agrees t hf