no goals
α : Type u_2
β : Type ?u.86729
β₂ : Type ?u.86732
γ : Type ?u.86735
ι : Sort u_1
ι' : Sort ?u.86741
κ : ι → Sort ?u.86746
κ' : ι' → Sort ?u.86751
inst✝¹ : CompleteLattice α
f g s t : ι → α
a b : α
inst✝ : Nonempty ι
⊢ (⨆ (x : ι), a) = a
rw [iSup, range_const, sSup_singleton]