no goals
J : Type u'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
F : J ⥤ PresheafedSpace C
j : J
U : Opens ↑↑(F.obj j)
⊢ 𝟙 ↑(F.obj j) = (F.map (𝟙 j)).base
simp
case mk
J : Type u'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
F : J ⥤ PresheafedSpace C
j : J
carrier✝ : Set ↑↑(F.obj j)
is_open'✝ : IsOpen carrier✝
⊢ (F.map (𝟙 j)).c.app { carrier := carrier✝, is_open' := is_open'✝ }.op =
    (Pushforward.id (F.obj j).presheaf).inv.app { carrier := carrier✝, is_open' := is_open'✝ }.op ≫
      (pushforwardEq (_ : 𝟙 ↑(F.obj j) = (F.map (𝟙 j)).base) (F.obj j).presheaf).hom.app
        { carrier := carrier✝, is_open' := is_open'✝ }.op
J : Type u'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
F : J ⥤ PresheafedSpace C
j : J
U : Opens ↑↑(F.obj j)
⊢ (F.map (𝟙 j)).c.app U.op =
    (Pushforward.id (F.obj j).presheaf).inv.app U.op ≫
      (pushforwardEq (_ : 𝟙 ↑(F.obj j) = (F.map (𝟙 j)).base) (F.obj j).presheaf).hom.app U.op
cases U
no goals
case mk
J : Type u'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
F : J ⥤ PresheafedSpace C
j : J
carrier✝ : Set ↑↑(F.obj j)
is_open'✝ : IsOpen carrier✝
⊢ (F.map (𝟙 j)).c.app { carrier := carrier✝, is_open' := is_open'✝ }.op =
    (Pushforward.id (F.obj j).presheaf).inv.app { carrier := carrier✝, is_open' := is_open'✝ }.op ≫
      (pushforwardEq (_ : 𝟙 ↑(F.obj j) = (F.map (𝟙 j)).base) (F.obj j).presheaf).hom.app
        { carrier := carrier✝, is_open' := is_open'✝ }.op
simp [PresheafedSpace.congr_app (F.map_id j)]