no goals
C : Type u
inst✝ : Category C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Functor.op (Opens.map f)).obj U = (Functor.op (Opens.map g)).obj U
rw [h]
no goals
C : Type u
inst✝ : Category C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (eqToHom (_ : f _* ℱ = g _* ℱ)).app U =
    ℱ.map (eqToHom (_ : (Functor.op (Opens.map f)).obj U = (Functor.op (Opens.map g)).obj U))
rw [eqToHom_app, eqToHom_map]