no goals
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ici a = Ici ↑a
rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Ici_subset_Ioi.2 <| bot_lt_coe a)]