fin_cases breaks on intervals of Fin

fin_cases fails on some intervals over the type Fin (k + 2). For example:

import Mathlib.Tactic

example (k : ℕ) (x : Fin (k + 2)) (hx : x ∈ Finset.Iic 1) : True := by
  fin_cases hx

and

import Mathlib.Tactic

example (k : ℕ) (x : Fin (k + 2)) (hx : x ∈ Finset.Icc 0 1) : True := by
  fin_cases hx

should each create two cases, (x = ⊥ and x = 1 in the first example, x = 0 and x = 1 in the second). Instead they both return the error "(kernel) declaration has metavariables '_example'". More examples of this can be found in this thread on the Lean Zulip.

Reproduce the two examples from the issue after importing Mathlib.Tactic, using fin_cases on Finset.Iic 1 and Finset.Icc 0 1 over Fin (k + 2). Read the fin_cases tactic entry point and compare the failing interval handling with the expected two cases; done means both examples elaborate without metavariable errors and produce the stated cases.