Lean4
/-- The cocone at `*` for the stalk functor of `skyscraperPresheaf p₀ A` when `y ∉ closure {p₀}` is a
colimit
-/
noncomputable def skyscraperPresheafCoconeIsColimitOfNotSpecializes {y : X} (h : ¬p₀ ⤳ y) :
IsColimit (skyscraperPresheafCocone p₀ A y) :=
let h1 : ∃ U : OpenNhds y, p₀ ∉ U.1 :=
let ⟨U, ho, h₀, hy⟩ := not_specializes_iff_exists_open.mp h
⟨⟨⟨U, ho⟩, h₀⟩, hy⟩
{ desc := fun c => eqToHom (if_neg h1.choose_spec).symm ≫ c.ι.app (op h1.choose)
fac := fun c U => by
change _ = c.ι.app (op U.unop)
simp only [← c.w (homOfLE <| @inf_le_left _ _ h1.choose U.unop).op,
← c.w (homOfLE <| @inf_le_right _ _ h1.choose U.unop).op, ← Category.assoc]
congr 1
refine ((if_neg ?_).symm.ndrec terminalIsTerminal).hom_ext _ _
exact fun h => h1.choose_spec h.1
uniq := fun c f H => by
dsimp
rw [← Category.id_comp f, ← H, ← Category.assoc]
congr 1; apply terminalIsTerminal.hom_ext }
