no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ stalk X x = stalk X x'
rw [h]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ stalk Y ((CategoryTheory.forget TopCat).map α.base x) = stalk Y ((CategoryTheory.forget TopCat).map α.base x')
rw [h]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x') =
    eqToHom
        (_ :
          stalk Y ((CategoryTheory.forget TopCat).map α.base x) =
            stalk Y ((CategoryTheory.forget TopCat).map α.base x')) ≫
      stalkMap α x'
rw [stalkMap.congr α α rfl x x' h]