no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
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
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ stalk Y ((CategoryTheory.forget TopCat).map α.base x) = stalk Y ((CategoryTheory.forget TopCat).map β.base x')
rw [h₁, h₂]
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h₂ : x = x'
U : Opens ↑↑Y
hx : (CategoryTheory.forget TopCat).map α.base x ∈ U
⊢ germ Y.presheaf { val := (CategoryTheory.forget TopCat).map α.base x, property := hx } ≫
      stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x') =
    germ Y.presheaf { val := (CategoryTheory.forget TopCat).map α.base x, property := hx } ≫
      eqToHom
          (_ :
            stalk Y ((CategoryTheory.forget TopCat).map α.base x) =
              stalk Y ((CategoryTheory.forget TopCat).map α.base x')) ≫
        stalkMap α x'
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
U : Opens ↑↑Y
hx : (CategoryTheory.forget TopCat).map α.base x ∈ U
⊢ germ Y.presheaf { val := (CategoryTheory.forget TopCat).map α.base x, property := hx } ≫
      stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x') =
    germ Y.presheaf { val := (CategoryTheory.forget TopCat).map α.base x, property := hx } ≫
      eqToHom
          (_ :
            stalk Y ((CategoryTheory.forget TopCat).map α.base x) =
              stalk Y ((CategoryTheory.forget TopCat).map β.base x')) ≫
        stalkMap β x'
subst h₁
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x : ↑↑X
U : Opens ↑↑Y
hx : (CategoryTheory.forget TopCat).map α.base x ∈ U
⊢ germ Y.presheaf { val := (CategoryTheory.forget TopCat).map α.base x, property := hx } ≫
      stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x) =
    germ Y.presheaf { val := (CategoryTheory.forget TopCat).map α.base x, property := hx } ≫
      eqToHom
          (_ :
            stalk Y ((CategoryTheory.forget TopCat).map α.base x) =
              stalk Y ((CategoryTheory.forget TopCat).map α.base x)) ≫
        stalkMap α x
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h₂ : x = x'
U : Opens ↑↑Y
hx : (CategoryTheory.forget TopCat).map α.base x ∈ U
⊢ germ Y.presheaf { val := (CategoryTheory.forget TopCat).map α.base x, property := hx } ≫
      stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x') =
    germ Y.presheaf { val := (CategoryTheory.forget TopCat).map α.base x, property := hx } ≫
      eqToHom
          (_ :
            stalk Y ((CategoryTheory.forget TopCat).map α.base x) =
              stalk Y ((CategoryTheory.forget TopCat).map α.base x')) ≫
        stalkMap α x'
subst h₂
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x : ↑↑X
U : Opens ↑↑Y
hx : (CategoryTheory.forget TopCat).map α.base x ∈ U
⊢ germ Y.presheaf { val := (CategoryTheory.forget TopCat).map α.base x, property := hx } ≫
      stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x) =
    germ Y.presheaf { val := (CategoryTheory.forget TopCat).map α.base x, property := hx } ≫
      eqToHom
          (_ :
            stalk Y ((CategoryTheory.forget TopCat).map α.base x) =
              stalk Y ((CategoryTheory.forget TopCat).map α.base x)) ≫
        stalkMap α x
simp