chore: fix namespaces in recently upstreamed tactics

[kim-em]

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 612d97440b4c0b3da967eaf041687b0f2c468f3a --onto 317adf42e92a4dbe07295bc1f0429b61bb8079fe. (2024-03-14 01:31:20)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8d2adf521d2b7636347a5b01bfe473bf0fcfaf31 --onto 317adf42e92a4dbe07295bc1f0429b61bb8079fe. (2024-03-14 02:21:47)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9ee10aa3ebb8e518132873e3d98a13dd7df5e9f7 --onto 0ec8862103e397715854a7a6962ce542bba4884d. (2024-03-17 06:43:29)