Use of `fin_cases` tactic with `let` declaration

Stream: mathlib4

[Will Bradley]

How do I use the fin_cases tactic with a let declaration? According to the docs, the using clause hasn't been added to mathlib4, but can I really not run this example (also from the docs) without naming the generated hypotheses?

  let a := f 3
  fin_cases a using ha

It generates the error

dependent elimination failed, failed to solve equation
  { val := 0, isLt := _ } = a```. I assume this is because it gets hung up on `Fin 0`.

[Timo Carlin-Burns]

Is this the full code you're referring to? (From docs#Lean.Elab.Tactic.finCases) It's helpful to provide an #mwe

import Mathlib.Tactic.FinCases

example (f : ℕ → Fin 3) : True := by
  let a := f 3
  fin_cases a using ha

[Timo Carlin-Burns]

Maybe the using variant wasn't ported. Here is a workaround

import Mathlib.Tactic.FinCases

example (f : ℕ → Fin 3) : True := by
  set a := f 3 with ha
  clear_value a
  fin_cases a

[Eric Rodriguez]

fin_cases has a lot of issues and one of the things in my todo list is to rewrite it

[Kyle Miller]

Will Bradley said:

dependent elimination failed, failed to solve equation
  { val := 0, isLt := _ } = a

I assume this is because it gets hung up on Fin 0.

The error is that it's seeing { val := 0, isLt := _ } = f 3 and for "dependent elimination" to succeed, which is used in cases inside the tactic, it needs one side of this to be a free variable, or it needs both sides to be a constructor application (and then it recurses).