no goals
α : Type u_2
β : Type ?u.58776
γ : Type ?u.58779
ι : Sort u_1
inst✝ : ConditionallyCompleteLattice α
s t : Set α
a✝ b : α
hι : Nonempty ι
a : α
⊢ (⨆ (x : ι), a) = a
rw [iSup, range_const, csSup_singleton]