C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x)).map (𝟙 X).c ≫ stalkPushforward C (𝟙 ↑X) X.presheaf x =
    𝟙 (stalk X x)
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ stalkMap (𝟙 X) x = 𝟙 (stalk X x)
dsimp [stalkMap]
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x)).map (𝟙 X).c ≫
      (stalkFunctor C x).map (Pushforward.id X.presheaf).hom =
    𝟙 (stalk X x)
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x)).map (𝟙 X).c ≫ stalkPushforward C (𝟙 ↑X) X.presheaf x =
    𝟙 (stalk X x)
simp only [stalkPushforward.id]
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x)).map ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom) =
    𝟙 (stalk X x)
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x)).map (𝟙 X).c ≫
      (stalkFunctor C x).map (Pushforward.id X.presheaf).hom =
    𝟙 (stalk X x)
erw [← map_comp]
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ :
  (stalk X ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x) ⟶ stalk X x) =
    ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
⊢ (𝟙 X).c ≫ (Pushforward.id X.presheaf).hom = 𝟙 X.presheaf
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x)).map ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom) =
    𝟙 (stalk X x)
convert (stalkFunctor C x).map_id X.presheaf
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x✝ : ↑↑X
e_1✝ :
  (stalk X ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x✝) ⟶ stalk X x✝) =
    ((stalkFunctor C x✝).obj X.presheaf ⟶ (stalkFunctor C x✝).obj X.presheaf)
x : (Opens ↑↑X)ᵒᵖ
⊢ ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom).app x = (𝟙 X.presheaf).app x
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ :
  (stalk X ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x) ⟶ stalk X x) =
    ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
⊢ (𝟙 X).c ≫ (Pushforward.id X.presheaf).hom = 𝟙 X.presheaf
refine NatTrans.ext _ _ <| funext fun x => ?_
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x✝ : ↑↑X
e_1✝ :
  (stalk X ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x✝) ⟶ stalk X x✝) =
    ((stalkFunctor C x✝).obj X.presheaf ⟶ (stalkFunctor C x✝).obj X.presheaf)
x : (Opens ↑↑X)ᵒᵖ
⊢ 𝟙 (X.presheaf.obj ((Opens.map (𝟙 ↑X)).obj x.unop).op) = (𝟙 X.presheaf).app x
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x✝ : ↑↑X
e_1✝ :
  (stalk X ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x✝) ⟶ stalk X x✝) =
    ((stalkFunctor C x✝).obj X.presheaf ⟶ (stalkFunctor C x✝).obj X.presheaf)
x : (Opens ↑↑X)ᵒᵖ
⊢ ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom).app x = (𝟙 X.presheaf).app x
simp only [id_c, id_comp, Pushforward.id_hom_app, op_obj, eqToHom_refl, map_id]
no goals
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X : PresheafedSpace C
x✝ : ↑↑X
e_1✝ :
  (stalk X ((CategoryTheory.forget TopCat).map (𝟙 ↑X) x✝) ⟶ stalk X x✝) =
    ((stalkFunctor C x✝).obj X.presheaf ⟶ (stalkFunctor C x✝).obj X.presheaf)
x : (Opens ↑↑X)ᵒᵖ
⊢ 𝟙 (X.presheaf.obj ((Opens.map (𝟙 ↑X)).obj x.unop).op) = (𝟙 X.presheaf).app x
rfl