fix: collapse empty DiscrTree tries

[robsimmons]

This PR ensures that DiscrTree operations collapse any trie nodes that end up empty.

This change allows mapArraysM to properly implement Aesop's filterDiscrTreeM in the downstream adaptation PR, which also deprecates Trie.isEmptyTrie in favor of the now-upstreamed Trie.isEmptyNode. Following Aesop's lead, this PR also adds @[specialize] annotations to the recursive portion of for mapArraysM and to the similarly-patterned foldM and foldValuesM.

Three new test files provide coverage of these and other DiscrTree operations. This PR (and the tests) are intended to lay groundwork for #14805.

[downstream-lean4]

The adaptation PR for this PR is leanprover/downstream-lean4#24.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-11 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. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-19 17:45:27)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-20 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. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-20 13:15:47)
• ✅ Mathlib branch lean-pr-testing-14844 has successfully built against this PR. (2026-08-21 02:32:05) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e9c0364b5bb39bf23b1a7279d4d4be29b992f368 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-21 03:15:49)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-19 17:45:30)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-20 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-20 13:15:49)
• 🟡 Reference manual branch lean-pr-testing-14844 build against this PR didn't complete normally. (2026-08-21 01:12:52) View Log
• ✅ Reference manual branch lean-pr-testing-14844 has successfully built against this PR. (2026-08-21 01:13:34) View Log
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e9c0364b5bb39bf23b1a7279d4d4be29b992f368 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-21 03:15:51)

[robsimmons]

!bench

[leanprover-radar]

Benchmark results for 7b84a7f against 7976735 are in. No significant results found. @robsimmons

• 🟥 build//instructions: +1.2G (+0.01%)

Small changes (2✅, 1🟥)

• ✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB//instructions: -23.3M (-1.05%)
• ✅ build/module/Lean.Meta.Tactic.Ext//instructions: -18.7M (-1.18%)
• 🟥 compiled/rbmap_fbip//maxrss: +348kiB (+0.35%)

[robsimmons]

!bench

[leanprover-radar]

Benchmark results for c84b5e1 against 7976735 are in. No significant results found. @robsimmons

• ✅ build//instructions: -189.8M (-0.00%)

Small changes (3✅)

• ✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB//instructions: -22.6M (-1.02%)
• ✅ build/module/Lean.Meta.DiscrTree.Util//instructions: -7.5M (-0.61%)
• ✅ build/module/Lean.Meta.Tactic.Ext//instructions: -18.0M (-1.13%)

[robsimmons]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@6926656 against leanprover-community/mathlib4-nightly-testing@5a95bed are in. No significant results found. @robsimmons

• 🟥 build//instructions: +93.4G (+0.07%)

Small changes (1✅, 2🟥)

• ✅ build/module/Aesop.Util.UnionFind//instructions: -26.0M (-1.50%)
• 🟥 build/module/Mathlib.FieldTheory.Cardinality//instructions: +76.4M (+1.34%)
• 🟥 build/module/Mathlib.MeasureTheory.Measure.Lebesgue.Complex//instructions: +88.4M (+1.22%)