case mp
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ IsSheaf J P → IsSheaf' J P

case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ IsSheaf' J P → IsSheaf J P
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ IsSheaf J P ↔ IsSheaf' J P
constructor
case mp
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
case mp
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ IsSheaf J P → IsSheaf' J P
intro h U R hR
case mp
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
⊢ IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))
case mp
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
refine' ⟨_⟩
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
⊢ (X : Aᵒᵖ) →
    IsLimit
      ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
case mp
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
⊢ IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))
apply coyonedaJointlyReflectsLimits
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
X : Aᵒᵖ
⊢ IsLimit
    ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
⊢ (X : Aᵒᵖ) →
    IsLimit
      ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
intro X
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
X : Aᵒᵖ
q : Presieve.IsSheafFor (P ⋙ coyoneda.obj X) (generate R).arrows
⊢ IsLimit
    ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
X : Aᵒᵖ
⊢ IsLimit
    ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
have q : Presieve.IsSheafFor (P ⋙ coyoneda.obj X) _ := h X.unop _ hR
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
X : Aᵒᵖ
q : Presieve.IsSheafFor (P ⋙ coyoneda.obj X) R
⊢ IsLimit
    ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
X : Aᵒᵖ
q : Presieve.IsSheafFor (P ⋙ coyoneda.obj X) (generate R).arrows
⊢ IsLimit
    ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
rw [← Presieve.isSheafFor_iff_generate] at q
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
X : Aᵒᵖ
q :
  Nonempty
    (IsLimit
      (Fork.ofι (Equalizer.forkMap (P ⋙ coyoneda.obj X) R)
        (_ :
          Equalizer.forkMap (P ⋙ coyoneda.obj X) R ≫ Equalizer.Presieve.firstMap (P ⋙ coyoneda.obj X) R =
            Equalizer.forkMap (P ⋙ coyoneda.obj X) R ≫ Equalizer.Presieve.secondMap (P ⋙ coyoneda.obj X) R)))
⊢ IsLimit
    ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
X : Aᵒᵖ
q : Presieve.IsSheafFor (P ⋙ coyoneda.obj X) R
⊢ IsLimit
    ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
rw [Equalizer.Presieve.sheaf_condition] at q
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
X : Aᵒᵖ
q :
  IsLimit
    (Fork.ofι (Equalizer.forkMap (P ⋙ coyoneda.obj X) R)
      (_ :
        Equalizer.forkMap (P ⋙ coyoneda.obj X) R ≫ Equalizer.Presieve.firstMap (P ⋙ coyoneda.obj X) R =
          Equalizer.forkMap (P ⋙ coyoneda.obj X) R ≫ Equalizer.Presieve.secondMap (P ⋙ coyoneda.obj X) R))
⊢ IsLimit
    ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
X : Aᵒᵖ
q :
  Nonempty
    (IsLimit
      (Fork.ofι (Equalizer.forkMap (P ⋙ coyoneda.obj X) R)
        (_ :
          Equalizer.forkMap (P ⋙ coyoneda.obj X) R ≫ Equalizer.Presieve.firstMap (P ⋙ coyoneda.obj X) R =
            Equalizer.forkMap (P ⋙ coyoneda.obj X) R ≫ Equalizer.Presieve.secondMap (P ⋙ coyoneda.obj X) R)))
⊢ IsLimit
    ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
replace q := Classical.choice q
no goals
case mp.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf J P
U : C
R : Presieve U
hR : generate R ∈ GrothendieckTopology.sieves J U
X : Aᵒᵖ
q :
  IsLimit
    (Fork.ofι (Equalizer.forkMap (P ⋙ coyoneda.obj X) R)
      (_ :
        Equalizer.forkMap (P ⋙ coyoneda.obj X) R ≫ Equalizer.Presieve.firstMap (P ⋙ coyoneda.obj X) R =
          Equalizer.forkMap (P ⋙ coyoneda.obj X) R ≫ Equalizer.Presieve.secondMap (P ⋙ coyoneda.obj X) R))
⊢ IsLimit
    ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
