[GOAL]
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
w :
  ∀ (x : { x // x ∈ U }),
    ∃ V x i,
      PrelocalPredicate.pred
        { pred := fun {U} => PrelocalPredicate.pred src✝,
          res :=
            (_ :
              ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
                PrelocalPredicate.pred src✝ f →
                  PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ PrelocalPredicate.pred
    { pred := fun {U} => PrelocalPredicate.pred src✝,
      res :=
        (_ :
          ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
            PrelocalPredicate.pred src✝ f →
              PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
    f
[PROOFSTEP]
apply continuous_iff_continuousAt.2
[GOAL]
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
w :
  ∀ (x : { x // x ∈ U }),
    ∃ V x i,
      PrelocalPredicate.pred
        { pred := fun {U} => PrelocalPredicate.pred src✝,
          res :=
            (_ :
              ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
                PrelocalPredicate.pred src✝ f →
                  PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ∀ (x : { x // x ∈ U }), ContinuousAt f x
[PROOFSTEP]
intro x
[GOAL]
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
w :
  ∀ (x : { x // x ∈ U }),
    ∃ V x i,
      PrelocalPredicate.pred
        { pred := fun {U} => PrelocalPredicate.pred src✝,
          res :=
            (_ :
              ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
                PrelocalPredicate.pred src✝ f →
                  PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
x : { x // x ∈ U }
⊢ ContinuousAt f x
[PROOFSTEP]
specialize w x
[GOAL]
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
x : { x // x ∈ U }
w :
  ∃ V x i,
    PrelocalPredicate.pred
      { pred := fun {U} => PrelocalPredicate.pred src✝,
        res :=
          (_ :
            ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
              PrelocalPredicate.pred src✝ f →
                PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
      fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ContinuousAt f x
[PROOFSTEP]
rcases w with ⟨V, m, i, w⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w :
  PrelocalPredicate.pred
    { pred := fun {U} => PrelocalPredicate.pred src✝,
      res :=
        (_ :
          ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
            PrelocalPredicate.pred src✝ f →
              PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
    fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ContinuousAt f x
[PROOFSTEP]
dsimp at w 
[GOAL]
case intro.intro.intro
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : Continuous fun x => f { val := ↑x, property := (_ : ↑x ∈ ↑U) }
⊢ ContinuousAt f x
[PROOFSTEP]
rw [continuous_iff_continuousAt] at w 
[GOAL]
case intro.intro.intro
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : ∀ (x : { x // x ∈ V }), ContinuousAt (fun x => f { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x
⊢ ContinuousAt f x
[PROOFSTEP]
specialize w ⟨x, m⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : ContinuousAt (fun x => f { val := ↑x, property := (_ : ↑x ∈ ↑U) }) { val := ↑x, property := m }
⊢ ContinuousAt f x
[PROOFSTEP]
simpa using (Opens.openEmbedding_of_le i.le).continuousAt_iff.1 w
[GOAL]
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : { x // x ∈ U }) → T ↑x
w :
  (fun {U} f =>
      ∀ (x : { x // x ∈ U }), ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
    f
x : { x // x ∈ V }
⊢ ∃ V_1 x i_1,
    pred P fun x =>
      (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
[PROOFSTEP]
specialize w (i x)
[GOAL]
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ V }
w : ∃ V_1 x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ∃ V_1 x i_1,
    pred P fun x =>
      (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
[PROOFSTEP]
rcases w with ⟨V', m', i', p⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ V }
V' : Opens ↑X
m' : ↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x) ∈ V'
i' : V' ⟶ U
p : pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ∃ V_1 x i_1,
    pred P fun x =>
      (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
[PROOFSTEP]
refine' ⟨V ⊓ V', ⟨x.2, m'⟩, Opens.infLELeft _ _, _⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ V }
V' : Opens ↑X
m' : ↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x) ∈ V'
i' : V' ⟶ U
p : pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ pred P fun x =>
    (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
[PROOFSTEP]
convert P.res (Opens.infLERight V V') _ p
[GOAL]
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
w :
  ∀ (x : { x // x ∈ U }),
    ∃ V x i,
      pred
        {
          pred := fun {U} f =>
            ∀ (x : { x // x ∈ U }), ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x),
          res :=
            (_ :
              ∀ {V U : Opens ↑X} (i : V ⟶ U) (f : (x : { x // x ∈ U }) → T ↑x),
                (∀ (x : { x // x ∈ U }),
                    ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)) →
                  ∀ (x : { x // x ∈ V }),
                    ∃ V_1 x i_1,
                      pred P fun x =>
                        (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
                          ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
x : { x // x ∈ U }
⊢ ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
specialize w x
[GOAL]
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ U }
w :
  ∃ V x i,
    pred
      {
        pred := fun {U} f =>
          ∀ (x : { x // x ∈ U }), ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x),
        res :=
          (_ :
            ∀ {V U : Opens ↑X} (i : V ⟶ U) (f : (x : { x // x ∈ U }) → T ↑x),
              (∀ (x : { x // x ∈ U }),
                  ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)) →
                ∀ (x : { x // x ∈ V }),
                  ∃ V_1 x i_1,
                    pred P fun x =>
                      (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
                        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
      fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
rcases w with ⟨V, m, i, p⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
p :
  pred
    {
      pred := fun {U} f =>
        ∀ (x : { x // x ∈ U }), ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x),
      res :=
        (_ :
          ∀ {V U : Opens ↑X} (i : V ⟶ U) (f : (x : { x // x ∈ U }) → T ↑x),
            (∀ (x : { x // x ∈ U }),
                ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)) →
              ∀ (x : { x // x ∈ V }),
                ∃ V_1 x i_1,
                  pred P fun x =>
                    (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
                      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
    fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
specialize p ⟨x.1, m⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
p :
  ∃ V_1 x i_1,
    pred P fun x =>
      (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
⊢ ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
rcases p with ⟨V', m', i', p'⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
V' : Opens ↑X
m' : ↑{ val := ↑x, property := m } ∈ V'
i' : V' ⟶ V
p' :
  pred P fun x =>
    (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
⊢ ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
exact ⟨V', m', i' ≫ i, p'⟩
[GOAL]
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
h : pred P f
x : { x // x ∈ U }
⊢ pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
convert h
[GOAL]
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
[PROOFSTEP]
let sf' : ∀ i : ι, (presheafToTypes X T).obj (op (U i)) := fun i => (sf i).val
[GOAL]
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
[PROOFSTEP]
have sf'_comp : (presheafToTypes X T).IsCompatible U sf' := fun i j =>
  congr_arg Subtype.val
    (sf_comp i j)
      -- So, we can obtain a unique gluing
[GOAL]
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
[PROOFSTEP]
obtain ⟨gl, gl_spec, gl_uniq⟩ := (sheafToTypes X T).existsUnique_gluing U sf' sf'_comp
[GOAL]
case intro.intro
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
[PROOFSTEP]
refine' ⟨⟨gl, _⟩, _, _⟩
[GOAL]
case intro.intro.refine'_1
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ PrelocalPredicate.pred P.toPrelocalPredicate gl
[PROOFSTEP]
apply P.locality
[GOAL]
case intro.intro.refine'_1.x
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∀ (x : { x // x ∈ (op (iSup U)).unop }),
    ∃ V x i,
      PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
        gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op (iSup U)).unop) }) x)
[PROOFSTEP]
rintro
  ⟨x, mem⟩
      -- Once we're at a particular point `x`, we can select some open set `x ∈ U i`.
[GOAL]
case intro.intro.refine'_1.x.mk
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (op (iSup U)).unop
⊢ ∃ V x i,
    PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
      gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op (iSup U)).unop) }) x)
[PROOFSTEP]
choose i hi using Opens.mem_iSup.mp mem
[GOAL]
case intro.intro.refine'_1.x.mk
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (op (iSup U)).unop
i : ι
hi : x ∈ U i
⊢ ∃ V x i,
    PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
      gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op (iSup U)).unop) }) x)
[PROOFSTEP]
use U i, hi, Opens.leSupr U i
[GOAL]
case h
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (op (iSup U)).unop
i : ι
hi : x ∈ U i
⊢ PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
    gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op (iSup U)).unop) }) x)
[PROOFSTEP]
convert (sf i).property using 1
[GOAL]
case h.e'_5.h
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (op (iSup U)).unop
i : ι
hi : x ∈ U i
e_4✝ : U i = (op (U i)).unop
⊢ (fun x => gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op (iSup U)).unop) }) x)) = ↑(sf i)
[PROOFSTEP]
exact gl_spec i
[GOAL]
case intro.intro.refine'_2
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ (fun s => IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s)
    { val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
[PROOFSTEP]
exact fun i => Subtype.ext (gl_spec i)
[GOAL]
case intro.intro.refine'_3
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∀ (y : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))),
    (fun s => IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s) y →
      y = { val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
[PROOFSTEP]
intro gl' hgl'
[GOAL]
case intro.intro.refine'_3
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
gl' : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))
hgl' : IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf gl'
⊢ gl' = { val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
[PROOFSTEP]
refine Subtype.ext ?_
[GOAL]
case intro.intro.refine'_3
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
gl' : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))
hgl' : IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf gl'
⊢ ↑gl' = ↑{ val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
[PROOFSTEP]
exact gl_uniq gl'.1 fun i => congr_arg Subtype.val (hgl' i)
[GOAL]
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
⊢ Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x ⟶ T x
[PROOFSTEP]
refine'
  colimit.desc _
    { pt := T x
      ι :=
        { app := fun U f => _
          naturality := _ } }
[GOAL]
case refine'_1
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
f :
  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
        (Sheaf.presheaf (subsheafToTypes P))).obj
    U
⊢ ((Functor.const (OpenNhds x)ᵒᵖ).obj (T x)).obj U
[PROOFSTEP]
exact f.1 ⟨x, (unop U).2⟩
[GOAL]
case refine'_2
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
⊢ ∀ ⦃X_1 Y : (OpenNhds x)ᵒᵖ⦄ (f : X_1 ⟶ Y),
    (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
              (Sheaf.presheaf (subsheafToTypes P))).map
          f ≫
        (fun U f => ↑f { val := x, property := (_ : x ∈ U.unop.obj) }) Y =
      (fun U f => ↑f { val := x, property := (_ : x ∈ U.unop.obj) }) X_1 ≫
        ((Functor.const (OpenNhds x)ᵒᵖ).obj (T x)).map f
[PROOFSTEP]
aesop
[GOAL]
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
x : { x // x ∈ U }
f : (Sheaf.presheaf (subsheafToTypes P)).obj (op U)
⊢ stalkToFiber P (↑x) (Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) x f) = ↑f x
[PROOFSTEP]
dsimp [Presheaf.germ, stalkToFiber]
[GOAL]
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
x : { x // x ∈ U }
f : (Sheaf.presheaf (subsheafToTypes P)).obj (op U)
⊢ colimit.desc ((OpenNhds.inclusion ↑x).op ⋙ subpresheafToTypes P.toPrelocalPredicate)
      { pt := T ↑x, ι := NatTrans.mk fun U_1 f => ↑f { val := ↑x, property := (_ : ↑x ∈ U_1.unop.obj) } }
      (colimit.ι ((OpenNhds.inclusion ↑x).op ⋙ subpresheafToTypes P.toPrelocalPredicate)
        (op { obj := U, property := (_ : ↑x ∈ U) }) f) =
    ↑f x
[PROOFSTEP]
cases x
[GOAL]
case mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
f : (Sheaf.presheaf (subsheafToTypes P)).obj (op U)
val✝ : ↑X
property✝ : val✝ ∈ U
⊢ colimit.desc
      ((OpenNhds.inclusion ↑{ val := val✝, property := property✝ }).op ⋙ subpresheafToTypes P.toPrelocalPredicate)
      { pt := T ↑{ val := val✝, property := property✝ },
        ι :=
          NatTrans.mk fun U_1 f =>
            ↑f
              { val := ↑{ val := val✝, property := property✝ },
                property := (_ : ↑{ val := val✝, property := property✝ } ∈ U_1.unop.obj) } }
      (colimit.ι
        ((OpenNhds.inclusion ↑{ val := val✝, property := property✝ }).op ⋙ subpresheafToTypes P.toPrelocalPredicate)
        (op { obj := U, property := (_ : ↑{ val := val✝, property := property✝ } ∈ U) }) f) =
    ↑f { val := val✝, property := property✝ }
[PROOFSTEP]
simp
[GOAL]
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
t : T x
⊢ ∃ a, stalkToFiber P x a = t
[PROOFSTEP]
rcases w t with ⟨U, f, h, rfl⟩
[GOAL]
case intro.intro.intro
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ ∃ a, stalkToFiber P x a = f { val := x, property := (_ : x ∈ U.obj) }
[PROOFSTEP]
fconstructor
[GOAL]
case intro.intro.intro.w
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
[PROOFSTEP]
exact (subsheafToTypes P).presheaf.germ ⟨x, U.2⟩ ⟨f, h⟩
[GOAL]
case intro.intro.intro.h
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ stalkToFiber P x
      (Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ U.obj) }
        { val := f, property := h }) =
    f { val := x, property := (_ : x ∈ U.obj) }
[PROOFSTEP]
exact stalkToFiber_germ _ U.1 ⟨x, U.2⟩ ⟨f, h⟩
[GOAL]
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.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)
tU tV : Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
h : stalkToFiber P x tU = stalkToFiber P x tV
⊢ tU = tV
[PROOFSTEP]
let Q :
  ∃ (W : (OpenNhds x)ᵒᵖ) (s : ∀ w : (unop W).1, T w) (hW : P.pred s),
    tU = (subsheafToTypes P).presheaf.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ ∧
      tV = (subsheafToTypes P).presheaf.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ :=
  ?_
[GOAL]
case refine_2
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.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)
tU tV : Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
h : stalkToFiber P x tU = stalkToFiber P x tV
Q : ∃ W s hW,
  tU =
      Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
        { val := s, property := hW } ∧
    tV =
      Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
        { val := s, property := hW } :=
  ?refine_1
⊢ tU = tV
[PROOFSTEP]
choose W s hW e using Q
[GOAL]
case refine_2
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.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)
tU tV : Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
h : stalkToFiber P x tU = stalkToFiber P x tV
W : (OpenNhds x)ᵒᵖ
s : (w : { x_1 // x_1 ∈ W.unop.obj }) → T ↑w
hW : PrelocalPredicate.pred P.toPrelocalPredicate s
e :
  tU =
      Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
        { val := s, property := hW } ∧
    tV =
      Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
        { val := s, property := hW }
⊢ tU = tV
[PROOFSTEP]
exact e.1.trans e.2.symm
[GOAL]
case refine_1
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.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)
tU tV : Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
h : stalkToFiber P x tU = stalkToFiber P x tV
⊢ ∃ W s hW,
    tU =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      tV =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
obtain ⟨U, ⟨fU, hU⟩, rfl⟩ := jointly_surjective'.{v, v} tU
[GOAL]
case refine_1.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.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)
tV : Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
h :
  stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (Sheaf.presheaf (subsheafToTypes P)))
        U { val := fU, property := hU }) =
    stalkToFiber P x tV
⊢ ∃ W s hW,
    colimit.ι
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
            (Sheaf.presheaf (subsheafToTypes P)))
          U { val := fU, property := hU } =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      tV =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
obtain ⟨V, ⟨fV, hV⟩, rfl⟩ := jointly_surjective'.{v, v} tV
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.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)
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h :
  stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (Sheaf.presheaf (subsheafToTypes P)))
        U { val := fU, property := hU }) =
    stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (Sheaf.presheaf (subsheafToTypes P)))
        V { val := fV, property := hV })
⊢ ∃ W s hW,
    colimit.ι
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
            (Sheaf.presheaf (subsheafToTypes P)))
          U { val := fU, property := hU } =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      colimit.ι
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
            (Sheaf.presheaf (subsheafToTypes P)))
          V { val := fV, property := hV } =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
dsimp
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.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)
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h :
  stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (Sheaf.presheaf (subsheafToTypes P)))
        U { val := fU, property := hU }) =
    stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (Sheaf.presheaf (subsheafToTypes P)))
        V { val := fV, property := hV })
⊢ ∃ W s hW,
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
simp only [stalkToFiber, Types.Colimit.ι_desc_apply'] at h 
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.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)
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
⊢ ∃ W s hW,
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
specialize w (unop U) (unop V) fU hU fV hV h
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
w :
  ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ ∃ W s hW,
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
rcases w with
  ⟨W, iU, iV, w⟩
    -- and put it back together again in the correct order.
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
W : OpenNhds x
iU : W ⟶ U.unop
iV : W ⟶ V.unop
w :
  ∀ (w : { x_1 // x_1 ∈ W.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ ∃ W s hW,
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
refine' ⟨op W, fun w => fU (iU w : (unop U).1), P.res _ _ hU, _⟩
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro.refine'_1
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
W : OpenNhds x
iU : W ⟶ U.unop
iV : W ⟶ V.unop
w :
  ∀ (w : { x_1 // x_1 ∈ W.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ (op W).unop.obj ⟶ U.unop.obj
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro.refine'_2
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
W : OpenNhds x
iU : W ⟶ U.unop
iV : W ⟶ V.unop
w :
  ∀ (w : { x_1 // x_1 ∈ W.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
      Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ (op W).unop.obj) }
        { val := fun w => fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w),
          property :=
            (_ :
              PrelocalPredicate.pred P.toPrelocalPredicate fun x_1 =>
                fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.unop.obj) }) x_1)) } ∧
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
      Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ (op W).unop.obj) }
        { val := fun w => fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w),
          property :=
            (_ :
              PrelocalPredicate.pred P.toPrelocalPredicate fun x_1 =>
                fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.unop.obj) }) x_1)) }
[PROOFSTEP]
rcases W with ⟨W, m⟩
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro.refine'_1.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
W : Opens ↑X
m : x ∈ W
iU : { obj := W, property := m } ⟶ U.unop
iV : { obj := W, property := m } ⟶ V.unop
w :
  ∀ (w : { x_1 // x_1 ∈ { obj := W, property := m }.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ (op { obj := W, property := m }).unop.obj ⟶ U.unop.obj
[PROOFSTEP]
exact iU
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro.refine'_2
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
W : OpenNhds x
iU : W ⟶ U.unop
iV : W ⟶ V.unop
w :
  ∀ (w : { x_1 // x_1 ∈ W.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
      Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ (op W).unop.obj) }
        { val := fun w => fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w),
          property :=
            (_ :
              PrelocalPredicate.pred P.toPrelocalPredicate fun x_1 =>
                fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.unop.obj) }) x_1)) } ∧
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
      Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ (op W).unop.obj) }
        { val := fun w => fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w),
          property :=
            (_ :
              PrelocalPredicate.pred P.toPrelocalPredicate fun x_1 =>
                fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.unop.obj) }) x_1)) }
[PROOFSTEP]
exact ⟨colimit_sound iU.op (Subtype.eq rfl), colimit_sound iV.op (Subtype.eq (funext w).symm)⟩
[GOAL]
X✝ : TopCat
T✝ : ↑X✝ → Type v
T : TopCat
X : (Opens ↑X✝)ᵒᵖ
⊢ (subpresheafToTypes (continuousPrelocal X✝ T)).obj X ⟶ (presheafToTop X✝ T).obj X
[PROOFSTEP]
rintro ⟨f, c⟩
[GOAL]
case mk
X✝ : TopCat
T✝ : ↑X✝ → Type v
T : TopCat
X : (Opens ↑X✝)ᵒᵖ
f : (x : { x // x ∈ X.unop }) → (fun x => ↑T) ↑x
c : PrelocalPredicate.pred (continuousPrelocal X✝ T) f
⊢ (presheafToTop X✝ T).obj X
[PROOFSTEP]
exact ⟨f, c⟩
[GOAL]
X✝ : TopCat
T✝ : ↑X✝ → Type v
T : TopCat
X : (Opens ↑X✝)ᵒᵖ
⊢ (presheafToTop X✝ T).obj X ⟶ (subpresheafToTypes (continuousPrelocal X✝ T)).obj X
[PROOFSTEP]
rintro ⟨f, c⟩
[GOAL]
case mk
X✝ : TopCat
T✝ : ↑X✝ → Type v
T : TopCat
X : (Opens ↑X✝)ᵒᵖ
f : ↑((Opens.toTopCat X✝).op.obj X).unop → ↑T
c : Continuous f
⊢ (subpresheafToTypes (continuousPrelocal X✝ T)).obj X
[PROOFSTEP]
exact ⟨f, c⟩
