cases hh with
| inl h => simp [uIoc, h, h.2.le, h.1.ne.symm, h.2.ne]
| inr h => simp [uIoc, h, h.2.le, h.1.ne.symm, h.2.ne]
case h.mp
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : a < t ∧ t < b ∨ b < t ∧ t < a
⊢ t ∈ Ι a b \ {a, b}
no goals