no goals
C : Type u
inst✝ : Category C
X : SheafedSpace C
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ X.presheaf.obj U = ((𝟙 X).base _* X.presheaf).obj U
aesop_cat
no goals
C : Type u
inst✝ : Category C
X : SheafedSpace C
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ (𝟙 X).c.app U =
    eqToHom (_ : X.presheaf.obj U = X.presheaf.obj ((Functor.op (Opens.map (𝟙 ↑X.toPresheafedSpace))).obj U))
aesop_cat