simp_rw [uIoc, mem_diff, mem_Ioc, mem_insert_iff, mem_singleton_iff] at hh
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : t ∈ Ι a b \ {a, b}
⊢ t ∈ uIoo a b
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ ¬(t = a ∨ t = b)
⊢ t ∈ uIoo a b