no goals
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Iic a = Iic ↑a
rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]