rcases hor with (rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl)
case h.mpr
x : ℤ
hor :
  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
⊢ |3 * x| < 24
case h.mpr.inl

⊢ |3 * -7| < 24

case h.mpr.inr.inl

⊢ |3 * -6| < 24

case h.mpr.inr.inr.inl

⊢ |3 * -5| < 24

case h.mpr.inr.inr.inr.inl

⊢ |3 * -4| < 24

case h.mpr.inr.inr.inr.inr.inl

⊢ |3 * -3| < 24

case h.mpr.inr.inr.inr.inr.inr.inl

⊢ |3 * -2| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * -1| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 0| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 1| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 2| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 3| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 4| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 5| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inl

⊢ |3 * 6| < 24

case h.mpr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.inr.refl

⊢ |3 * 7| < 24