∀ {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)
  (x x_1 : (TopologicalSpace.OpenNhds y)ᵒᵖ) (x_2 : x ⟶ x_1),
  CategoryTheory.CategoryStruct.comp
      (((TopologicalSpace.OpenNhds.inclusion y).op.comp (skyscraperPresheaf p₀ A)).map x_2)
      (CategoryTheory.Limits.terminal.from
        (((TopologicalSpace.OpenNhds.inclusion y).op.comp (skyscraperPresheaf p₀ A)).obj x_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.terminal.from
        (((TopologicalSpace.OpenNhds.inclusion y).op.comp (skyscraperPresheaf p₀ A)).obj x))
      (((CategoryTheory.Functor.const (TopologicalSpace.OpenNhds y)ᵒᵖ).obj (⊤_ C)).map x_2)