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