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