feat: let `unfold` do zeta-delta reduction of local definitions

[kmill]

This is "upstreaming" mathlib's unfold_let tactic by incorporating its functionality into unfold. Now unfold can, in addition to unfolding global definitions, unfold local definitions.

An improvement to unfold_let is that it beta reduces unfolded local functions. A change is that it no longer removes unused let bindings.

Two features not present in unfold are that (1) unfold_let with no arguments does zeta delta reduction of all local definitions, and also (2) unfold_let can interleave unfoldings (in contrast, unfold a b c is exactly the same as unfold a; unfold b; unfold c).

Closes RFC #4090

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-07-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-07-25 22:17:58)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e5e577865fe74ad17182346a225f8f209fa6e2e4 --onto 3ec55d3d498ce361f5886afee516d16df5cbd6fc. (2024-09-07 21:50:54)

[kmill]

This is still a draft. It needs

• updated tactic docstrings
• similar changes to the conv version of unfold
• (perhaps) an additional purely zeta delta tactic that's closer to unfold_let

[kmill]

@semorrison Would you mind taking a look at this change to the unfold tactic? It'd be nice to get some eyes on it before merging.

Something I didn't get to is create a zeta_delta tactic (which would be a true upstreaming of unfold_let), but it shouldn't be very much work to define it from here.