no goals
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioo a b = Ioo ↑a ↑b
rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Ioi_self <| Ioi_subset_Ioi bot_le)]