case 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
x : ↑X
t : (forget C).obj (stalk F x)
U : (OpenNhds x)ᵒᵖ
s : (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F ⋙ forget C).obj U
e :
  ((forget C).mapCocone
            (colimit.cocone
              (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F))).ι.app
      U s =
    t
⊢ ∃ U m s, (forget C).map (germ F { val := x, property := m }) s = 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
x : ↑X
t : (forget C).obj (stalk F x)
⊢ ∃ U m s, (forget C).map (germ F { val := x, property := m }) s = t
obtain ⟨U, s, e⟩ :=
  Types.jointly_surjective.{v, v} _ (isColimitOfPreserves (forget C) (colimit.isColimit _)) t
case 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
x : ↑X
t : (forget C).obj (stalk F x)
U : (OpenNhds x)ᵒᵖ
⊢ ∀
    (s :
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F ⋙ forget C).obj
        U),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj
                    F))).ι.app
          U s =
        t →
      ∃ U m s, (forget C).map (germ F { val := x, property := m }) s = t
case 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
x : ↑X
t : (forget C).obj (stalk F x)
U : (OpenNhds x)ᵒᵖ
s : (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F ⋙ forget C).obj U
e :
  ((forget C).mapCocone
            (colimit.cocone
              (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F))).ι.app
      U s =
    t
⊢ ∃ U m s, (forget C).map (germ F { val := x, property := m }) s = t
revert s e
case intro.intro.h
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : (forget C).obj (stalk F x)
U : OpenNhds x
⊢ ∀
    (s :
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F ⋙ forget C).obj
        U.op),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj
                    F))).ι.app
          U.op s =
        t →
      ∃ U m s, (forget C).map (germ F { val := x, property := m }) s = t
case 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
x : ↑X
t : (forget C).obj (stalk F x)
U : (OpenNhds x)ᵒᵖ
⊢ ∀
    (s :
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F ⋙ forget C).obj
        U),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj
                    F))).ι.app
          U s =
        t →
      ∃ U m s, (forget C).map (germ F { val := x, property := m }) s = t
induction U with | h U => ?_
case intro.intro.h.mk
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : (forget C).obj (stalk F x)
V : Opens ↑X
m : x ∈ V
⊢ ∀
    (s :
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F ⋙ forget C).obj
        { obj := V, property := m }.op),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj
                    F))).ι.app
          { obj := V, property := m }.op s =
        t →
      ∃ U m s, (forget C).map (germ F { val := x, property := m }) s = t
case intro.intro.h
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : (forget C).obj (stalk F x)
U : OpenNhds x
⊢ ∀
    (s :
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F ⋙ forget C).obj
        U.op),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj
                    F))).ι.app
          U.op s =
        t →
      ∃ U m s, (forget C).map (germ F { val := x, property := m }) s = t
cases' U with V m
case intro.intro.h.mk
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : (forget C).obj (stalk F x)
V : Opens ↑X
m : x ∈ V
s :
  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F ⋙ forget C).obj
    { obj := V, property := m }.op
e :
  ((forget C).mapCocone
            (colimit.cocone
              (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F))).ι.app
      { obj := V, property := m }.op s =
    t
⊢ ∃ U m s, (forget C).map (germ F { val := x, property := m }) s = t
case intro.intro.h.mk
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : (forget C).obj (stalk F x)
V : Opens ↑X
m : x ∈ V
⊢ ∀
    (s :
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F ⋙ forget C).obj
        { obj := V, property := m }.op),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj
                    F))).ι.app
          { obj := V, property := m }.op s =
        t →
      ∃ U m s, (forget C).map (germ F { val := x, property := m }) s = t
intro s e
no goals
case intro.intro.h.mk
C : Type u
inst✝³ : Category C
inst✝² : HasColimits C
X Y Z : TopCat
inst✝¹ : ConcreteCategory C
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : (forget C).obj (stalk F x)
V : Opens ↑X
m : x ∈ V
s :
  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F ⋙ forget C).obj
    { obj := V, property := m }.op
e :
  ((forget C).mapCocone
            (colimit.cocone
              (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F))).ι.app
      { obj := V, property := m }.op s =
    t
⊢ ∃ U m s, (forget C).map (germ F { val := x, property := m }) s = t
exact ⟨V, m, s, e⟩