∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C] {y : ↑X}
  (h : p₀ ⤳ y)
  (c : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion y).op.comp (skyscraperPresheaf p₀ A)))
  (U : (TopologicalSpace.OpenNhds y)ᵒᵖ),
  CategoryTheory.CategoryStruct.comp ((skyscraperPresheafCoconeOfSpecializes p₀ A h).ι.app U)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (c.ι.app (Opposite.op ⊤))) =
    c.ι.app U