rename bvar

Stream: mathlib4

[Yury G. Kudryashov]

I tried to use docs#rename_bvar on a goal with lots of x/a variables introduced by simp and found 3 issues:

• the syntax expects rename_bvar a → b, not rename_bvar a b as the documentation says; I'll open a PR tonight or tomorrow;
• the syntax doesn't support renaming more than 1 variable;
• if I have x at more than 1 level, then Lean pretty prints them as x and x_1 but rename_bvar renames all of them at once.