feat: port Batteries.WF for executable well-founded fixpoints

[joehendrix]

This PR ports Batteries.WF to Init.WFC for executable well-founded fixpoints. It introduces csimp theorems to replace the recursors and non-executable definitions with executable definitions.

This ocassionally comes up on Zulip as it prevents admiting definitions generated from well-founded induction. (e.g., #lean4 > Computable WellFounded.fix and #mathlib4 > Why Nat.find is computable, when Wellfounded.fix isn't?).

This was motivated by running into poor elaboration performance with recursive definitions involving complex inductive types generated by a custom elaborator. It would be helpful to explore bypassing the elaborator and generating elaborated terms directly, but this requires an executable fixpoint (such as WellFounded.fixC introduced in batteries).

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c4477939d07116df842258bf8f9267deea51c466 --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-11 20:14:27)
• 💥 Mathlib branch lean-pr-testing-11620 build failed against this PR. (2025-12-12 10:18:34) View Log
• 💥 Mathlib branch lean-pr-testing-11620 build failed against this PR. (2025-12-12 23:00:48) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c4477939d07116df842258bf8f9267deea51c466 --onto eee58f4506d28a14c9a171165f999445a0663d93. You can force reference manual CI using the force-manual-ci label. (2025-12-11 20:14:29)
• ✅ Reference manual branch lean-pr-testing-11620 has successfully built against this PR. (2025-12-12 10:19:03) View Log
• 🟡 Reference manual branch lean-pr-testing-11620 build against this PR didn't complete normally. (2025-12-12 10:19:42) View Log

[nomeata]

This was motivated by running into poor elaboration performance with recursive definitions involving complex inductive types generated by a custom elaborator

Do we have an issue tracking this?

But assuming the compiled code you get from using this here is reasonable, I'm happy to have this in core.

We should make wrap public, it's useful generally.

[joehendrix]

No issue tracking -- happy to add one if that is helpful.

For performance, I did a little bit of testing with a function defined using this and another defined relying on the elaborator introducing well-founded induction; profiling results in #eval were similar.

I'd naively expect the compiler may do better with the elaborator generated code, since I assume that generates better code, but I haven't really tested it.

[nomeata]

Happy to merge without an issue once CI is happy.

[joehendrix]

CI checks seem to be working.

I looked into the Batteries failure, and it is the expected name failures. I think that's a trivial fix, but I don't have permission to push to batteries.