case h
C : Type u
inst✝ : Category C
X : TopCat
ℱ : Presheaf C X
U : Opens ↑X
⊢ (id ℱ).hom.app U.op = ℱ.map (eqToHom (_ : (Functor.op (Opens.map (𝟙 X))).obj U.op = U.op))
C : Type u
inst✝ : Category C
X : TopCat
ℱ : Presheaf C X
U : (Opens ↑X)ᵒᵖ
⊢ (id ℱ).hom.app U = ℱ.map (eqToHom (_ : (Functor.op (Opens.map (𝟙 X))).obj U = U))
induction' U with U
no goals
case h
C : Type u
inst✝ : Category C
X : TopCat
ℱ : Presheaf C X
U : Opens ↑X
⊢ (id ℱ).hom.app U.op = ℱ.map (eqToHom (_ : (Functor.op (Opens.map (𝟙 X))).obj U.op = U.op))
apply id_hom_app'