Bug in `fin_cases`?

Stream: mathlib4

[Riccardo Brasca]

Is this a bug in fin_cases or I am missing something?

import Mathlib.Tactic

example (p : ℕ) (h2 : 2 < p) (h5 : p < 5) : p = 3 ∨ p = 4 := by
  have hp : p ∈ Finset.Ioo 2 5 := (Finset.mem_Ioo).2 ⟨h2, h5⟩
  fin_cases hp -- Hypothesis must be of type `x ∈ (A : List α)`, `x ∈ (A : Finset α)`, or `x ∈ (A : Multiset α)`

If I give hp : p ∈ Finset.Ioo 2 5 as an explicit assumption than fin_cases works as expected.

[Kyle Miller]

In the code it looks like a missing instantiateMVars. I'll check if that's right.

[Riccardo Brasca]

Thanks!

[Kyle Miller]

@Riccardo Brasca #6046

[Riccardo Brasca]

(I am not going to review it since my knowledge in meta code is essentially zero)

[Kevin Buzzard]

But you've done your job -- you found and minimised the issue :-)