apply (isSheafForIsSheafFor' _ _ _ _).symm q
case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ Presieve.IsSheafFor (P ⋙ coyoneda.obj U.op) S.arrows
case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ IsSheaf' J P → IsSheaf J P
intro h U X S hS
case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ Nonempty
    (IsLimit
      (Fork.ofι (Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows)
        (_ :
          Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows ≫
              Equalizer.Presieve.firstMap (P ⋙ coyoneda.obj U.op) S.arrows =
            Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows ≫
              Equalizer.Presieve.secondMap (P ⋙ coyoneda.obj U.op) S.arrows)))
case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ Presieve.IsSheafFor (P ⋙ coyoneda.obj U.op) S.arrows
rw [Equalizer.Presieve.sheaf_condition]
case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ IsLimit
    (Fork.ofι (Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows)
      (_ :
        Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows ≫
            Equalizer.Presieve.firstMap (P ⋙ coyoneda.obj U.op) S.arrows =
          Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows ≫
            Equalizer.Presieve.secondMap (P ⋙ coyoneda.obj U.op) S.arrows))
case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ Nonempty
    (IsLimit
      (Fork.ofι (Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows)
        (_ :
          Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows ≫
              Equalizer.Presieve.firstMap (P ⋙ coyoneda.obj U.op) S.arrows =
            Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows ≫
              Equalizer.Presieve.secondMap (P ⋙ coyoneda.obj U.op) S.arrows)))
refine' ⟨_⟩
case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ IsLimit
    ((coyoneda.obj U.op).mapCone
      (Fork.ofι (forkMap S.arrows P)
        (_ : forkMap S.arrows P ≫ firstMap S.arrows P = forkMap S.arrows P ≫ secondMap S.arrows P)))
case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ IsLimit
    (Fork.ofι (Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows)
      (_ :
        Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows ≫
            Equalizer.Presieve.firstMap (P ⋙ coyoneda.obj U.op) S.arrows =
          Equalizer.forkMap (P ⋙ coyoneda.obj U.op) S.arrows ≫
            Equalizer.Presieve.secondMap (P ⋙ coyoneda.obj U.op) S.arrows))
refine' isSheafForIsSheafFor' _ _ _ _ _
case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
this : PreservesLimitsOfSize (coyoneda.obj U.op) := preservesSmallestLimitsOfPreservesLimits (coyoneda.obj U.op)
⊢ IsLimit
    ((coyoneda.obj U.op).mapCone
      (Fork.ofι (forkMap S.arrows P)
        (_ : forkMap S.arrows P ≫ firstMap S.arrows P = forkMap S.arrows P ≫ secondMap S.arrows P)))
case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ IsLimit
    ((coyoneda.obj U.op).mapCone
      (Fork.ofι (forkMap S.arrows P)
        (_ : forkMap S.arrows P ≫ firstMap S.arrows P = forkMap S.arrows P ≫ secondMap S.arrows P)))
letI := preservesSmallestLimitsOfPreservesLimits (coyoneda.obj (op U))
case mpr.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
this : PreservesLimitsOfSize (coyoneda.obj U.op) := preservesSmallestLimitsOfPreservesLimits (coyoneda.obj U.op)
⊢ IsLimit
    (Fork.ofι (forkMap S.arrows P)
      (_ : forkMap S.arrows P ≫ firstMap S.arrows P = forkMap S.arrows P ≫ secondMap S.arrows P))
case mpr
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
this : PreservesLimitsOfSize (coyoneda.obj U.op) := preservesSmallestLimitsOfPreservesLimits (coyoneda.obj U.op)
⊢ IsLimit
    ((coyoneda.obj U.op).mapCone
      (Fork.ofι (forkMap S.arrows P)
        (_ : forkMap S.arrows P ≫ firstMap S.arrows P = forkMap S.arrows P ≫ secondMap S.arrows P)))
apply isLimitOfPreserves
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
this : PreservesLimitsOfSize (coyoneda.obj U.op) := preservesSmallestLimitsOfPreservesLimits (coyoneda.obj U.op)
⊢ generate S.arrows ∈ GrothendieckTopology.sieves J X
case mpr.t
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
this : PreservesLimitsOfSize (coyoneda.obj U.op) := preservesSmallestLimitsOfPreservesLimits (coyoneda.obj U.op)
⊢ IsLimit
    (Fork.ofι (forkMap S.arrows P)
      (_ : forkMap S.arrows P ≫ firstMap S.arrows P = forkMap S.arrows P ≫ secondMap S.arrows P))
apply Classical.choice (h _ S.arrows _)
no goals
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U✝ : C
R : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
h : IsSheaf' J P
U : A
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
this : PreservesLimitsOfSize (coyoneda.obj U.op) := preservesSmallestLimitsOfPreservesLimits (coyoneda.obj U.op)
⊢ generate S.arrows ∈ GrothendieckTopology.sieves J X
simpa