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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
let sf' : ∀ i : ι, (presheafToTypes X T).obj (op (U i)) := fun i => (sf i).val
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
have sf'_comp : (presheafToTypes X T).IsCompatible U sf' := fun i j =>
  congr_arg Subtype.val (sf_comp i j)
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
obtain ⟨gl, gl_spec, gl_uniq⟩ := (sheafToTypes X T).existsUnique_gluing U sf' sf'_comp
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ PrelocalPredicate.pred P.toPrelocalPredicate gl

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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (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 := ?intro.intro.refine'_1 }

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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∀ (y : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (iSup U).op)),
    (fun s => IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s) y →
      y = { val := gl, property := ?intro.intro.refine'_1 }
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
refine' ⟨⟨gl, _⟩, _, _⟩
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∀ (x : { x // x ∈ (iSup U).op.unop }),
    ∃ V x i,
      PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
        gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(iSup U).op.unop) }) x)
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ PrelocalPredicate.pred P.toPrelocalPredicate gl
apply P.locality
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (iSup U).op.unop
⊢ ∃ V x i,
    PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
      gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(iSup U).op.unop) }) x)
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∀ (x : { x // x ∈ (iSup U).op.unop }),
    ∃ V x i,
      PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
        gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(iSup U).op.unop) }) x)
rintro ⟨x, mem⟩
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (iSup U).op.unop
i : ι
hi : x ∈ U i
⊢ ∃ V x i,
    PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
      gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(iSup U).op.unop) }) x)
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (iSup U).op.unop
⊢ ∃ V x i,
    PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
      gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(iSup U).op.unop) }) x)
choose i hi using Opens.mem_iSup.mp mem
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (iSup U).op.unop
i : ι
hi : x ∈ U i
⊢ PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
    gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(iSup U).op.unop) }) x)
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (iSup U).op.unop
i : ι
hi : x ∈ U i
⊢ ∃ V x i,
    PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
      gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(iSup U).op.unop) }) x)
use U i, hi, Opens.leSupr U i
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (iSup U).op.unop
i : ι
hi : x ∈ U i
e_4✝ : U i = (U i).op.unop
⊢ (fun x => gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(iSup U).op.unop) }) x)) = ↑(sf i)
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (iSup U).op.unop
i : ι
hi : x ∈ U i
⊢ PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
    gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(iSup U).op.unop) }) x)
convert (sf i).property using 1
no goals
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (iSup U).op.unop
i : ι
hi : x ∈ U i
e_4✝ : U i = (U i).op.unop
⊢ (fun x => gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(iSup U).op.unop) }) x)) = ↑(sf i)
exact gl_spec i
no goals
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (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) }
exact fun i => Subtype.ext (gl_spec i)
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
gl' : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (iSup U).op)
hgl' : IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf gl'
⊢ gl' = { val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∀ (y : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (iSup U).op)),
    (fun s => IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s) y →
      y = { val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
intro gl' hgl'
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
gl' : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (iSup U).op)
hgl' : IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf gl'
⊢ ↑gl' = ↑{ val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
gl' : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (iSup U).op)
hgl' : IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf gl'
⊢ gl' = { val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
refine Subtype.ext ?_
no goals
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 (U i).op)
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (U i).op := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (iSup U).op)),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
gl' : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (iSup U).op)
hgl' : IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf gl'
⊢ ↑gl' = ↑{ val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
exact gl_uniq gl'.1 fun i => congr_arg Subtype.val (hgl' i)