fix: recognize long list literals

[sankalpsthakur]

This PR makes Expr.listLit? recognize list literals that use Lean's let-bound expansion for 33 or more elements.

Short list literals elaborate directly to nested List.cons applications. Longer literals are partitioned through intermediate let bindings to avoid deeply nested expressions, but the recognizer did not zeta-reduce those bindings and returned none.

Unwrap encountered letEs while traversing the literal and add a focused 33-element regression.

Closes #7730

Validation

• Added tests/elab/issue7730.lean
• Exact PR-history search found no competing implementation
• Full Lean CI is the authoritative validation

AI assistance

AI tools assisted with issue triage, source tracing, implementation, and regression preparation. I reviewed the list-literal macro threshold, recognizer behavior, and final diff.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 23d17351ab630c393aadb7f8c97ef9b8ee633cdb --onto 5b8d06c1764fa367a1e27b3e89f64667eac425af. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-02 06:50:41)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 945e78b86645b179655123cd2fdba83d89d28d07 --onto 110db9cb751afaee8b2ac344887d6c7e632f77b4. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-04 02:10:20)

[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 23d17351ab630c393aadb7f8c97ef9b8ee633cdb --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-02 06:50:42)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 945e78b86645b179655123cd2fdba83d89d28d07 --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-04 02:10:22)