mathlib3

9dbe038e - fix({ tactic/fin_cases + test/interval_cases }): add `focus1` and a test (#16752)

fix({ tactic/fin_cases + test/interval_cases }): add `focus1` and a test (#16752) Fix [this bug](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/interval_cases.20bug), reported by @hrmacbeth. The current solution is to move the `focus1` to `fin_cases_at`, instead of relying on `fin_cases` and `interval_cases` to call `focus1`. Having `interval_cases` wrapped in `focus1` is the reason for this PR. An older (compiling) solution was to just use `focus1` inside `interval_cases`, but calling it in `fin_cases_at` seems more stable. The link above is to a Zulip discussion with more details.