unknown free variable error

Stream: new members

[Snir Broshi]

import Mathlib

theorem foo {α : Type*} [DecidableEq α] (z : Sym2 α) (h : z.toFinset.Nonempty) : True := by
  let z' := z
  let s := z'.toFinset
  have h' : s.Nonempty := h
  let ⟨x, hx⟩ := h'

results in this error:

unknown free variable `_fvar.61`

There are a few bug reports about this error message, but none of them seem like the same scenario to me.
Is this one of the known issues? Is it a new bug? Or am I doing something wrong?

[Yongxi Lin (Aaron)]

You should use obtain instead of let in your last line.

[Ruben Van de Velde]

You probably should, but this still looks like a bug.

[Aaron Liu]

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/unknown.20free.20variable.20on.20.60obtain.60

[Aaron Liu]

this could be the same thing?

[Snir Broshi]

Yongxi Lin (Aaron) said:

You should use obtain instead of let in your last line.

Inlining any of the 3 definitions also gets rid of the error, but I think all of these (admittedly weird since it's a #mwe) operations are legitimate

[Snir Broshi]

Reported as lean4#11626

[Snir Broshi]

Somehow ran into another unknown free variable for unrelated reasons: lean4#11692