case intro.intro.intro
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ ∃ a, stalkToFiber P x a = f { val := x, property := (_ : x ∈ U.obj) }
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
t : T x
⊢ ∃ a, stalkToFiber P x a = t
rcases w t with ⟨U, f, h, rfl⟩
case intro.intro.intro.w
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x

case intro.intro.intro.h
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ stalkToFiber P x ?intro.intro.intro.w = f { val := x, property := (_ : x ∈ U.obj) }
case intro.intro.intro
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ ∃ a, stalkToFiber P x a = f { val := x, property := (_ : x ∈ U.obj) }
fconstructor
no goals
case intro.intro.intro.w
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
exact (subsheafToTypes P).presheaf.germ ⟨x, U.2⟩ ⟨f, h⟩
no goals
case intro.intro.intro.h
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ stalkToFiber P x
      (Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ U.obj) }
        { val := f, property := h }) =
    f { val := x, property := (_ : x ∈ U.obj) }
exact stalkToFiber_germ _ U.1 ⟨x, U.2⟩ ⟨f, h⟩