simp only [Set.mem_singleton_iff, Set.mem_insert_iff, or_self]
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
⊢ x ∈ {-7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
case h.mp.intro
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
⊢ x = -7 ∨
    x = -6 ∨ x = -5 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7