case intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
U V : Opens ↑X
x : ↑X
mU : x ∈ U
mV : x ∈ V
s : (forget C).obj (F.obj U.op)
t : (forget C).obj (F.obj V.op)
h : (forget C).map (germ F { val := x, property := mU }) s = (forget C).map (germ F { val := x, property := mV }) t
W : (OpenNhds x)ᵒᵖ
iU : { obj := U, property := (_ : ↑{ val := x, property := mU } ∈ U) }.op ⟶ W
iV : { obj := V, property := (_ : ↑{ val := x, property := mV } ∈ V) }.op ⟶ W
e :
  ((Functor.op (OpenNhds.inclusion x) ⋙ F) ⋙ forget C).map iU s =
    ((Functor.op (OpenNhds.inclusion x) ⋙ F) ⋙ forget C).map iV t
⊢ ∃ W _m iU iV, (forget C).map (F.map iU.op) s = (forget C).map (F.map iV.op) t
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
U V : Opens ↑X
x : ↑X
mU : x ∈ U
mV : x ∈ V
s : (forget C).obj (F.obj U.op)
t : (forget C).obj (F.obj V.op)
h : (forget C).map (germ F { val := x, property := mU }) s = (forget C).map (germ F { val := x, property := mV }) t
⊢ ∃ W _m iU iV, (forget C).map (F.map iU.op) s = (forget C).map (F.map iV.op) t
obtain ⟨W, iU, iV, e⟩ :=
  (Types.FilteredColimit.isColimit_eq_iff.{v, v} _
        (isColimitOfPreserves _ (colimit.isColimit ((OpenNhds.inclusion x).op ⋙ F)))).mp h
no goals
case intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
U V : Opens ↑X
x : ↑X
mU : x ∈ U
mV : x ∈ V
s : (forget C).obj (F.obj U.op)
t : (forget C).obj (F.obj V.op)
h : (forget C).map (germ F { val := x, property := mU }) s = (forget C).map (germ F { val := x, property := mV }) t
W : (OpenNhds x)ᵒᵖ
iU : { obj := U, property := (_ : ↑{ val := x, property := mU } ∈ U) }.op ⟶ W
iV : { obj := V, property := (_ : ↑{ val := x, property := mV } ∈ V) }.op ⟶ W
e :
  ((Functor.op (OpenNhds.inclusion x) ⋙ F) ⋙ forget C).map iU s =
    ((Functor.op (OpenNhds.inclusion x) ⋙ F) ⋙ forget C).map iV t
⊢ ∃ W _m iU iV, (forget C).map (F.map iU.op) s = (forget C).map (F.map iV.op) t
exact ⟨(unop W).1, (unop W).2, iU.unop, iV.unop, e⟩