C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C X
U : Opens ↑Y
⊢ ℱ.map (𝟙 ((Opens.map f).obj U).op) = 𝟙 (ℱ.obj ((Opens.map f).obj U).op)
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C X
U : Opens ↑Y
⊢ (pushforwardEq (_ : f = f) ℱ).hom.app U.op = 𝟙 ((f _* ℱ).obj U.op)
dsimp [pushforwardEq]
no goals
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C X
U : Opens ↑Y
⊢ ℱ.map (𝟙 ((Opens.map f).obj U).op) = 𝟙 (ℱ.obj ((Opens.map f).obj U).op)
simp