simp only [mem_Ioc, mem_sdiff, not_and, not_le]
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ x ∈ Ioc a b ↔ x ∈ Ioc a c \ Ioc b c
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ a < x ∧ x ≤ b ↔ (a < x ∧ x ≤ c) ∧ (b < x → c < x)