by_cases hl : mem a b I.left
a b : ℕ
I : BasicInterval
h : mem a b I
⊢ mem a b (left I) ∨ mem a b (right I)
case pos
a b : ℕ
I : BasicInterval
h : mem a b I
hl : mem a b (left I)
⊢ mem a b (left I) ∨ mem a b (right I)

case neg
a b : ℕ
I : BasicInterval
h : mem a b I
hl : ¬mem a b (left I)
⊢ mem a b (left I) ∨ mem a b (right I)