unknown free variable on `obtain`

Stream: lean4

[Aaron Liu]

Here's a mwe

example (h : ∃ a : Nat, (∃ b, a = b + 1) ∧ 0 ≤ a) : True := by
  obtain ⟨_, ⟨b, rfl⟩, put_your_cursor_here_and_look_at_the_infoview⟩ := h
  trivial

[Aaron Liu]

The error is

Error updating: Error fetching goals: Rpc error: InternalError: unknown free variable '_fvar.161'. Try again.

[Aaron Liu]

This kind of obtain pattern turn up for membership in the image of a set.