[GOAL]
X : TopCat
F : Presheaf (Type v) X
U U' : (Opens ↑X)ᵒᵖ
f : U ⟶ U'
⊢ F.map f ≫
      (fun U f =>
          { val := fun x => germ F x f,
            property :=
              (_ :
                PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                  germ F x f) })
        U' =
    (fun U f =>
          { val := fun x => germ F x f,
            property :=
              (_ :
                PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                  germ F x f) })
        U ≫
      (sheafify F).val.map f
[PROOFSTEP]
ext x
[GOAL]
case h
X : TopCat
F : Presheaf (Type v) X
U U' : (Opens ↑X)ᵒᵖ
f : U ⟶ U'
x : F.obj U
⊢ (F.map f ≫
        (fun U f =>
            { val := fun x => germ F x f,
              property :=
                (_ :
                  PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                    germ F x f) })
          U')
      x =
    ((fun U f =>
            { val := fun x => germ F x f,
              property :=
                (_ :
                  PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                    germ F x f) })
          U ≫
        (sheafify F).val.map f)
      x
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case h.a
X : TopCat
F : Presheaf (Type v) X
U U' : (Opens ↑X)ᵒᵖ
f : U ⟶ U'
x : F.obj U
⊢ ↑((F.map f ≫
          (fun U f =>
              { val := fun x => germ F x f,
                property :=
                  (_ :
                    PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                      germ F x f) })
            U')
        x) =
    ↑(((fun U f =>
              { val := fun x => germ F x f,
                property :=
                  (_ :
                    PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                      germ F x f) })
            U ≫
          (sheafify F).val.map f)
        x)
[PROOFSTEP]
ext ⟨u, m⟩
[GOAL]
case h.a.h.mk
X : TopCat
F : Presheaf (Type v) X
U U' : (Opens ↑X)ᵒᵖ
f : U ⟶ U'
x : F.obj U
u : ↑X
m : u ∈ U'.unop
⊢ ↑((F.map f ≫
            (fun U f =>
                { val := fun x => germ F x f,
                  property :=
                    (_ :
                      PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate
                        fun x => germ F x f) })
              U')
          x)
      { val := u, property := m } =
    ↑(((fun U f =>
                { val := fun x => germ F x f,
                  property :=
                    (_ :
                      PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate
                        fun x => germ F x f) })
              U ≫
            (sheafify F).val.map f)
          x)
      { val := u, property := m }
[PROOFSTEP]
exact germ_res_apply F f.unop ⟨u, m⟩ x
[GOAL]
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ Function.Surjective (stalkToFiber F x)
[PROOFSTEP]
apply TopCat.stalkToFiber_surjective
[GOAL]
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ ∀ (t : stalk F x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
[PROOFSTEP]
intro t
[GOAL]
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
t : stalk F x
⊢ ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
[PROOFSTEP]
obtain ⟨U, m, s, rfl⟩ := F.germ_exist _ t
[GOAL]
case w.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (forget (Type v)).obj (F.obj (op U))
⊢ ∃ U_1 f x_1, f { val := x, property := (_ : x ∈ U_1.obj) } = ↑(germ F { val := x, property := m }) s
[PROOFSTEP]
use⟨U, m⟩
[GOAL]
case h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (forget (Type v)).obj (F.obj (op U))
⊢ ∃ f x_1,
    f { val := x, property := (_ : x ∈ { obj := U, property := m }.obj) } = ↑(germ F { val := x, property := m }) s
[PROOFSTEP]
fconstructor
[GOAL]
case h.w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (forget (Type v)).obj (F.obj (op U))
⊢ (y : { x_1 // x_1 ∈ { obj := U, property := m }.obj }) → stalk F ↑y
[PROOFSTEP]
exact fun y => F.germ y s
[GOAL]
case h.h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (forget (Type v)).obj (F.obj (op U))
⊢ ∃ x_1,
    germ F { val := x, property := (_ : x ∈ { obj := U, property := m }.obj) } s =
      ↑(germ F { val := x, property := m }) s
[PROOFSTEP]
exact ⟨PrelocalPredicate.sheafifyOf ⟨s, fun _ => rfl⟩, rfl⟩
[GOAL]
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ Function.Injective (stalkToFiber F x)
[PROOFSTEP]
apply TopCat.stalkToFiber_injective
[GOAL]
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y),
    PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → stalk F ↑y),
        PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV →
          fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) } →
            ∃ W iU iV,
              ∀ (w : { x_4 // x_4 ∈ W.obj }),
                fU ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑U.obj) }) w) =
                  fV ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑V.obj) }) w)
