no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
i : ι
⊢ res F U ≫ limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i } = F.map (leSupr U i).op
rw [res, limit.lift_π, Fan.mk_π_app]