no goals
J : Type u'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (colimitPresheafObjIsoComponentwiseLimit F U).hom ≫ limit.π (componentwiseDiagram F U) j.op =
    (colimit.ι F j).c.app U.op
rw [← Iso.eq_inv_comp, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app]