feat: infer mutual structural recursion

[nomeata]

the support for mutual structural recursion (new since #4575) is extended so that Lean tries to infer it even without annotations.

• The error message when termination checking fails looks quite different now. Maybe a bit better, maybe with more room for improvements.
• If there are too many combinations (with an arbitrary cut-off) for a given argument type, it will just give up and ask the user to use termination_by structural.
• It is now legal to specify termination_by structural on not necessarily all functions of a clique; this simply restricts the combinations of arguments that Lean considers.

[leanprover-community-mathlib4-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 c01e003b49c4b75da1eec88155430f6ce6310750 --onto 582d6e7f7168e0dc0819099edaace27d913b893e. (2024-07-10 16:31:41)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5f70c1ca64a2c05a5866c47b9eb80a92034433ec --onto ce8a13072496063ed1b6305ba8dc68d6680eada3. (2024-07-11 08:03:13)
• ✅ Mathlib branch lean-pr-testing-4718 has successfully built against this PR. (2024-07-12 09:24:00) View Log
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-07-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-07-12 10:03:36)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ae49c3abaade6f2f4420665b4a67d93069fd81 --onto 5f70c1ca64a2c05a5866c47b9eb80a92034433ec. (2024-07-13 06:57:48)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1118978cbb344e6570729a70c74cd0d3121e8c35 --onto 5f70c1ca64a2c05a5866c47b9eb80a92034433ec. (2024-07-13 09:06:09)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f99427bd1ac6595f9717796b7fabe6c6e8791e14 --onto 5f70c1ca64a2c05a5866c47b9eb80a92034433ec. (2024-07-15 09:36:11)