refine ⟨hh.1.1, lt_of_le_of_ne hh.1.2 ?_⟩
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
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 ≠ a ⊔ b