no goals
α : Type u_1
β : Type ?u.46571
inst✝ : PartialOrder α
a b c : α
hab : a < b
⊢ Ioo a b ∪ {a} = Ico a b
rw [← Ico_diff_left, diff_union_self,
  union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)]