no goals
α : Type u_1
β : Type ?u.89762
γ : Type ?u.89765
ι : Sort u_2
ι' : Sort ?u.89771
f✝ : ι → α
s t : Set α
f : ι → α
x : α
⊢ range f ⊆ {x} ↔ f = const ι x
simp [range_subset_iff, funext_iff, mem_singleton]