no goals
ι : Type ?u.57885
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderBot α
⊢ Ioo a b ⊆ Iio b
simpa [← coe_subset] using Set.Ioo_subset_Iio_self