feat: support idents in auto tactics

[digama0]

This is still experimental, but it implements identifier support in auto tactics "in the obvious way". It also converts quoteAutoTactic to generate Expr directly instead of going via syntax (this doesn't have any effect other than increasing compile cost AFAICT).

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std CI can not be attempted yet, as the nightly-testing-2024-02-14 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-02-14 08:48:31)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1d17c7df2beafbef0b480aa68d395b37db278732 --onto 806e41151b6eb645e4ed5a40915b94b99f933564. (2024-05-02 22:18:12)

[kim-em]

What's the status of this PR? It would be good to have a test showing the changed behaviour. It's clear there's enthusiasm for this one, so it would be nice to get in.