fix: bv_normalize loose mvars

[hargoniX]

bv_normalize would just silently drop other goals if called while not focused on a singular goal, for example:

theorem mvarid (x y : Bool) (h : x ∨ y) : y ∨ x := by
  cases h
  bv_normalize
  -- we want to write another bv_normalize here but all goals are gone

Would make the second subgoal disappear and then throw an error about meta variables in the kernel.

[tobiasgrosser]

Thank you.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fd08c9206097781c9bca8f61531de6a0479df0f8 --onto 0fcee100e7ea382069854d91e854265c56b54428. (2024-11-01 15:19:50)