C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))) ↔
    IsSheafOpensLeCover F
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ IsSheaf F ↔ IsSheafOpensLeCover F
refine' (Presheaf.isSheaf_iff_isLimit _ _).trans _
case mp
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))) →
    IsSheafOpensLeCover F

case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ IsSheafOpensLeCover F →
    ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))) ↔
    IsSheafOpensLeCover F
constructor
case mp
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (opensLeCoverCocone U))))
case mp
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ (∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))) →
    IsSheafOpensLeCover F
intro h ι U
case mp
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty
    (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U (iSup U))).arrows))))
case mp
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (opensLeCoverCocone U))))
rw [(isLimitOpensLeEquivGenerate₁ F U rfl).nonempty_congr]
case mp.a
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Sieve.generate (presieveOfCoveringAux U (iSup U)) ∈
    GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) (iSup U)
case mp
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty
    (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate (presieveOfCoveringAux U (iSup U))).arrows))))
apply h
no goals
case mp.a
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι✝ : Type w
U✝ : ι✝ → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U✝
h :
  ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
      Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
ι : Type w
U : ι → Opens ↑X
⊢ Sieve.generate (presieveOfCoveringAux U (iSup U)) ∈
    GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) (iSup U)
apply presieveOfCovering.mem_grothendieckTopology
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
⊢ S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y →
    Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ IsSheafOpensLeCover F →
    ∀ ⦃X_1 : Opens ↑X⦄ (S : Sieve X_1),
      S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) X_1 →
        Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
intro h Y S
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
⊢ Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y →
    Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate S.arrows).arrows))))
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
⊢ S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y →
    Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone S.arrows))))
rw [← Sieve.generate_sieve S]
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate S.arrows).arrows))))
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
⊢ Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y →
    Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate S.arrows).arrows))))
intro hS
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (opensLeCoverCocone (coveringOfPresieve Y S.arrows)))))
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (Presieve.cocone (Sieve.generate S.arrows).arrows))))
rw [← (isLimitOpensLeEquivGenerate₂ F S.1 hS).nonempty_congr]
no goals
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
ι : Type w
U : ι → Opens ↑X
Y✝ : Opens ↑X
hY : Y✝ = iSup U
h : IsSheafOpensLeCover F
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (opensLeCoverCocone (coveringOfPresieve Y S.arrows)))))
apply h