C : Type ?u.248420
inst✝ : Category C
X : PresheafedSpace C
⊢ X.presheaf =
    ((Opens.inclusionTopIso ↑X).inv ≫
        (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).base) _*
      X.presheaf
C : Type ?u.248420
inst✝ : Category C
X : PresheafedSpace C
⊢ X.presheaf =
    (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).base _*
      (restrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).presheaf
rw [restrict_top_presheaf, ← Presheaf.Pushforward.comp_eq]
C : Type ?u.248420
inst✝ : Category C
X : PresheafedSpace C
⊢ X.presheaf = 𝟙 ↑X _* X.presheaf
C : Type ?u.248420
inst✝ : Category C
X : PresheafedSpace C
⊢ X.presheaf =
    ((Opens.inclusionTopIso ↑X).inv ≫
        (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).base) _*
      X.presheaf
erw [Iso.inv_hom_id]
no goals
C : Type ?u.248420
inst✝ : Category C
X : PresheafedSpace C
⊢ X.presheaf = 𝟙 ↑X _* X.presheaf
rw [Presheaf.Pushforward.id_eq]
case app
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
⊢ (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).c.app =
    (eqToHom
        (_ :
          X.presheaf =
            (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).base _*
              (restrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).presheaf)).app
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
⊢ (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).c =
    eqToHom
      (_ :
        X.presheaf =
          (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).base _*
            (restrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).presheaf)
apply NatTrans.ext
case app.h
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).c.app U =
    (eqToHom
          (_ :
            X.presheaf =
              (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).base _*
                (restrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).presheaf)).app
      U
case app
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
⊢ (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).c.app =
    (eqToHom
        (_ :
          X.presheaf =
            (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).base _*
              (restrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).presheaf)).app
ext1 U
case app.h
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ X.presheaf.map
      ((IsOpenMap.adjunction (_ : IsOpenMap ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).counit.app
          U.unop).op =
    (eqToHom
          (_ :
            X.presheaf =
              Opens.inclusion ⊤ _*
                (Functor.op
                    (IsOpenMap.functor (_ : IsOpenMap ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))) ⋙
                  X.presheaf))).app
      U
case app.h
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).c.app U =
    (eqToHom
          (_ :
            X.presheaf =
              (ofRestrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).base _*
                (restrict X (_ : OpenEmbedding ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).presheaf)).app
      U
dsimp [ofRestrict]
case app.h.p
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ U =
    ((IsOpenMap.functor (_ : IsOpenMap ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).obj
        ((Opens.map (Opens.inclusion ⊤)).obj U.unop)).op

case app.h.p
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ U =
    ((IsOpenMap.functor (_ : IsOpenMap ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).obj
        ((Opens.map (Opens.inclusion ⊤)).obj U.unop)).op
case app.h
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ X.presheaf.map
      ((IsOpenMap.adjunction (_ : IsOpenMap ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).counit.app
          U.unop).op =
    (eqToHom
          (_ :
            X.presheaf =
              Opens.inclusion ⊤ _*
                (Functor.op
                    (IsOpenMap.functor (_ : IsOpenMap ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))) ⋙
                  X.presheaf))).app
      U
erw [eqToHom_map, eqToHom_app]
no goals
case app.h.p
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ U =
    ((IsOpenMap.functor (_ : IsOpenMap ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).obj
        ((Opens.map (Opens.inclusion ⊤)).obj U.unop)).op

case app.h.p
C : Type u_1
inst✝ : Category C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ U =
    ((IsOpenMap.functor (_ : IsOpenMap ((CategoryTheory.forget TopCat).map (Opens.inclusion ⊤)))).obj
        ((Opens.map (Opens.inclusion ⊤)).obj U.unop)).op
simp