no goals
α✝ : Type u
β✝ : Type v
inst✝³ : TopologicalSpace α✝
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space β
y : β
s : Set α
x✝ : IsClosed s
h2s : Set.Nonempty s
⊢ IsClosed (const α y '' s)
simp_rw [const, h2s.image_const, isClosed_singleton]