X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
⊢ ∃! s, IsGluing (presheafToTypes X T) U sf s
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
⊢ ∃! s, IsGluing (presheafToTypes X T) U sf s
choose index index_spec using fun x : ↑(iSup U) => Opens.mem_iSup.mp x.2
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
⊢ ∃! s, IsGluing (presheafToTypes X T) U sf s
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
⊢ ∃! s, IsGluing (presheafToTypes X T) U sf s
let s : ∀ x : ↑(iSup U), T x := fun x => sf (index x) ⟨x.1, index_spec x⟩
case refine'_1
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
⊢ (fun s => IsGluing (presheafToTypes X T) U sf s) s

case refine'_2
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
⊢ ∀ (y : (forget (Type u)).obj ((presheafToTypes X T).obj (iSup U).op)),
    (fun s => IsGluing (presheafToTypes X T) U sf s) y → y = s
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
⊢ ∃! s, IsGluing (presheafToTypes X T) U sf s
refine' ⟨s, _, _⟩
case refine'_1
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
i : ι
⊢ (forget (Type u)).map ((presheafToTypes X T).map (leSupr U i).op) s = sf i
case refine'_1
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
⊢ (fun s => IsGluing (presheafToTypes X T) U sf s) s
intro i
case refine'_1.h
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
i : ι
x : { x // x ∈ (U i).op.unop }
⊢ (forget (Type u)).map ((presheafToTypes X T).map (leSupr U i).op) s x = sf i x
case refine'_1
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
i : ι
⊢ (forget (Type u)).map ((presheafToTypes X T).map (leSupr U i).op) s = sf i
funext x
no goals
case refine'_1.h
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
i : ι
x : { x // x ∈ (U i).op.unop }
⊢ (forget (Type u)).map ((presheafToTypes X T).map (leSupr U i).op) s x = sf i x
exact congr_fun (hsf (index ⟨x, _⟩) i) ⟨x, ⟨index_spec ⟨x.1, _⟩, x.2⟩⟩
case refine'_2
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
t : (forget (Type u)).obj ((presheafToTypes X T).obj (iSup U).op)
ht : IsGluing (presheafToTypes X T) U sf t
⊢ t = s
case refine'_2
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
⊢ ∀ (y : (forget (Type u)).obj ((presheafToTypes X T).obj (iSup U).op)),
    (fun s => IsGluing (presheafToTypes X T) U sf s) y → y = s
intro t ht
case refine'_2.h
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
t : (forget (Type u)).obj ((presheafToTypes X T).obj (iSup U).op)
ht : IsGluing (presheafToTypes X T) U sf t
x : { x // x ∈ (iSup U).op.unop }
⊢ t x = s x
case refine'_2
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
t : (forget (Type u)).obj ((presheafToTypes X T).obj (iSup U).op)
ht : IsGluing (presheafToTypes X T) U sf t
⊢ t = s
funext x
no goals
case refine'_2.h
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (U i).op)
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
t : (forget (Type u)).obj ((presheafToTypes X T).obj (iSup U).op)
ht : IsGluing (presheafToTypes X T) U sf t
x : { x // x ∈ (iSup U).op.unop }
⊢ t x = s x
exact congr_fun (ht (index x)) ⟨x.1, index_spec x⟩