case mp
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : IsGluing F U ((piOpensIsoSectionsFamily F U).hom sf) s
⊢ res F U s = sf

case mpr
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : res F U s = sf
⊢ IsGluing F U ((piOpensIsoSectionsFamily F U).hom sf) s
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
⊢ IsGluing F U ((piOpensIsoSectionsFamily F U).hom sf) s ↔ res F U s = sf
constructor <;> intro h
case mp
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : IsGluing F U ((piOpensIsoSectionsFamily F U).hom sf) s
x✝ : Discrete ι
i : ι
⊢ limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i } (res F U s) =
    limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i } sf
case mp
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : IsGluing F U ((piOpensIsoSectionsFamily F U).hom sf) s
⊢ res F U s = sf
refine Types.limit_ext' _ _ _ fun ⟨i⟩ => ?_
case mp
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : IsGluing F U ((piOpensIsoSectionsFamily F U).hom sf) s
x✝ : Discrete ι
i : ι
⊢ F.map (leSupr U { as := i }.as).op s = limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i } sf
case mp
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : IsGluing F U ((piOpensIsoSectionsFamily F U).hom sf) s
x✝ : Discrete ι
i : ι
⊢ limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i } (res F U s) =
    limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i } sf
rw [res, Types.Limit.lift_π_apply', Fan.mk_π_app]
no goals
case mp
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : IsGluing F U ((piOpensIsoSectionsFamily F U).hom sf) s
x✝ : Discrete ι
i : ι
⊢ F.map (leSupr U { as := i }.as).op s = limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i } sf
exact h i
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : res F U s = sf
i : ι
⊢ (forget (Type v)).map (F.map (leSupr U i).op) s = (piOpensIsoSectionsFamily F U).hom sf i
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : res F U s = sf
⊢ IsGluing F U ((piOpensIsoSectionsFamily F U).hom sf) s
intro i
case h.e'_2.h
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : res F U s = sf
i : ι
e_1✝ : (forget (Type v)).obj (F.obj (U i).op) = F.obj (U i).op
⊢ (forget (Type v)).map (F.map (leSupr U i).op) s = Pi.π (fun i => F.obj (U i).op) i (res F U s)
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : res F U s = sf
i : ι
⊢ (forget (Type v)).map (F.map (leSupr U i).op) s = (piOpensIsoSectionsFamily F U).hom sf i
convert congr_arg (Limits.Pi.π (fun i : ι => F.obj (op (U i))) i) h
case h.e'_2.h
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : res F U s = sf
i : ι
e_1✝ : (forget (Type v)).obj (F.obj (U i).op) = F.obj (U i).op
⊢ (forget (Type v)).map (F.map (leSupr U i).op) s = F.map (leSupr U i).op s
case h.e'_2.h
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : res F U s = sf
i : ι
e_1✝ : (forget (Type v)).obj (F.obj (U i).op) = F.obj (U i).op
⊢ (forget (Type v)).map (F.map (leSupr U i).op) s = Pi.π (fun i => F.obj (U i).op) i (res F U s)
rw [res, Types.pi_lift_π_apply]
no goals
case h.e'_2.h
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
sf : piOpens F U
s : F.obj (iSup U).op
h : res F U s = sf
i : ι
e_1✝ : (forget (Type v)).obj (F.obj (U i).op) = F.obj (U i).op
⊢ (forget (Type v)).map (F.map (leSupr U i).op) s = F.map (leSupr U i).op s
rfl