C : Type u
inst✝ : Category C
X Y : SheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Functor.op (Opens.map α.base)).obj U = (Functor.op (Opens.map α.base)).obj U
C : Type u
inst✝ : Category C
X Y : SheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Functor.op (Opens.map β.base)).obj U = (Functor.op (Opens.map α.base)).obj U
subst h
no goals
C : Type u
inst✝ : Category C
X Y : SheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Functor.op (Opens.map α.base)).obj U = (Functor.op (Opens.map α.base)).obj U
rfl