The behavior of the "obtain" tactic is different from the description in section 3.2

[ctchou]

In section 3.2, it is stated that:

Think of the first obtain instruction as matching the “contents” of ubf with the given pattern and assigning the components to the named variables. rcases and obtain are said to destruct their arguments, though there is a small difference in that rcases clears ubf from the context when it is done, whereas it is still present after obtain.

However, that is not what I see. In the example that uses "obtain", when my cursor is just before the word "exact", I see the following goal:

which is identical to the goal I see when my cursor is at the word "exact" in the example that uses "rintro", in which both "ubf" and "ubg" have disappeared from the context.

I'm using:

Lean (version 4.13.0-rc3, arm64-apple-darwin23.6.0, commit 01d414ac36dc, Release)

under VScode on an M1 MacBook Air.