C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
⊢ Functor.op (IsOpenMap.functor (_ : IsOpenMap ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))) ⋙ X.presheaf =
    (Opens.inclusionTopIso ↑X).inv _* X.presheaf
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
⊢ (restrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).presheaf =
    (Opens.inclusionTopIso ↑X).inv _* X.presheaf
dsimp
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
⊢ Functor.op (Opens.map (Opens.inclusionTopIso ↑X).inv) ⋙ X.presheaf = (Opens.inclusionTopIso ↑X).inv _* X.presheaf
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
⊢ Functor.op (IsOpenMap.functor (_ : IsOpenMap ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))) ⋙ X.presheaf =
    (Opens.inclusionTopIso ↑X).inv _* X.presheaf
rw [Opens.inclusion_top_functor X.carrier]
no goals
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
⊢ Functor.op (Opens.map (Opens.inclusionTopIso ↑X).inv) ⋙ X.presheaf = (Opens.inclusionTopIso ↑X).inv _* X.presheaf
rfl