feat: extract_lets and lift_lets tactics

[kmill]

This PR implements tactics called extract_lets and lift_lets that manipulate let/let_fun expressions. The extract_lets tactic creates new local declarations extracted from any let and let_fun expressions in the main goal. For top-level lets in the target, it is like the intros tactic, but in general it can extract lets from deeper subexpressions as well. The lift_lets tactic moves let and let_fun expressions as far out of an expression as possible, but it does not extract any new local declarations. The option extract_lets +lift combines these behaviors.

This is a re-implementation of extract_lets and lift_lets from mathlib. The new extract_lets is like doing lift_lets; extract_lets, but it does not lift unextractable lets like lift_lets. The lift_lets; extract_lets behavior is now handled by extract_lets +lift. The new lift_lets tactic is a frontend to extract_lets +lift machinery, which rather than creating new local definitions instead represents the accumulated local declarations as top-level lets.

There are also conv tactics for both of these. The extract_lets has a limitation due to the conv architecture; it can extract lets for a given conv goal, but the local declarations don't survive outside conv. They get zeta reduced immediately upon leaving conv.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-6432 build failed against this PR. (2024-12-21 02:10:43) View Log
• 💥 Mathlib branch lean-pr-testing-6432 build failed against this PR. (2024-12-21 03:25:31) View Log
• 💥 Mathlib branch lean-pr-testing-6432 build failed against this PR. (2024-12-21 03:40:49) View Log
• ✅ Mathlib branch lean-pr-testing-6432 has successfully built against this PR. (2024-12-21 05:03:14) View Log
• 💥 Mathlib branch lean-pr-testing-6432 build failed against this PR. (2024-12-21 20:43:06) View Log
• ✅ Mathlib branch lean-pr-testing-6432 has successfully built against this PR. (2024-12-21 21:56:41) View Log
• ✅ Mathlib branch lean-pr-testing-6432 has successfully built against this PR. (2024-12-22 10:13:41) View Log
• ✅ Mathlib branch lean-pr-testing-6432 has successfully built against this PR. (2024-12-23 09:50:09) View Log
• ✅ Mathlib branch lean-pr-testing-6432 has successfully built against this PR. (2024-12-31 15:28:59) View Log
• ✅ Mathlib branch lean-pr-testing-6432 has successfully built against this PR. (2024-12-31 20:30:48) View Log