feat: structural recursion over nested datatypes

[nomeata]

This now works:

inductive Tree where | node : List Tree → Tree

mutual
def Tree.size : Tree → Nat
  | node ts => list_size ts

def Tree.list_size : List Tree → Nat
  | [] => 0
  | t::ts => t.size + list_size ts
end

It is still out of scope to expect to be able to use nested recursion (e.g. through List.map or List.foldl) here.

Depends on #4718.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ 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 13:34:32)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 891824bc51726cb99e6229be078d6757111b9b57 --onto 5f70c1ca64a2c05a5866c47b9eb80a92034433ec. (2024-07-12 22:26:44)
• ❗ 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:55:02)
• ❗ 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:03:22)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3ab2c714ec03550bf67f8fadb5344419fb40a748 --onto 5f70c1ca64a2c05a5866c47b9eb80a92034433ec. (2024-07-15 10:29:12)