X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
x : { x // x ∈ U }
f : (Sheaf.presheaf (subsheafToTypes P)).obj U.op
⊢ colimit.desc (Functor.op (OpenNhds.inclusion ↑x) ⋙ subpresheafToTypes P.toPrelocalPredicate)
      { pt := T ↑x, ι := NatTrans.mk fun U_1 f => ↑f { val := ↑x, property := (_ : ↑x ∈ U_1.unop.obj) } }
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑x) ⋙ subpresheafToTypes P.toPrelocalPredicate)
        { obj := U, property := (_ : ↑x ∈ U) }.op f) =
    ↑f x
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
x : { x // x ∈ U }
f : (Sheaf.presheaf (subsheafToTypes P)).obj U.op
⊢ stalkToFiber P (↑x) (Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) x f) = ↑f x
dsimp [Presheaf.germ, stalkToFiber]
case mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
f : (Sheaf.presheaf (subsheafToTypes P)).obj U.op
val✝ : ↑X
property✝ : val✝ ∈ U
⊢ colimit.desc
      (Functor.op (OpenNhds.inclusion ↑{ val := val✝, property := property✝ }) ⋙
        subpresheafToTypes P.toPrelocalPredicate)
      { pt := T ↑{ val := val✝, property := property✝ },
        ι :=
          NatTrans.mk fun U_1 f =>
            ↑f
              { val := ↑{ val := val✝, property := property✝ },
                property := (_ : ↑{ val := val✝, property := property✝ } ∈ U_1.unop.obj) } }
      (colimit.ι
        (Functor.op (OpenNhds.inclusion ↑{ val := val✝, property := property✝ }) ⋙
          subpresheafToTypes P.toPrelocalPredicate)
        { obj := U, property := (_ : ↑{ val := val✝, property := property✝ } ∈ U) }.op f) =
    ↑f { val := val✝, property := property✝ }
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
x : { x // x ∈ U }
f : (Sheaf.presheaf (subsheafToTypes P)).obj U.op
⊢ colimit.desc (Functor.op (OpenNhds.inclusion ↑x) ⋙ subpresheafToTypes P.toPrelocalPredicate)
      { pt := T ↑x, ι := NatTrans.mk fun U_1 f => ↑f { val := ↑x, property := (_ : ↑x ∈ U_1.unop.obj) } }
      (colimit.ι (Functor.op (OpenNhds.inclusion ↑x) ⋙ subpresheafToTypes P.toPrelocalPredicate)
        { obj := U, property := (_ : ↑x ∈ U) }.op f) =
    ↑f x
cases x
no goals
case mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
f : (Sheaf.presheaf (subsheafToTypes P)).obj U.op
val✝ : ↑X
property✝ : val✝ ∈ U
⊢ colimit.desc
      (Functor.op (OpenNhds.inclusion ↑{ val := val✝, property := property✝ }) ⋙
        subpresheafToTypes P.toPrelocalPredicate)
      { pt := T ↑{ val := val✝, property := property✝ },
        ι :=
          NatTrans.mk fun U_1 f =>
            ↑f
              { val := ↑{ val := val✝, property := property✝ },
                property := (_ : ↑{ val := val✝, property := property✝ } ∈ U_1.unop.obj) } }
      (colimit.ι
        (Functor.op (OpenNhds.inclusion ↑{ val := val✝, property := property✝ }) ⋙
          subpresheafToTypes P.toPrelocalPredicate)
        { obj := U, property := (_ : ↑{ val := val✝, property := property✝ } ∈ U) }.op f) =
    ↑f { val := val✝, property := property✝ }
simp