Ranges of naturals

Stream: new members

[Michael Wahlberg]

If we have finite ranges, how do we trivially say that the number will be in one of the ranges mentioned? This is a lean4 code

example (n : ℕ)(hn1 : 2 ≤ n)(hn2 : n < 4)  : n = 2 ∨ n = 3 := by
  sorry

[Alex J. Best]

Looks like a perfect job for tactic#interval_cases (it should work in lean 4 too after Mathlib.Tactic.IntervalCases)