[PROOFSTEP]
intro U V fU hU fV hV e
[GOAL]
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
e : fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) }
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
rcases hU ⟨x, U.2⟩ with ⟨U', mU, iU, gU, wU⟩
[GOAL]
case w.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
e : fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) }
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
rcases hV ⟨x, V.2⟩ with ⟨V', mV, iV, gV, wV⟩
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
e : fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) }
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
have wUx := wU ⟨x, mU⟩
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
e : fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) }
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wUx :
  (fun x_1 => fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.obj) }) x_1)) { val := x, property := mU } =
    germ F { val := x, property := mU } gU
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
dsimp at wUx 
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
e : fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) }
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wUx : fU { val := x, property := (_ : ↑{ val := x, property := mU } ∈ ↑U.obj) } = germ F { val := x, property := mU } gU
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
erw [wUx] at e 
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : germ F { val := x, property := mU } gU = fV { val := x, property := (_ : x ∈ V.obj) }
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wUx : fU { val := x, property := (_ : ↑{ val := x, property := mU } ∈ ↑U.obj) } = germ F { val := x, property := mU } gU
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
clear wUx
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : germ F { val := x, property := mU } gU = fV { val := x, property := (_ : x ∈ V.obj) }
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
have wVx := wV ⟨x, mV⟩
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : germ F { val := x, property := mU } gU = fV { val := x, property := (_ : x ∈ V.obj) }
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wVx :
  (fun x_1 => fV ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑V.obj) }) x_1)) { val := x, property := mV } =
    germ F { val := x, property := mV } gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
dsimp at wVx 
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : germ F { val := x, property := mU } gU = fV { val := x, property := (_ : x ∈ V.obj) }
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wVx : fV { val := x, property := (_ : ↑{ val := x, property := mV } ∈ ↑V.obj) } = germ F { val := x, property := mV } gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
erw [wVx] at e 
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wVx : fV { val := x, property := (_ : ↑{ val := x, property := mV } ∈ ↑V.obj) } = germ F { val := x, property := mV } gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
clear wVx
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
rcases F.germ_eq x mU mV gU gV e with ⟨W, mW, iU', iV', (e' : F.map iU'.op gU = F.map iV'.op gV)⟩
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
use⟨W ⊓ (U' ⊓ V'), ⟨mW, mU, mV⟩⟩
[GOAL]
case h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ ∃ iU iV,
    ∀ (w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
refine' ⟨_, _, _⟩
[GOAL]
case h.refine'_1
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) } ⟶ U
[PROOFSTEP]
change W ⊓ (U' ⊓ V') ⟶ U.obj
[GOAL]
case h.refine'_1
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ W ⊓ (U' ⊓ V') ⟶ U.obj
[PROOFSTEP]
exact Opens.infLERight _ _ ≫ Opens.infLELeft _ _ ≫ iU
[GOAL]
case h.refine'_2
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) } ⟶ V
[PROOFSTEP]
change W ⊓ (U' ⊓ V') ⟶ V.obj
[GOAL]
case h.refine'_2
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ W ⊓ (U' ⊓ V') ⟶ V.obj
[PROOFSTEP]
exact Opens.infLERight _ _ ≫ Opens.infLERight _ _ ≫ iV
[GOAL]
case h.refine'_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ ∀ (w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
intro w
[GOAL]
case h.refine'_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }
⊢ fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
    fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
specialize wU ⟨w.1, w.2.2.1⟩
[GOAL]
case h.refine'_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }
wU :
  (fun x_1 => fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.obj) }) x_1))
      { val := ↑w, property := (_ : ↑w ∈ ↑U') } =
    germ F { val := ↑w, property := (_ : ↑w ∈ ↑U') } gU
⊢ fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
    fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
specialize wV ⟨w.1, w.2.2.2⟩
[GOAL]
case h.refine'_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }
wU :
  (fun x_1 => fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.obj) }) x_1))
      { val := ↑w, property := (_ : ↑w ∈ ↑U') } =
    germ F { val := ↑w, property := (_ : ↑w ∈ ↑U') } gU
wV :
  (fun x_1 => fV ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑V.obj) }) x_1))
      { val := ↑w, property := (_ : ↑w ∈ ↑V') } =
    germ F { val := ↑w, property := (_ : ↑w ∈ ↑V') } gV
⊢ fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
    fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
dsimp at wU wV ⊢
[GOAL]
case h.refine'_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }
wU :
  fU { val := ↑w, property := (_ : ↑{ val := ↑w, property := (_ : ↑w ∈ ↑U') } ∈ ↑U.obj) } =
    germ F { val := ↑w, property := (_ : ↑w ∈ ↑U') } gU
wV :
  fV { val := ↑w, property := (_ : ↑{ val := ↑w, property := (_ : ↑w ∈ ↑V') } ∈ ↑V.obj) } =
    germ F { val := ↑w, property := (_ : ↑w ∈ ↑V') } gV
⊢ fU { val := ↑w, property := (_ : ↑w ∈ ↑U.obj) } = fV { val := ↑w, property := (_ : ↑w ∈ ↑V.obj) }
[PROOFSTEP]
erw [wU, ← F.germ_res iU' ⟨w, w.2.1⟩, wV, ← F.germ_res iV' ⟨w, w.2.1⟩, CategoryTheory.types_comp_apply,
  CategoryTheory.types_comp_apply, e']
