-- Mathlib/Topology/Sheaves/Stalks.lean
theorem germ_exist (F : X.Presheaf C) (x : X) (t : ToType (stalk.{v, u} F x)) :
    ∃ (U : Opens X) (m : x ∈ U) (s : ToType (F.obj (op U))), F.germ _ x m s = t

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
U : (OpenNhds x)ᵒᵖ
⊢ ∀ (s : (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj U),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
          U s =
        t →
      ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
induction U with | h U => ?_

Result:
case intro.intro.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
U : OpenNhds x
⊢ ∀ (s : (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj (op U)),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
          (op U) s =
        t →
      ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Proof state:
case intro.intro.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
U : OpenNhds x
⊢ ∀ (s : (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj (op U)),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
          (op U) s =
        t →
      ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
obtain ⟨V, m⟩ := U

Result:
case intro.intro.h.mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
V : Opens ↑X
m : x ∈ V
⊢ ∀
    (s :
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj
        (op { obj := V, property := m })),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
          (op { obj := V, property := m }) s =
        t →
      ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
U : (OpenNhds x)ᵒᵖ
s : (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj U
e :
  ((forget C).mapCocone
            (colimit.cocone
              (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
      U s =
    t
⊢ ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
revert s e

Result:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
U : (OpenNhds x)ᵒᵖ
⊢ ∀ (s : (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj U),
    ((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
          U s =
        t →
      ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
⊢ ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
obtain ⟨U, s, e⟩ :=
  Types.jointly_surjective.{v, v} _ (isColimitOfPreserves (forget C) (colimit.isColimit _)) t

Result:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
U : (OpenNhds x)ᵒᵖ
s : (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj U
e :
  ((forget C).mapCocone
            (colimit.cocone
              (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
      U s =
    t
⊢ ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Proof state:
case intro.intro.h.mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
V : Opens ↑X
m : x ∈ V
s :
  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj
    (op { obj := V, property := m })
e :
  ((forget C).mapCocone
            (colimit.cocone
              (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
      (op { obj := V, property := m }) s =
    t
⊢ ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
exact ⟨V, m, s, e⟩

Result:
no goals