[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U V : Cᵒᵖ
x✝¹ : U ⟶ V
x : F.obj U
x✝ : x ∈ (fun U => ⊤) U
⊢ x ∈ F.map x✝¹ ⁻¹' (fun U => ⊤) V
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
X : Cᵒᵖ
⊢ { obj := fun U => ↑(obj G U),
          map := fun U V i x => { val := F.map i ↑x, property := (_ : ↑x ∈ F.map i ⁻¹' obj G V) } }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun U => ↑(obj G U),
            map := fun U V i x => { val := F.map i ↑x, property := (_ : ↑x ∈ F.map i ⁻¹' obj G V) } }.obj
        X)
[PROOFSTEP]
ext ⟨x, _⟩
[GOAL]
case h.mk
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
X : Cᵒᵖ
x : F.obj X
property✝ : x ∈ obj G X
⊢ { obj := fun U => ↑(obj G U),
          map := fun U V i x => { val := F.map i ↑x, property := (_ : ↑x ∈ F.map i ⁻¹' obj G V) } }.map
      (𝟙 X) { val := x, property := property✝ } =
    𝟙
      ({ obj := fun U => ↑(obj G U),
            map := fun U V i x => { val := F.map i ↑x, property := (_ : ↑x ∈ F.map i ⁻¹' obj G V) } }.obj
        X)
      { val := x, property := property✝ }
[PROOFSTEP]
dsimp
[GOAL]
case h.mk
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
X : Cᵒᵖ
x : F.obj X
property✝ : x ∈ obj G X
⊢ { val := F.map (𝟙 X) x, property := (_ : x ∈ F.map (𝟙 X) ⁻¹' obj G X) } = { val := x, property := property✝ }
[PROOFSTEP]
simp only [FunctorToTypes.map_id_apply]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
X Y Z : Cᵒᵖ
i : X ⟶ Y
j : Y ⟶ Z
⊢ { obj := fun U => ↑(obj G U),
          map := fun U V i x => { val := F.map i ↑x, property := (_ : ↑x ∈ F.map i ⁻¹' obj G V) } }.map
      (i ≫ j) =
    { obj := fun U => ↑(obj G U),
            map := fun U V i x => { val := F.map i ↑x, property := (_ : ↑x ∈ F.map i ⁻¹' obj G V) } }.map
        i ≫
      { obj := fun U => ↑(obj G U),
            map := fun U V i x => { val := F.map i ↑x, property := (_ : ↑x ∈ F.map i ⁻¹' obj G V) } }.map
        j
[PROOFSTEP]
ext ⟨x, _⟩
[GOAL]
case h.mk
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
X Y Z : Cᵒᵖ
i : X ⟶ Y
j : Y ⟶ Z
x : F.obj X
property✝ : x ∈ obj G X
⊢ { obj := fun U => ↑(obj G U),
          map := fun U V i x => { val := F.map i ↑x, property := (_ : ↑x ∈ F.map i ⁻¹' obj G V) } }.map
      (i ≫ j) { val := x, property := property✝ } =
    ({ obj := fun U => ↑(obj G U),
              map := fun U V i x => { val := F.map i ↑x, property := (_ : ↑x ∈ F.map i ⁻¹' obj G V) } }.map
          i ≫
        { obj := fun U => ↑(obj G U),
              map := fun U V i x => { val := F.map i ↑x, property := (_ : ↑x ∈ F.map i ⁻¹' obj G V) } }.map
          j)
      { val := x, property := property✝ }
[PROOFSTEP]
dsimp
[GOAL]
case h.mk
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
X Y Z : Cᵒᵖ
i : X ⟶ Y
j : Y ⟶ Z
x : F.obj X
property✝ : x ∈ obj G X
⊢ { val := F.map (i ≫ j) x, property := (_ : x ∈ F.map (i ≫ j) ⁻¹' obj G Z) } =
    { val := F.map j (F.map i x), property := (_ : F.map i x ∈ F.map j ⁻¹' obj G Z) }
[PROOFSTEP]
simp only [FunctorToTypes.map_comp_apply]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G✝ G'✝ G G' : Subpresheaf F
h : G ≤ G'
⊢ homOfLe h ≫ ι G' = ι G
[PROOFSTEP]
ext
[GOAL]
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G✝ G'✝ G G' : Subpresheaf F
h : G ≤ G'
x✝ : Cᵒᵖ
a✝ : (toPresheaf G).obj x✝
⊢ NatTrans.app (homOfLe h ≫ ι G') x✝ a✝ = NatTrans.app (ι G) x✝ a✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ IsIso (Subpresheaf.ι ⊤)
[PROOFSTEP]
refine @NatIso.isIso_of_isIso_app _ _ _ _ _ _ _ ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ ∀ (X : Cᵒᵖ), IsIso (NatTrans.app (Subpresheaf.ι ⊤) X)
[PROOFSTEP]
intro X
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
X : Cᵒᵖ
⊢ IsIso (NatTrans.app (Subpresheaf.ι ⊤) X)
[PROOFSTEP]
rw [isIso_iff_bijective]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
X : Cᵒᵖ
⊢ Function.Bijective (NatTrans.app (Subpresheaf.ι ⊤) X)
[PROOFSTEP]
exact ⟨Subtype.coe_injective, fun x => ⟨⟨x, _root_.trivial⟩, rfl⟩⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ G = ⊤ ↔ IsIso (ι G)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ G = ⊤ → IsIso (ι G)
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G' : Subpresheaf F
⊢ IsIso (ι ⊤)
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ IsIso (ι G) → G = ⊤
[PROOFSTEP]
intro H
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
⊢ G = ⊤
[PROOFSTEP]
ext U x
[GOAL]
case mpr.obj.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
U : Cᵒᵖ
x : F.obj U
⊢ x ∈ obj G U ↔ x ∈ obj ⊤ U
[PROOFSTEP]
apply iff_true_iff.mpr
[GOAL]
case mpr.obj.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
U : Cᵒᵖ
x : F.obj U
⊢ x ∈ obj G U
[PROOFSTEP]
rw [← IsIso.inv_hom_id_apply (G.ι.app U) x]
[GOAL]
case mpr.obj.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
U : Cᵒᵖ
x : F.obj U
⊢ ↑(NatTrans.app (ι G) U)
      (↑(Classical.choose
            (_ :
              ∃ inv, NatTrans.app (ι G) U ≫ inv = 𝟙 ((toPresheaf G).obj U) ∧ inv ≫ NatTrans.app (ι G) U = 𝟙 (F.obj U)))
        x) ∈
    obj G U
[PROOFSTEP]
exact ((inv (G.ι.app U)) x).2
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), NatTrans.app f U x ∈ obj G U
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y),
    F'.map f_1 ≫ (fun U x => { val := NatTrans.app f U x, property := (_ : NatTrans.app f U x ∈ obj G U) }) Y =
      (fun U x => { val := NatTrans.app f U x, property := (_ : NatTrans.app f U x ∈ obj G U) }) X ≫
        (toPresheaf G).map f_1
[PROOFSTEP]
have := elementwise_of% f.naturality
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), NatTrans.app f U x ∈ obj G U
this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : F'.obj X), NatTrans.app f Y (F'.map f_1 x) = F.map f_1 (NatTrans.app f X x)
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y),
    F'.map f_1 ≫ (fun U x => { val := NatTrans.app f U x, property := (_ : NatTrans.app f U x ∈ obj G U) }) Y =
      (fun U x => { val := NatTrans.app f U x, property := (_ : NatTrans.app f U x ∈ obj G U) }) X ≫
        (toPresheaf G).map f_1
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), NatTrans.app f U x ∈ obj G U
this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : F'.obj X), NatTrans.app f Y (F'.map f_1 x) = F.map f_1 (NatTrans.app f X x)
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ F'.map f✝ ≫ (fun U x => { val := NatTrans.app f U x, property := (_ : NatTrans.app f U x ∈ obj G U) }) Y✝ =
    (fun U x => { val := NatTrans.app f U x, property := (_ : NatTrans.app f U x ∈ obj G U) }) X✝ ≫
      (toPresheaf G).map f✝
[PROOFSTEP]
refine funext fun x => Subtype.ext ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), NatTrans.app f U x ∈ obj G U
this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : F'.obj X), NatTrans.app f Y (F'.map f_1 x) = F.map f_1 (NatTrans.app f X x)
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
x : F'.obj X✝
⊢ ↑((F'.map f✝ ≫ (fun U x => { val := NatTrans.app f U x, property := (_ : NatTrans.app f U x ∈ obj G U) }) Y✝) x) =
    ↑(((fun U x => { val := NatTrans.app f U x, property := (_ : NatTrans.app f U x ∈ obj G U) }) X✝ ≫
          (toPresheaf G).map f✝)
        x)
[PROOFSTEP]
simp only [toPresheaf_obj, types_comp_apply]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), NatTrans.app f U x ∈ obj G U
this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : F'.obj X), NatTrans.app f Y (F'.map f_1 x) = F.map f_1 (NatTrans.app f X x)
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
x : F'.obj X✝
⊢ NatTrans.app f Y✝ (F'.map f✝ x) =
    ↑((toPresheaf G).map f✝ { val := NatTrans.app f X✝ x, property := (_ : NatTrans.app f X✝ x ∈ obj G X✝) })
[PROOFSTEP]
exact this _ _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), NatTrans.app f U x ∈ obj G U
⊢ lift G f hf ≫ ι G = f
[PROOFSTEP]
ext
[GOAL]
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), NatTrans.app f U x ∈ obj G U
x✝ : Cᵒᵖ
a✝ : F'.obj x✝
⊢ NatTrans.app (lift G f hf ≫ ι G) x✝ a✝ = NatTrans.app f x✝ a✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
V W : C
i : V ⟶ U.unop
hi : (fun V f => F.map f.op s ∈ obj G (op V)) V i
j : W ⟶ V
⊢ (fun V f => F.map f.op s ∈ obj G (op V)) W (j ≫ i)
[PROOFSTEP]
simp only [op_unop, op_comp, FunctorToTypes.map_comp_apply]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
V W : C
i : V ⟶ U.unop
hi : (fun V f => F.map f.op s ∈ obj G (op V)) V i
j : W ⟶ V
⊢ F.map j.op (F.map i.op s) ∈ obj G (op W)
[PROOFSTEP]
exact G.map _ hi
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
⊢ Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s)
[PROOFSTEP]
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ e
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ U.unop
f₂ : Y₂ ⟶ U.unop
h₁ : (sieveOfSection G s).arrows f₁
h₂ : (sieveOfSection G s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (toPresheaf G).map g₁.op (familyOfElementsOfSection G s f₁ h₁) =
    (toPresheaf G).map g₂.op (familyOfElementsOfSection G s f₂ h₂)
[PROOFSTEP]
refine
  Subtype.ext
    ?_
      -- port note: `ext1` does not work here
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ U.unop
f₂ : Y₂ ⟶ U.unop
h₁ : (sieveOfSection G s).arrows f₁
h₂ : (sieveOfSection G s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ ↑((toPresheaf G).map g₁.op (familyOfElementsOfSection G s f₁ h₁)) =
    ↑((toPresheaf G).map g₂.op (familyOfElementsOfSection G s f₂ h₂))
[PROOFSTEP]
change F.map g₁.op (F.map f₁.op s) = F.map g₂.op (F.map f₂.op s)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ U.unop
f₂ : Y₂ ⟶ U.unop
h₁ : (sieveOfSection G s).arrows f₁
h₂ : (sieveOfSection G s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ F.map g₁.op (F.map f₁.op s) = F.map g₂.op (F.map f₂.op s)
[PROOFSTEP]
rw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply, ← op_comp, ← op_comp, e]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ ∀ {U V : Cᵒᵖ} (i : U ⟶ V),
    (fun U => {s | sieveOfSection G s ∈ sieves J U.unop}) U ⊆
      F.map i ⁻¹' (fun U => {s | sieveOfSection G s ∈ sieves J U.unop}) V
[PROOFSTEP]
rintro U V i s hs
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs : s ∈ (fun U => {s | sieveOfSection G s ∈ sieves J U.unop}) U
⊢ s ∈ F.map i ⁻¹' (fun U => {s | sieveOfSection G s ∈ sieves J U.unop}) V
[PROOFSTEP]
refine' J.superset_covering _ (J.pullback_stable i.unop hs)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs : s ∈ (fun U => {s | sieveOfSection G s ∈ sieves J U.unop}) U
⊢ Sieve.pullback i.unop (sieveOfSection G s) ≤ sieveOfSection G (F.map i s)
[PROOFSTEP]
intro _ _ h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs : s ∈ (fun U => {s | sieveOfSection G s ∈ sieves J U.unop}) U
Y✝ : C
f✝ : Y✝ ⟶ V.unop
h : (Sieve.pullback i.unop (sieveOfSection G s)).arrows f✝
⊢ (sieveOfSection G (F.map i s)).arrows f✝
[PROOFSTEP]
dsimp at h ⊢
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs : s ∈ (fun U => {s | sieveOfSection G s ∈ sieves J U.unop}) U
Y✝ : C
f✝ : Y✝ ⟶ V.unop
h : F.map (i ≫ f✝.op) s ∈ obj G (op Y✝)
⊢ F.map f✝.op (F.map i s) ∈ obj G (op Y✝)
[PROOFSTEP]
rwa [← FunctorToTypes.map_comp_apply]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ G ≤ sheafify J G
[PROOFSTEP]
intro U s hs
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj G U
⊢ s ∈ obj (sheafify J G) U
[PROOFSTEP]
change _ ∈ J _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj G U
⊢ sieveOfSection G s ∈ sieves J U.unop
[PROOFSTEP]
convert J.top_mem U.unop
[GOAL]
case h.e'_4
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj G U
⊢ sieveOfSection G s = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
case h.e'_4
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj G U
⊢ ⊤ ≤ sieveOfSection G s
[PROOFSTEP]
rintro V i -
[GOAL]
case h.e'_4
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj G U
V : C
i : V ⟶ U.unop
⊢ (sieveOfSection G s).arrows i
[PROOFSTEP]
exact G.map i.op hs
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
⊢ G = sheafify J G
[PROOFSTEP]
apply (G.le_sheafify J).antisymm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
⊢ sheafify J G ≤ G
[PROOFSTEP]
intro U s hs
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ s ∈ obj G U
[PROOFSTEP]
suffices ((hG _ hs).amalgamate _ (G.family_of_elements_compatible s)).1 = s
  by
  rw [← this]
  exact ((hG _ hs).amalgamate _ (G.family_of_elements_compatible s)).2
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
this :
  ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
        (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
    s
⊢ s ∈ obj G U
[PROOFSTEP]
rw [← this]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
this :
  ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
        (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
    s
⊢ ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
        (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) ∈
    obj G U
[PROOFSTEP]
exact ((hG _ hs).amalgamate _ (G.family_of_elements_compatible s)).2
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
        (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
    s
[PROOFSTEP]
apply (h _ hs).isSeparatedFor.ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
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
          ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
              (familyOfElementsOfSection G s)
              (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
        F.map f.op s
[PROOFSTEP]
intro V i hi
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
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
      ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
          (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
    F.map i.op s
[PROOFSTEP]
exact (congr_arg Subtype.val ((hG _ hs).valid_glue (G.family_of_elements_compatible s) _ hi) : _)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
⊢ Presieve.IsSheaf J (toPresheaf (sheafify J G))
[PROOFSTEP]
intro U S hS x hx
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
let S' := Sieve.bind S fun Y f hf => G.sieveOfSection (x f hf).1
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
have := fun (V) (i : V ⟶ U) (hi : S' i) => hi
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
this : ∀ (V : C) (i : V ⟶ U), S'.arrows i → S'.arrows i
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
choose W i₁ i₂ hi₂ h₁ h₂ using this
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (fun Y f h => ((fun Y f hf => sieveOfSection G ↑(x f hf)) Y f h).arrows) (W V i hi) (i₂ V i hi)
      (_ : S.arrows (i₂ V i hi)) (i₁ V i hi)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
dsimp [-Sieve.bind_apply] at *
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
let x'' : Presieve.FamilyOfElements F S' := fun V i hi => F.map (i₁ V i hi).op (x _ (hi₂ V i hi))
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
have H : ∀ s, x.IsAmalgamation s ↔ x''.IsAmalgamation s.1 :=
  by
  intro s
  constructor
  · intro H V i hi
    dsimp only [show x'' = fun V i hi => F.map (i₁ V i hi).op (x _ (hi₂ V i hi)) from rfl]
    conv_lhs => rw [← h₂ _ _ hi]
    rw [← H _ (hi₂ _ _ hi)]
    exact FunctorToTypes.map_comp_apply F (i₂ _ _ hi).op (i₁ _ _ hi).op _
  · intro H V i hi
    refine Subtype.ext ?_
    apply (hF _ (x i hi).2).isSeparatedFor.ext
    intro V' i' hi'
    have hi'' : S' (i' ≫ i) := ⟨_, _, _, hi, hi', rfl⟩
    have := H _ hi''
    rw [op_comp, F.map_comp] at this 
    refine' this.trans (congr_arg Subtype.val (hx _ _ (hi₂ _ _ hi'') hi (h₂ _ _ hi'')))
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
⊢ ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
[PROOFSTEP]
intro s
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
⊢ Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
⊢ Presieve.FamilyOfElements.IsAmalgamation x s → Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
[PROOFSTEP]
intro H V i hi
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map i.op ↑s = x'' i hi
[PROOFSTEP]
dsimp only [show x'' = fun V i hi => F.map (i₁ V i hi).op (x _ (hi₂ V i hi)) from rfl]
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map i.op ↑s = F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
[PROOFSTEP]
conv_lhs => rw [← h₂ _ _ hi]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
| F.map i.op ↑s
[PROOFSTEP]
rw [← h₂ _ _ hi]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
| F.map i.op ↑s
[PROOFSTEP]
rw [← h₂ _ _ hi]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
| F.map i.op ↑s
[PROOFSTEP]
rw [← h₂ _ _ hi]
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map (i₁ V i hi ≫ i₂ V i hi).op ↑s = F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
[PROOFSTEP]
rw [← H _ (hi₂ _ _ hi)]
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map (i₁ V i hi ≫ i₂ V i hi).op ↑s = F.map (i₁ V i hi).op ↑((toPresheaf (sheafify J G)).map (i₂ V i hi).op s)
[PROOFSTEP]
exact FunctorToTypes.map_comp_apply F (i₂ _ _ hi).op (i₁ _ _ hi).op _
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
⊢ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s → Presieve.FamilyOfElements.IsAmalgamation x s
[PROOFSTEP]
intro H V i hi
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ (toPresheaf (sheafify J G)).map i.op s = x i hi
[PROOFSTEP]
refine Subtype.ext ?_
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ ↑((toPresheaf (sheafify J G)).map i.op s) = ↑(x i hi)
[PROOFSTEP]
apply (hF _ (x i hi).2).isSeparatedFor.ext
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ (op V).unop⦄,
    (sieveOfSection G ↑(x i hi)).arrows f → F.map f.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map f.op ↑(x i hi)
[PROOFSTEP]
intro V' i' hi'
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ (op V).unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
[PROOFSTEP]
have hi'' : S' (i' ≫ i) := ⟨_, _, _, hi, hi', rfl⟩
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ (op V).unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
[PROOFSTEP]
have := H _ hi''
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ (op V).unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : F.map (i' ≫ i).op ↑s = x'' (i' ≫ i) hi''
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
[PROOFSTEP]
rw [op_comp, F.map_comp] at this 
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
s : (toPresheaf (sheafify J G)).obj (op U)
H : Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ (op V).unop
hi' : (sieveOfSection G ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : (F.map i.op ≫ F.map i'.op) ↑s = x'' (i' ≫ i) hi''
⊢ F.map i'.op ↑((toPresheaf (sheafify J G)).map i.op s) = F.map i'.op ↑(x i hi)
[PROOFSTEP]
refine' this.trans (congr_arg Subtype.val (hx _ _ (hi₂ _ _ hi'') hi (h₂ _ _ hi'')))
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
have : x''.Compatible := by
  intro V₁ V₂ V₃ g₁ g₂ g₃ g₄ S₁ S₂ e
  rw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply]
  exact
    congr_arg Subtype.val
      (hx (g₁ ≫ i₁ _ _ S₁) (g₂ ≫ i₁ _ _ S₂) (hi₂ _ _ S₁) (hi₂ _ _ S₂) (by simp only [Category.assoc, h₂, e]))
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
⊢ Presieve.FamilyOfElements.Compatible x''
[PROOFSTEP]
intro V₁ V₂ V₃ g₁ g₂ g₃ g₄ S₁ S₂ e
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ F.map g₁.op (x'' g₃ S₁) = F.map g₂.op (x'' g₄ S₂)
[PROOFSTEP]
rw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ F.map ((i₁ V₁ g₃ S₁).op ≫ g₁.op) ↑(x (i₂ V₁ g₃ S₁) (_ : S.arrows (i₂ V₁ g₃ S₁))) =
    F.map ((i₁ V₂ g₄ S₂).op ≫ g₂.op) ↑(x (i₂ V₂ g₄ S₂) (_ : S.arrows (i₂ V₂ g₄ S₂)))
[PROOFSTEP]
exact
  congr_arg Subtype.val
    (hx (g₁ ≫ i₁ _ _ S₁) (g₂ ≫ i₁ _ _ S₂) (hi₂ _ _ S₁) (hi₂ _ _ S₂) (by simp only [Category.assoc, h₂, e]))
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ (g₁ ≫ i₁ V₁ g₃ S₁) ≫ i₂ V₁ g₃ S₁ = (g₂ ≫ i₁ V₂ g₄ S₂) ≫ i₂ V₂ g₄ S₂
[PROOFSTEP]
simp only [Category.assoc, h₂, e]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
obtain ⟨t, ht, ht'⟩ := hF _ (J.bind_covering hS fun V i hi => (x i hi).2) _ this
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj (op U)
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj (op U)), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
refine' ⟨⟨t, _⟩, (H ⟨t, _⟩).mpr ht, fun y hy => Subtype.ext (ht' _ ((H _).mp hy))⟩
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj (op U)
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj (op U)), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
⊢ t ∈ obj (sheafify J G) (op U)
[PROOFSTEP]
refine' J.superset_covering _ (J.bind_covering hS fun V i hi => (x i hi).2)
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj (op U)
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj (op U)), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
⊢ (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)) ≤ sieveOfSection G t
[PROOFSTEP]
intro V i hi
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj (op U)
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj (op U)), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
V : C
i : V ⟶ (op U).unop
hi : (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)).arrows i
⊢ (sieveOfSection G t).arrows i
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj (op U)
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj (op U)), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
V : C
i : V ⟶ (op U).unop
hi : (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)).arrows i
⊢ F.map i.op t ∈ obj G (op V)
[PROOFSTEP]
rw [ht _ hi]
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ sieves J U
x : Presieve.FamilyOfElements (toPresheaf (sheafify J G)) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi))) ∈ obj G (op V)
h₂ :
  ∀ (V : C) (i : V ⟶ U) (hi : (Sieve.bind S.arrows fun Y f hf => sieveOfSection G ↑(x f hf)).arrows i),
    i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) (_ : S.arrows (i₂ V i hi)))
H :
  ∀ (s : (toPresheaf (sheafify J G)).obj (op U)),
    Presieve.FamilyOfElements.IsAmalgamation x s ↔ Presieve.FamilyOfElements.IsAmalgamation x'' ↑s
this : Presieve.FamilyOfElements.Compatible x''
t : F.obj (op U)
ht : Presieve.FamilyOfElements.IsAmalgamation x'' t
ht' : ∀ (y : F.obj (op U)), (fun t => Presieve.FamilyOfElements.IsAmalgamation x'' t) y → y = t
V : C
i : V ⟶ (op U).unop
hi : (Sieve.bind S.arrows fun V i hi => sieveOfSection G ↑(x i hi)).arrows i
⊢ x'' i hi ∈ obj G (op V)
[PROOFSTEP]
exact h₁ _ _ hi
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ Presieve.IsSheaf J (toPresheaf G) ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), sieveOfSection G s ∈ sieves J U.unop → s ∈ obj G U
[PROOFSTEP]
rw [← G.eq_sheafify_iff h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), sieveOfSection G s ∈ sieves J U.unop → s ∈ obj G U
[PROOFSTEP]
change _ ↔ G.sheafify J ≤ G
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ sheafify J G ≤ G
[PROOFSTEP]
exact ⟨Eq.ge, (G.le_sheafify J).antisymm⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y),
    (toPresheaf (sheafify J G)).map f_1 ≫
        (fun U s =>
            Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
              (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
              (_ :
                Presieve.FamilyOfElements.Compatible
                  (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
          Y =
      (fun U s =>
            Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
              (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
              (_ :
                Presieve.FamilyOfElements.Compatible
                  (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
          X ≫
        F'.map f_1
[PROOFSTEP]
intro U V i
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
⊢ (toPresheaf (sheafify J G)).map i ≫
      (fun U s =>
          Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
            (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
            (_ :
              Presieve.FamilyOfElements.Compatible
                (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
        V =
    (fun U s =>
          Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
            (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
            (_ :
              Presieve.FamilyOfElements.Compatible
                (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
        U ≫
      F'.map i
[PROOFSTEP]
ext s
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
⊢ ((toPresheaf (sheafify J G)).map i ≫
        (fun U s =>
            Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
              (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
              (_ :
                Presieve.FamilyOfElements.Compatible
                  (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
          V)
      s =
    ((fun U s =>
            Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
              (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
              (_ :
                Presieve.FamilyOfElements.Compatible
                  (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
          U ≫
        F'.map i)
      s
[PROOFSTEP]
apply (h _ ((Subpresheaf.sheafify J G).toPresheaf.map i s).prop).isSeparatedFor.ext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ V.unop⦄,
    (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows f_1 →
      F'.map f_1.op
          (((toPresheaf (sheafify J G)).map i ≫
              (fun U s =>
                  Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
                    (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
                    (_ :
                      Presieve.FamilyOfElements.Compatible
                        (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
                V)
            s) =
        F'.map f_1.op
          (((fun U s =>
                  Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
                    (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
                    (_ :
                      Presieve.FamilyOfElements.Compatible
                        (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
                U ≫
              F'.map i)
            s)
[PROOFSTEP]
intro W j hj
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
⊢ F'.map j.op
      (((toPresheaf (sheafify J G)).map i ≫
          (fun U s =>
              Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
                (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
                (_ :
                  Presieve.FamilyOfElements.Compatible
                    (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
            V)
        s) =
    F'.map j.op
      (((fun U s =>
              Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
                (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
                (_ :
                  Presieve.FamilyOfElements.Compatible
                    (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
            U ≫
          F'.map i)
        s)
[PROOFSTEP]
refine'
  (Presieve.IsSheafFor.valid_glue (h _ ((G.sheafify J).toPresheaf.map i s).2)
        ((G.family_of_elements_compatible _).compPresheafMap _) _ hj).trans
    _
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
⊢ Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑((toPresheaf (sheafify J G)).map i s)) j
      hj =
    F'.map j.op
      (((fun U s =>
              Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
                (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
                (_ :
                  Presieve.FamilyOfElements.Compatible
                    (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
            U ≫
          F'.map i)
        s)
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
⊢ Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G (F.map i ↑s)) j hj =
    F'.map j.op
      (F'.map i
        (Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
          (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
          (_ :
            Presieve.FamilyOfElements.Compatible
              (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s)))))
[PROOFSTEP]
conv_rhs => rw [← FunctorToTypes.map_comp_apply]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
| F'.map j.op
    (F'.map i
      (Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
        (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
        (_ :
          Presieve.FamilyOfElements.Compatible
            (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s)))))
[PROOFSTEP]
rw [← FunctorToTypes.map_comp_apply]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
| F'.map j.op
    (F'.map i
      (Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
        (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
        (_ :
          Presieve.FamilyOfElements.Compatible
            (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s)))))
[PROOFSTEP]
rw [← FunctorToTypes.map_comp_apply]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
| F'.map j.op
    (F'.map i
      (Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
        (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
        (_ :
          Presieve.FamilyOfElements.Compatible
            (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s)))))
[PROOFSTEP]
rw [← FunctorToTypes.map_comp_apply]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
⊢ Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G (F.map i ↑s)) j hj =
    F'.map (i ≫ j.op)
      (Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
        (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
        (_ :
          Presieve.FamilyOfElements.Compatible
            (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
[PROOFSTEP]
change _ = F'.map (j ≫ i.unop).op _
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
⊢ Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G (F.map i ↑s)) j hj =
    F'.map (j ≫ i.unop).op
      (Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor F' (sieveOfSection G ↑s).arrows)
        (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))
        (_ :
          Presieve.FamilyOfElements.Compatible
            (Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s))))
[PROOFSTEP]
refine'
  Eq.trans _
    (Presieve.IsSheafFor.valid_glue (h _ s.2) ((G.family_of_elements_compatible s.1).compPresheafMap f) (j ≫ i.unop)
        _).symm
[GOAL]
case h.refine'_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
⊢ Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G (F.map i ↑s)) j hj =
    Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s) (j ≫ i.unop) ?h.refine'_2
case h.refine'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
⊢ (sieveOfSection G ↑s).arrows (j ≫ i.unop)
[PROOFSTEP]
swap
  -- porting note: need to swap two goals otherwise the first goal needs to be proven
      -- inside the second goal any way
[GOAL]
case h.refine'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
⊢ (sieveOfSection G ↑s).arrows (j ≫ i.unop)
[PROOFSTEP]
dsimp [Presieve.FamilyOfElements.compPresheafMap] at hj ⊢
[GOAL]
case h.refine'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : F.map j.op (F.map i ↑s) ∈ obj G (op W)
⊢ F.map (i ≫ j.op) ↑s ∈ obj G (op W)
[PROOFSTEP]
rwa [FunctorToTypes.map_comp_apply]
[GOAL]
case h.refine'_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
⊢ Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G (F.map i ↑s)) j hj =
    Presieve.FamilyOfElements.compPresheafMap f (familyOfElementsOfSection G ↑s) (j ≫ i.unop)
      (_ : (sieveOfSection G ↑s).arrows (j ≫ i.unop))
[PROOFSTEP]
dsimp [Presieve.FamilyOfElements.compPresheafMap]
[GOAL]
case h.refine'_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (toPresheaf (sheafify J G)).obj U
W : C
j : W ⟶ V.unop
hj : (sieveOfSection G ↑((toPresheaf (sheafify J G)).map i s)).arrows j
⊢ NatTrans.app f (op W) (familyOfElementsOfSection G (F.map i ↑s) j hj) =
    NatTrans.app f (op W) (familyOfElementsOfSection G (↑s) (j ≫ i.unop) (_ : F.map (i ≫ j.op) ↑s ∈ obj G (op W)))
[PROOFSTEP]
exact congr_arg _ (Subtype.ext (FunctorToTypes.map_comp_apply _ _ _ _).symm)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
⊢ homOfLe (_ : G ≤ sheafify J G) ≫ sheafifyLift G f h = f
[PROOFSTEP]
ext U s
[GOAL]
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : (toPresheaf G).obj U
⊢ NatTrans.app (homOfLe (_ : G ≤ sheafify J G) ≫ sheafifyLift G f h) U s = NatTrans.app f U s
[PROOFSTEP]
apply (h _ ((Subpresheaf.homOfLe (G.le_sheafify J)).app U s).prop).isSeparatedFor.ext
[GOAL]
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : (toPresheaf G).obj U
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ U.unop⦄,
    (sieveOfSection G ↑(NatTrans.app (homOfLe (_ : G ≤ sheafify J G)) U s)).arrows f_1 →
      F'.map f_1.op (NatTrans.app (homOfLe (_ : G ≤ sheafify J G) ≫ sheafifyLift G f h) U s) =
        F'.map f_1.op (NatTrans.app f U s)
[PROOFSTEP]
intro V i hi
[GOAL]
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : (toPresheaf G).obj U
V : C
i : V ⟶ U.unop
hi : (sieveOfSection G ↑(NatTrans.app (homOfLe (_ : G ≤ sheafify J G)) U s)).arrows i
⊢ F'.map i.op (NatTrans.app (homOfLe (_ : G ≤ sheafify J G) ≫ sheafifyLift G f h) U s) =
    F'.map i.op (NatTrans.app f U s)
[PROOFSTEP]
have := elementwise_of% f.naturality
[GOAL]
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : toPresheaf G ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : (toPresheaf G).obj U
V : C
i : V ⟶ U.unop
hi : (sieveOfSection G ↑(NatTrans.app (homOfLe (_ : G ≤ sheafify J G)) U s)).arrows i
this :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : (toPresheaf G).obj X),
    NatTrans.app f Y ((toPresheaf G).map f_1 x) = F'.map f_1 (NatTrans.app f X x)
⊢ F'.map i.op (NatTrans.app (homOfLe (_ : G ≤ sheafify J G) ≫ sheafifyLift G f h) U s) =
    F'.map i.op (NatTrans.app f U s)
[PROOFSTEP]
exact
  (Presieve.IsSheafFor.valid_glue (h _ ((homOfLe (_ : G ≤ sheafify J G)).app U s).2)
        ((G.family_of_elements_compatible _).compPresheafMap _) _ hi).trans
    (this _ _)
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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₂
[PROOFSTEP]
ext U ⟨s, hs⟩
[GOAL]
case w.h.h.mk
C : Type u
inst✝ : Category.{v, u} 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
⊢ NatTrans.app l₁ U { val := s, property := hs } = NatTrans.app l₂ U { val := s, property := hs }
[PROOFSTEP]
apply (h _ hs).isSeparatedFor.ext
[GOAL]
case w.h.h.mk
C : Type u
inst✝ : Category.{v, u} 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 (NatTrans.app l₁ U { val := s, property := hs }) =
        F'.map f.op (NatTrans.app l₂ U { val := s, property := hs })
[PROOFSTEP]
rintro V i hi
[GOAL]
case w.h.h.mk
C : Type u
inst✝ : Category.{v, u} 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 (NatTrans.app l₁ U { val := s, property := hs }) =
    F'.map i.op (NatTrans.app l₂ U { val := s, property := hs })
[PROOFSTEP]
dsimp at hi 
[GOAL]
case w.h.h.mk
C : Type u
inst✝ : Category.{v, u} 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 (op V)
⊢ F'.map i.op (NatTrans.app l₁ U { val := s, property := hs }) =
    F'.map i.op (NatTrans.app l₂ U { val := s, property := hs })
[PROOFSTEP]
erw [← FunctorToTypes.naturality, ← FunctorToTypes.naturality]
[GOAL]
case w.h.h.mk
C : Type u
inst✝ : Category.{v, u} 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 (op V)
⊢ NatTrans.app l₁ (op V) ((toPresheaf (sheafify J G)).map i.op { val := s, property := hs }) =
    NatTrans.app l₂ (op V) ((toPresheaf (sheafify J G)).map i.op { val := s, property := hs })
[PROOFSTEP]
exact (congr_fun (congr_app e <| op V) ⟨_, hi⟩ : _)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J (toPresheaf G')
⊢ sheafify J G ≤ G'
[PROOFSTEP]
intro U x hx
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J (toPresheaf G')
U : Cᵒᵖ
x : F.obj U
hx : x ∈ obj (sheafify J G) U
⊢ x ∈ obj G' U
[PROOFSTEP]
convert ((G.sheafifyLift (Subpresheaf.homOfLe h) hG').app U ⟨x, hx⟩).2
[GOAL]
case h.e'_4
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J (toPresheaf G')
U : Cᵒᵖ
x : F.obj U
hx : x ∈ obj (sheafify J G) U
⊢ x = ↑(NatTrans.app (sheafifyLift G (homOfLe h) hG') U { val := x, property := hx })
[PROOFSTEP]
apply (hF _ hx).isSeparatedFor.ext
[GOAL]
case h.e'_4
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J (toPresheaf G')
U : Cᵒᵖ
x : F.obj U
hx : x ∈ obj (sheafify J G) U
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ U.unop⦄,
    (sieveOfSection G x).arrows f →
      F.map f.op x = F.map f.op ↑(NatTrans.app (sheafifyLift G (homOfLe h) hG') U { val := x, property := hx })
[PROOFSTEP]
intro V i hi
[GOAL]
case h.e'_4
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J (toPresheaf G')
U : Cᵒᵖ
x : F.obj U
hx : x ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : (sieveOfSection G x).arrows i
⊢ F.map i.op x = F.map i.op ↑(NatTrans.app (sheafifyLift G (homOfLe h) hG') U { val := x, property := hx })
[PROOFSTEP]
have :=
  congr_arg (fun f : G.toPresheaf ⟶ G'.toPresheaf => (NatTrans.app f (op V) ⟨_, hi⟩).1)
    (G.to_sheafifyLift (Subpresheaf.homOfLe h) hG')
[GOAL]
case h.e'_4
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J (toPresheaf G')
U : Cᵒᵖ
x : F.obj U
hx : x ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : (sieveOfSection G x).arrows i
this :
  (fun f => ↑(NatTrans.app f (op V) { val := F.map i.op x, property := hi }))
      (homOfLe (_ : G ≤ sheafify J G) ≫ sheafifyLift G (homOfLe h) hG') =
    (fun f => ↑(NatTrans.app f (op V) { val := F.map i.op x, property := hi })) (homOfLe h)
⊢ F.map i.op x = F.map i.op ↑(NatTrans.app (sheafifyLift G (homOfLe h) hG') U { val := x, property := hx })
[PROOFSTEP]
convert this.symm
[GOAL]
case h.e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J (toPresheaf G')
U : Cᵒᵖ
x : F.obj U
hx : x ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : (sieveOfSection G x).arrows i
this :
  (fun f => ↑(NatTrans.app f (op V) { val := F.map i.op x, property := hi }))
      (homOfLe (_ : G ≤ sheafify J G) ≫ sheafifyLift G (homOfLe h) hG') =
    (fun f => ↑(NatTrans.app f (op V) { val := F.map i.op x, property := hi })) (homOfLe h)
⊢ F.map i.op ↑(NatTrans.app (sheafifyLift G (homOfLe h) hG') U { val := x, property := hx }) =
    (fun f => ↑(NatTrans.app f (op V) { val := F.map i.op x, property := hi }))
      (homOfLe (_ : G ≤ sheafify J G) ≫ sheafifyLift G (homOfLe h) hG')
[PROOFSTEP]
erw [← Subpresheaf.nat_trans_naturality]
[GOAL]
case h.e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J (toPresheaf G')
U : Cᵒᵖ
x : F.obj U
hx : x ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : (sieveOfSection G x).arrows i
this :
  (fun f => ↑(NatTrans.app f (op V) { val := F.map i.op x, property := hi }))
      (homOfLe (_ : G ≤ sheafify J G) ≫ sheafifyLift G (homOfLe h) hG') =
    (fun f => ↑(NatTrans.app f (op V) { val := F.map i.op x, property := hi })) (homOfLe h)
⊢ ↑(NatTrans.app (sheafifyLift G (homOfLe h) hG') (op V)
        ((toPresheaf (sheafify J G)).map i.op { val := x, property := hx })) =
    (fun f => ↑(NatTrans.app f (op V) { val := F.map i.op x, property := hi }))
      (homOfLe (_ : G ≤ sheafify J G) ≫ sheafifyLift G (homOfLe h) hG')
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
⊢ ∀ {U V : Cᵒᵖ} (i : U ⟶ V),
    (fun U => Set.range (NatTrans.app f U)) U ⊆ F.map i ⁻¹' (fun U => Set.range (NatTrans.app f U)) V
[PROOFSTEP]
rintro U V i _ ⟨x, rfl⟩
[GOAL]
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
U V : Cᵒᵖ
i : U ⟶ V
x : F'.obj U
⊢ NatTrans.app f U x ∈ F.map i ⁻¹' (fun U => Set.range (NatTrans.app f U)) V
[PROOFSTEP]
have := elementwise_of% f.naturality
[GOAL]
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
U V : Cᵒᵖ
i : U ⟶ V
x : F'.obj U
this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : F'.obj X), NatTrans.app f Y (F'.map f_1 x) = F.map f_1 (NatTrans.app f X x)
⊢ NatTrans.app f U x ∈ F.map i ⁻¹' (fun U => Set.range (NatTrans.app f U)) V
[PROOFSTEP]
exact ⟨_, this i x⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ imagePresheaf (𝟙 F) = ⊤
[PROOFSTEP]
ext
[GOAL]
case obj.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
x✝¹ : Cᵒᵖ
x✝ : F.obj x✝¹
⊢ x✝ ∈ Subpresheaf.obj (imagePresheaf (𝟙 F)) x✝¹ ↔ x✝ ∈ Subpresheaf.obj ⊤ x✝¹
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Cᵒᵖ ⥤ TypeMax
f : F ⟶ F'
hf : Mono f
⊢ IsIso (toImagePresheaf f)
[PROOFSTEP]
have : ∀ (X : Cᵒᵖ), IsIso ((toImagePresheaf f).app X) :=
  by
  intro X
  rw [isIso_iff_bijective]
  constructor
  · intro x y e
    have := (NatTrans.mono_iff_mono_app _ _).mp hf X
    rw [mono_iff_injective] at this 
    exact this (congr_arg Subtype.val e : _)
  · rintro ⟨_, ⟨x, rfl⟩⟩
    exact ⟨x, rfl⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Cᵒᵖ ⥤ TypeMax
f : F ⟶ F'
hf : Mono f
⊢ ∀ (X : Cᵒᵖ), IsIso (NatTrans.app (toImagePresheaf f) X)
[PROOFSTEP]
intro X
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Cᵒᵖ ⥤ TypeMax
f : F ⟶ F'
hf : Mono f
X : Cᵒᵖ
⊢ IsIso (NatTrans.app (toImagePresheaf f) X)
[PROOFSTEP]
rw [isIso_iff_bijective]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Cᵒᵖ ⥤ TypeMax
f : F ⟶ F'
hf : Mono f
X : Cᵒᵖ
⊢ Function.Bijective (NatTrans.app (toImagePresheaf f) X)
[PROOFSTEP]
constructor
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Cᵒᵖ ⥤ TypeMax
f : F ⟶ F'
hf : Mono f
X : Cᵒᵖ
⊢ Function.Injective (NatTrans.app (toImagePresheaf f) X)
[PROOFSTEP]
intro x y e
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Cᵒᵖ ⥤ TypeMax
f : F ⟶ F'
hf : Mono f
X : Cᵒᵖ
x y : F.obj X
e : NatTrans.app (toImagePresheaf f) X x = NatTrans.app (toImagePresheaf f) X y
⊢ x = y
[PROOFSTEP]
have := (NatTrans.mono_iff_mono_app _ _).mp hf X
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Cᵒᵖ ⥤ TypeMax
f : F ⟶ F'
hf : Mono f
X : Cᵒᵖ
x y : F.obj X
e : NatTrans.app (toImagePresheaf f) X x = NatTrans.app (toImagePresheaf f) X y
this : Mono (NatTrans.app f X)
⊢ x = y
[PROOFSTEP]
rw [mono_iff_injective] at this 
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Cᵒᵖ ⥤ TypeMax
f : F ⟶ F'
hf : Mono f
X : Cᵒᵖ
x y : F.obj X
e : NatTrans.app (toImagePresheaf f) X x = NatTrans.app (toImagePresheaf f) X y
this : Function.Injective (NatTrans.app f X)
⊢ x = y
[PROOFSTEP]
exact this (congr_arg Subtype.val e : _)
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Cᵒᵖ ⥤ TypeMax
f : F ⟶ F'
hf : Mono f
X : Cᵒᵖ
⊢ Function.Surjective (NatTrans.app (toImagePresheaf f) X)
[PROOFSTEP]
rintro ⟨_, ⟨x, rfl⟩⟩
[GOAL]
case right.mk.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Cᵒᵖ ⥤ TypeMax
f : F ⟶ F'
hf : Mono f
X : Cᵒᵖ
x : F.obj X
⊢ ∃ a,
    NatTrans.app (toImagePresheaf f) X a =
      { val := NatTrans.app f X x, property := (_ : ∃ y, NatTrans.app f X y = NatTrans.app f X x) }
[PROOFSTEP]
exact ⟨x, rfl⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Cᵒᵖ ⥤ TypeMax
f : F ⟶ F'
hf : Mono f
this : ∀ (X : Cᵒᵖ), IsIso (NatTrans.app (toImagePresheaf f) X)
⊢ IsIso (toImagePresheaf f)
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf f.val)))
[PROOFSTEP]
rw [isSheaf_iff_isSheaf_of_type]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Presieve.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf f.val)))
[PROOFSTEP]
apply Subpresheaf.sheafify_isSheaf
[GOAL]
case hF
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Presieve.IsSheaf J F'.val
[PROOFSTEP]
rw [← isSheaf_iff_isSheaf_of_type]
[GOAL]
case hF
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Presheaf.IsSheaf J F'.val
[PROOFSTEP]
exact F'.2
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ toImageSheaf f ≫ imageSheafι f = f
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ (toImageSheaf f ≫ imageSheafι f).val = f.val
[PROOFSTEP]
simp [toImagePresheafSheafify]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Mono ((sheafToPresheaf J (Type w)).map (imageSheafι f))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Mono (Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf f.val)))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Epi (toImageSheaf f)
[PROOFSTEP]
refine' ⟨@fun G' g₁ g₂ e => _⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : imageSheaf f ⟶ G'
e : toImageSheaf f ≫ g₁ = toImageSheaf f ≫ g₂
⊢ g₁ = g₂
[PROOFSTEP]
ext U ⟨s, hx⟩
[GOAL]
case h.w.h.h.mk
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : imageSheaf f ⟶ G'
e : toImageSheaf f ≫ g₁ = toImageSheaf f ≫ g₂
U : Cᵒᵖ
s : F'.val.obj U
hx : s ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f.val)) U
⊢ NatTrans.app g₁.val U { val := s, property := hx } = NatTrans.app g₂.val U { val := s, property := hx }
[PROOFSTEP]
apply ((isSheaf_iff_isSheaf_of_type J _).mp G'.2 _ hx).isSeparatedFor.ext
[GOAL]
case h.w.h.h.mk
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : imageSheaf f ⟶ G'
e : toImageSheaf f ≫ g₁ = toImageSheaf f ≫ g₂
U : Cᵒᵖ
s : F'.val.obj U
hx : s ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f.val)) U
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ U.unop⦄,
    (Subpresheaf.sieveOfSection (imagePresheaf f.val) s).arrows f_1 →
      G'.val.map f_1.op (NatTrans.app g₁.val U { val := s, property := hx }) =
        G'.val.map f_1.op (NatTrans.app g₂.val U { val := s, property := hx })
[PROOFSTEP]
rintro V i ⟨y, e'⟩
[GOAL]
case h.w.h.h.mk.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : imageSheaf f ⟶ G'
e : toImageSheaf f ≫ g₁ = toImageSheaf f ≫ g₂
U : Cᵒᵖ
s : F'.val.obj U
hx : s ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f.val)) U
V : C
i : V ⟶ U.unop
y : F.val.obj (op V)
e' : NatTrans.app f.val (op V) y = F'.val.map i.op s
⊢ G'.val.map i.op (NatTrans.app g₁.val U { val := s, property := hx }) =
    G'.val.map i.op (NatTrans.app g₂.val U { val := s, property := hx })
[PROOFSTEP]
change (g₁.val.app _ ≫ G'.val.map _) _ = (g₂.val.app _ ≫ G'.val.map _) _
[GOAL]
case h.w.h.h.mk.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : imageSheaf f ⟶ G'
e : toImageSheaf f ≫ g₁ = toImageSheaf f ≫ g₂
U : Cᵒᵖ
s : F'.val.obj U
hx : s ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f.val)) U
V : C
i : V ⟶ U.unop
y : F.val.obj (op V)
e' : NatTrans.app f.val (op V) y = F'.val.map i.op s
⊢ (NatTrans.app g₁.val (op U.unop) ≫ G'.val.map i.op) { val := s, property := hx } =
    (NatTrans.app g₂.val (op U.unop) ≫ G'.val.map i.op) { val := s, property := hx }
[PROOFSTEP]
rw [← NatTrans.naturality, ← NatTrans.naturality]
[GOAL]
case h.w.h.h.mk.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : imageSheaf f ⟶ G'
e : toImageSheaf f ≫ g₁ = toImageSheaf f ≫ g₂
U : Cᵒᵖ
s : F'.val.obj U
hx : s ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f.val)) U
V : C
i : V ⟶ U.unop
y : F.val.obj (op V)
e' : NatTrans.app f.val (op V) y = F'.val.map i.op s
⊢ ((imageSheaf f).val.map i.op ≫ NatTrans.app g₁.val (op V)) { val := s, property := hx } =
    ((imageSheaf f).val.map i.op ≫ NatTrans.app g₂.val (op V)) { val := s, property := hx }
[PROOFSTEP]
have E : (toImageSheaf f).val.app (op V) y = (imageSheaf f).val.map i.op ⟨s, hx⟩ := Subtype.ext e'
[GOAL]
case h.w.h.h.mk.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : imageSheaf f ⟶ G'
e : toImageSheaf f ≫ g₁ = toImageSheaf f ≫ g₂
U : Cᵒᵖ
s : F'.val.obj U
hx : s ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f.val)) U
V : C
i : V ⟶ U.unop
y : F.val.obj (op V)
e' : NatTrans.app f.val (op V) y = F'.val.map i.op s
E : NatTrans.app (toImageSheaf f).val (op V) y = (imageSheaf f).val.map i.op { val := s, property := hx }
⊢ ((imageSheaf f).val.map i.op ≫ NatTrans.app g₁.val (op V)) { val := s, property := hx } =
    ((imageSheaf f).val.map i.op ≫ NatTrans.app g₂.val (op V)) { val := s, property := hx }
[PROOFSTEP]
have := congr_arg (fun f : F ⟶ G' => (Sheaf.Hom.val f).app _ y) e
[GOAL]
case h.w.h.h.mk.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : imageSheaf f ⟶ G'
e : toImageSheaf f ≫ g₁ = toImageSheaf f ≫ g₂
U : Cᵒᵖ
s : F'.val.obj U
hx : s ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f.val)) U
V : C
i : V ⟶ U.unop
y : F.val.obj (op V)
e' : NatTrans.app f.val (op V) y = F'.val.map i.op s
E : NatTrans.app (toImageSheaf f).val (op V) y = (imageSheaf f).val.map i.op { val := s, property := hx }
this :
  (fun f => NatTrans.app f.val (op V) y) (toImageSheaf f ≫ g₁) =
    (fun f => NatTrans.app f.val (op V) y) (toImageSheaf f ≫ g₂)
⊢ ((imageSheaf f).val.map i.op ≫ NatTrans.app g₁.val (op V)) { val := s, property := hx } =
    ((imageSheaf f).val.map i.op ≫ NatTrans.app g₂.val (op V)) { val := s, property := hx }
[PROOFSTEP]
dsimp at this ⊢
[GOAL]
case h.w.h.h.mk.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : imageSheaf f ⟶ G'
e : toImageSheaf f ≫ g₁ = toImageSheaf f ≫ g₂
U : Cᵒᵖ
s : F'.val.obj U
hx : s ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f.val)) U
V : C
i : V ⟶ U.unop
y : F.val.obj (op V)
e' : NatTrans.app f.val (op V) y = F'.val.map i.op s
E : NatTrans.app (toImageSheaf f).val (op V) y = (imageSheaf f).val.map i.op { val := s, property := hx }
this :
  NatTrans.app g₁.val (op V) (NatTrans.app (toImagePresheafSheafify J f.val) (op V) y) =
    NatTrans.app g₂.val (op V) (NatTrans.app (toImagePresheafSheafify J f.val) (op V) y)
⊢ NatTrans.app g₁.val (op V)
      ((Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf f.val))).map i.op { val := s, property := hx }) =
    NatTrans.app g₂.val (op V)
      ((Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf f.val))).map i.op { val := s, property := hx })
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2.h.e'_5
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : imageSheaf f ⟶ G'
e : toImageSheaf f ≫ g₁ = toImageSheaf f ≫ g₂
U : Cᵒᵖ
s : F'.val.obj U
hx : s ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f.val)) U
V : C
i : V ⟶ U.unop
y : F.val.obj (op V)
e' : NatTrans.app f.val (op V) y = F'.val.map i.op s
E : NatTrans.app (toImageSheaf f).val (op V) y = (imageSheaf f).val.map i.op { val := s, property := hx }
this :
  NatTrans.app g₁.val (op V) (NatTrans.app (toImagePresheafSheafify J f.val) (op V) y) =
    NatTrans.app g₂.val (op V) (NatTrans.app (toImagePresheafSheafify J f.val) (op V) y)
⊢ (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf f.val))).map i.op { val := s, property := hx } =
    NatTrans.app (toImagePresheafSheafify J f.val) (op V) y
[PROOFSTEP]
exact E.symm
[GOAL]
case h.e'_3.h.e'_5
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : imageSheaf f ⟶ G'
e : toImageSheaf f ≫ g₁ = toImageSheaf f ≫ g₂
U : Cᵒᵖ
s : F'.val.obj U
hx : s ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f.val)) U
V : C
i : V ⟶ U.unop
y : F.val.obj (op V)
e' : NatTrans.app f.val (op V) y = F'.val.map i.op s
E : NatTrans.app (toImageSheaf f).val (op V) y = (imageSheaf f).val.map i.op { val := s, property := hx }
this :
  NatTrans.app g₁.val (op V) (NatTrans.app (toImagePresheafSheafify J f.val) (op V) y) =
    NatTrans.app g₂.val (op V) (NatTrans.app (toImagePresheafSheafify J f.val) (op V) y)
⊢ (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf f.val))).map i.op { val := s, property := hx } =
    NatTrans.app (toImagePresheafSheafify J f.val) (op V) y
[PROOFSTEP]
exact E.symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ (imageMonoFactorization f).I ⟶ I.I
[PROOFSTEP]
haveI M := (Sheaf.Hom.mono_iff_presheaf_mono J TypeMax.{v, u} _).mp I.m_mono
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
⊢ (imageMonoFactorization f).I ⟶ I.I
[PROOFSTEP]
haveI := isIso_toImagePresheaf I.m.1
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
⊢ (imageMonoFactorization f).I ⟶ I.I
[PROOFSTEP]
refine' ⟨Subpresheaf.homOfLe _ ≫ inv (toImagePresheaf I.m.1)⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
⊢ Subpresheaf.sheafify J (imagePresheaf f.val) ≤ imagePresheaf I.m.val
[PROOFSTEP]
apply Subpresheaf.sheafify_le
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
⊢ imagePresheaf f.val ≤ imagePresheaf I.m.val
[PROOFSTEP]
conv_lhs => rw [← I.fac]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
| imagePresheaf f.val
[PROOFSTEP]
rw [← I.fac]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
| imagePresheaf f.val
[PROOFSTEP]
rw [← I.fac]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
| imagePresheaf f.val
[PROOFSTEP]
rw [← I.fac]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
⊢ imagePresheaf (I.e ≫ I.m).val ≤ imagePresheaf I.m.val
[PROOFSTEP]
apply imagePresheaf_comp_le
[GOAL]
case hF
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
⊢ Presieve.IsSheaf J F'.val
[PROOFSTEP]
rw [← isSheaf_iff_isSheaf_of_type]
[GOAL]
case hF
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
⊢ Presheaf.IsSheaf J F'.val
[PROOFSTEP]
exact F'.2
[GOAL]
case hG'
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
⊢ Presieve.IsSheaf J (Subpresheaf.toPresheaf (imagePresheaf I.m.val))
[PROOFSTEP]
apply Presieve.isSheaf_iso J (asIso <| toImagePresheaf I.m.1)
[GOAL]
case hG'
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
⊢ Presieve.IsSheaf J I.I.val
[PROOFSTEP]
rw [← isSheaf_iff_isSheaf_of_type]
[GOAL]
case hG'
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.val
this : IsIso (toImagePresheaf I.m.val)
⊢ Presheaf.IsSheaf J I.I.val
[PROOFSTEP]
exact I.I.2
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ (fun I =>
          {
            val :=
              Subpresheaf.homOfLe (_ : Subpresheaf.sheafify J (imagePresheaf f.val) ≤ imagePresheaf I.m.val) ≫
                inv (toImagePresheaf I.m.val) })
        I ≫
      I.m =
    (imageMonoFactorization f).m
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ ((fun I =>
            {
              val :=
                Subpresheaf.homOfLe (_ : Subpresheaf.sheafify J (imagePresheaf f.val) ≤ imagePresheaf I.m.val) ≫
                  inv (toImagePresheaf I.m.val) })
          I ≫
        I.m).val =
    (imageMonoFactorization f).m.val
[PROOFSTEP]
dsimp [imageMonoFactorization]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ (Subpresheaf.homOfLe (_ : Subpresheaf.sheafify J (imagePresheaf f.val) ≤ imagePresheaf I.m.val) ≫
        inv (toImagePresheaf I.m.val)) ≫
      I.m.val =
    Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf f.val))
[PROOFSTEP]
generalize_proofs h
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
h : Subpresheaf.sheafify J (imagePresheaf f.val) ≤ imagePresheaf I.m.val
h✝ : IsIso (toImagePresheaf I.m.val)
⊢ (Subpresheaf.homOfLe (_ : Subpresheaf.sheafify J (imagePresheaf f.val) ≤ imagePresheaf I.m.val) ≫
        inv (toImagePresheaf I.m.val)) ≫
      I.m.val =
    Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf f.val))
[PROOFSTEP]
rw [← Subpresheaf.homOfLe_ι h, Category.assoc]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
h : Subpresheaf.sheafify J (imagePresheaf f.val) ≤ imagePresheaf I.m.val
h✝ : IsIso (toImagePresheaf I.m.val)
⊢ Subpresheaf.homOfLe (_ : Subpresheaf.sheafify J (imagePresheaf f.val) ≤ imagePresheaf I.m.val) ≫
      inv (toImagePresheaf I.m.val) ≫ I.m.val =
    Subpresheaf.homOfLe h ≫ Subpresheaf.ι (imagePresheaf I.m.val)
[PROOFSTEP]
congr 1
[GOAL]
case h.e_a
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J TypeMax
f : F ⟶ F'
I : Limits.MonoFactorisation f
h : Subpresheaf.sheafify J (imagePresheaf f.val) ≤ imagePresheaf I.m.val
h✝ : IsIso (toImagePresheaf I.m.val)
⊢ inv (toImagePresheaf I.m.val) ≫ I.m.val = Subpresheaf.ι (imagePresheaf I.m.val)
[PROOFSTEP]
rw [IsIso.inv_comp_eq, toImagePresheaf_ι]
