feat: upstream Std's rfl tactic

[semorrison]

This allows tagging lemmas with @[refl], that will then by used by rfl.

This is preparatory to upstreaming Mathlib's convert tactic.

[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:35:38)
• ❗ 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:22:15)
• ❗ 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 07:09:26)

[nomeata]

Once this is merged we can tackle #3302