chore: adaptations for lean4#12459

[sgraf812]

Summary

• Updates lean-toolchain for testing lean4#12459 (new do elaborator)
• Adapts Qq/Match.lean for the new doLetElse syntax which now includes an optional body as part of its syntax
• Fixes a bug where the do elaborator's expansion of doLetElse would default the body to pure PUnit.unit when none was provided, causing type mismatches in mixed Qq patterns (e.g., (2, ~q(1)), ⟨~q(Nat), ~q($n)⟩)
• The fix builds nested doLetElse structures (from inside out) so that every let pat := rhs | alt always has an explicit body

Test plan

• lake build passes (all modules including QqTest.matching)

🤖 Generated with Claude Code

[kim-em]

Merged into nightly-testing. Thanks!