no goals
C✝ : Type u
inst✝³ : Category C✝
inst✝² : HasColimits C✝
X✝ Y Z : TopCat
C : Type u_1
inst✝¹ : Category C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x y z : ↑X
h : x ⤳ y
h' : y ⤳ z
x✝¹ : Opens ↑X
x✝ : z ∈ x✝¹
⊢ germ F { val := z, property := x✝ } ≫ stalkSpecializes F h' ≫ stalkSpecializes F h =
    germ F { val := z, property := x✝ } ≫ stalkSpecializes F (_ : x ⤳ z)
simp