case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ ∀ (t : stalk F x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ Function.Surjective (stalkToFiber F x)
apply TopCat.stalkToFiber_surjective
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
t : stalk F x
⊢ ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ ∀ (t : stalk F x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
intro t
case w.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (CategoryTheory.forget (Type v)).obj (F.obj U.op)
⊢ ∃ U_1 f x_1,
    f { val := x, property := (_ : x ∈ U_1.obj) } =
      (CategoryTheory.forget (Type v)).map (germ F { val := x, property := m }) s
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
t : stalk F x
⊢ ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
obtain ⟨U, m, s, rfl⟩ := F.germ_exist _ t
case w.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (CategoryTheory.forget (Type v)).obj (F.obj U.op)
⊢ ∃ f x_1,
    f { val := x, property := (_ : x ∈ { obj := U, property := m }.obj) } =
      (CategoryTheory.forget (Type v)).map (germ F { val := x, property := m }) s
case w.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (CategoryTheory.forget (Type v)).obj (F.obj U.op)
⊢ ∃ U_1 f x_1,
    f { val := x, property := (_ : x ∈ U_1.obj) } =
      (CategoryTheory.forget (Type v)).map (germ F { val := x, property := m }) s
use ⟨U, m⟩
case w.intro.intro.intro.w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (CategoryTheory.forget (Type v)).obj (F.obj U.op)
⊢ (y : { x_1 // x_1 ∈ { obj := U, property := m }.obj }) → stalk F ↑y

case w.intro.intro.intro.h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (CategoryTheory.forget (Type v)).obj (F.obj U.op)
⊢ ∃ x_1,
    ?w.intro.intro.intro.w { val := x, property := (_ : x ∈ { obj := U, property := m }.obj) } =
      (CategoryTheory.forget (Type v)).map (germ F { val := x, property := m }) s
case w.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (CategoryTheory.forget (Type v)).obj (F.obj U.op)
⊢ ∃ f x_1,
    f { val := x, property := (_ : x ∈ { obj := U, property := m }.obj) } =
      (CategoryTheory.forget (Type v)).map (germ F { val := x, property := m }) s
fconstructor
no goals
case w.intro.intro.intro.w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (CategoryTheory.forget (Type v)).obj (F.obj U.op)
⊢ (y : { x_1 // x_1 ∈ { obj := U, property := m }.obj }) → stalk F ↑y
exact fun y => F.germ y s
no goals
case w.intro.intro.intro.h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (CategoryTheory.forget (Type v)).obj (F.obj U.op)
⊢ ∃ x_1,
    germ F { val := x, property := (_ : x ∈ { obj := U, property := m }.obj) } s =
      (CategoryTheory.forget (Type v)).map (germ F { val := x, property := m }) s
exact ⟨PrelocalPredicate.sheafifyOf ⟨s, fun _ => rfl⟩, rfl⟩