feat: builtin as_aux_lemma tactic and tree_tac simp attribute

[datokrat]

This PR adds a builtin tactic and a builtin attribute that are required for the tree map. The tactic, as_aux_lemma, can generally be used to wrap the proof term generated by a tactic sequence into a separate auxiliary lemma in order to keep the proof term small. This can, in rare cases, be necessary if the proof term will appear multiple times in the encompassing term. The new attribute, Std.Internal.tree_tac, is internal and should not be used outside of Std.

[datokrat]

Is it correct that such a purely internal change should not be part of the changelog?

[nomeata]

Is there a reason why as_aux_lemma isn’t a generally useful tactic for our users? Then it’s changelog-language

[leanprover-community-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch lean-pr-testing-6823 built against this PR, but testing failed. (2025-01-28 18:32:55) View Log
• ❌ Mathlib branch lean-pr-testing-6823 built against this PR, but testing failed. (2025-01-29 08:40:30) View Log
• ✅ Mathlib branch lean-pr-testing-6823 has successfully built against this PR. (2025-01-30 09:13:47) View Log
• ✅ Mathlib branch lean-pr-testing-6823 has successfully built against this PR. (2025-01-30 10:23:12) View Log
• 🟡 Mathlib branch lean-pr-testing-6823 build against this PR was cancelled. (2025-01-31 08:55:30) View Log
• ✅ Mathlib branch lean-pr-testing-6823 has successfully built against this PR. (2025-01-31 09:42:55) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 832d7c500d709deb5e7f0a5a6fd0f01865d1a303 --onto d68c2ce28bc11ec0271a97aa7a7316905f15a484. (2025-02-03 08:08:41)

[datokrat]

I'm not sure yet whether the

Is there a reason why as_aux_lemma isn’t a generally useful tactic for our users? Then it’s changelog-language

@nomeata The reason I was hesitating to think of this as a tactic used outside lean itself is because using as_aux_lemma seems more like a hack that we hopefully might not need anymore in the future. On the other hand, if we find it helpful right now, why not other people struggling with large proof terms, too? So I think I'll still keep the syntax protected, in order not to pollute the global namespace with obscure tactics, but add this to the language changelog.