case w.h.h.mk
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F'
l₁ l₂ : toPresheaf (sheafify J G) ⟶ F'
e : homOfLe (_ : G ≤ sheafify J G) ≫ l₁ = homOfLe (_ : G ≤ sheafify J G) ≫ l₂
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ l₁.app U { val := s, property := hs } = l₂.app U { val := s, property := hs }
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F'
l₁ l₂ : toPresheaf (sheafify J G) ⟶ F'
e : homOfLe (_ : G ≤ sheafify J G) ≫ l₁ = homOfLe (_ : G ≤ sheafify J G) ≫ l₂
⊢ l₁ = l₂
ext (U⟨s, hs⟩)
case w.h.h.mk
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F'
l₁ l₂ : toPresheaf (sheafify J G) ⟶ F'
e : homOfLe (_ : G ≤ sheafify J G) ≫ l₁ = homOfLe (_ : G ≤ sheafify J G) ≫ l₂
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ U.unop⦄,
    (sieveOfSection G s).arrows f →
      F'.map f.op (l₁.app U { val := s, property := hs }) = F'.map f.op (l₂.app U { val := s, property := hs })
case w.h.h.mk
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F'
l₁ l₂ : toPresheaf (sheafify J G) ⟶ F'
e : homOfLe (_ : G ≤ sheafify J G) ≫ l₁ = homOfLe (_ : G ≤ sheafify J G) ≫ l₂
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ l₁.app U { val := s, property := hs } = l₂.app U { val := s, property := hs }
apply (h _ hs).isSeparatedFor.ext
case w.h.h.mk
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F'
l₁ l₂ : toPresheaf (sheafify J G) ⟶ F'
e : homOfLe (_ : G ≤ sheafify J G) ≫ l₁ = homOfLe (_ : G ≤ sheafify J G) ≫ l₂
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : (sieveOfSection G s).arrows i
⊢ F'.map i.op (l₁.app U { val := s, property := hs }) = F'.map i.op (l₂.app U { val := s, property := hs })
case w.h.h.mk
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F'
l₁ l₂ : toPresheaf (sheafify J G) ⟶ F'
e : homOfLe (_ : G ≤ sheafify J G) ≫ l₁ = homOfLe (_ : G ≤ sheafify J G) ≫ l₂
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ U.unop⦄,
    (sieveOfSection G s).arrows f →
      F'.map f.op (l₁.app U { val := s, property := hs }) = F'.map f.op (l₂.app U { val := s, property := hs })
rintro V i hi
case w.h.h.mk
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F'
l₁ l₂ : toPresheaf (sheafify J G) ⟶ F'
e : homOfLe (_ : G ≤ sheafify J G) ≫ l₁ = homOfLe (_ : G ≤ sheafify J G) ≫ l₂
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : F.map i.op s ∈ obj G V.op
⊢ F'.map i.op (l₁.app U { val := s, property := hs }) = F'.map i.op (l₂.app U { val := s, property := hs })
case w.h.h.mk
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F'
l₁ l₂ : toPresheaf (sheafify J G) ⟶ F'
e : homOfLe (_ : G ≤ sheafify J G) ≫ l₁ = homOfLe (_ : G ≤ sheafify J G) ≫ l₂
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : (sieveOfSection G s).arrows i
⊢ F'.map i.op (l₁.app U { val := s, property := hs }) = F'.map i.op (l₂.app U { val := s, property := hs })
dsimp at hi
case w.h.h.mk
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F'
l₁ l₂ : toPresheaf (sheafify J G) ⟶ F'
e : homOfLe (_ : G ≤ sheafify J G) ≫ l₁ = homOfLe (_ : G ≤ sheafify J G) ≫ l₂
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : F.map i.op s ∈ obj G V.op
⊢ l₁.app V.op ((toPresheaf (sheafify J G)).map i.op { val := s, property := hs }) =
    l₂.app V.op ((toPresheaf (sheafify J G)).map i.op { val := s, property := hs })
case w.h.h.mk
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F'
l₁ l₂ : toPresheaf (sheafify J G) ⟶ F'
e : homOfLe (_ : G ≤ sheafify J G) ≫ l₁ = homOfLe (_ : G ≤ sheafify J G) ≫ l₂
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : F.map i.op s ∈ obj G V.op
⊢ F'.map i.op (l₁.app U { val := s, property := hs }) = F'.map i.op (l₂.app U { val := s, property := hs })
erw [← FunctorToTypes.naturality, ← FunctorToTypes.naturality]
no goals
case w.h.h.mk
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F'
l₁ l₂ : toPresheaf (sheafify J G) ⟶ F'
e : homOfLe (_ : G ≤ sheafify J G) ≫ l₁ = homOfLe (_ : G ≤ sheafify J G) ≫ l₂
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : F.map i.op s ∈ obj G V.op
⊢ l₁.app V.op ((toPresheaf (sheafify J G)).map i.op { val := s, property := hs }) =
    l₂.app V.op ((toPresheaf (sheafify J G)).map i.op { val := s, property := hs })
exact (congr_fun (congr_app e <| op V) ⟨_, hi⟩ : _)