feat: upstream apply helper tactics from Mathlib

[kim-em]

These are used in Mathlib's congr! and convert tactics, which will be upstreamed soon.

[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:27:59)
• ❗ 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:23:11)