chore: bump toolchain to v4.33.1

[kim-em]

This PR bumps the Lean toolchain from v4.23.0 to v4.33.1 and refreshes the Lake manifest.

Aesop, Plausible and lean4-cli move from v4.23.0 to v4.33.0, their most recent tags.

Five adaptations were needed across the ten releases:

• ForIn.forIn no longer takes a [Monad m] binder on the field itself, so the Iterator instance drops its redundant one.
• String.drop returns a String.Slice, so Dtype.fromNpyString converts back with .toString.
• #guard_msgs expectations updated: declaration uses 'sorry' is now written with backticks.
• In Broadcast, an aesop call no longer makes progress; the if is now discharged explicitly from the ordering hypothesis.
• ByteArray.replicateSize needs a final rfl.

🤖 Prepared with Claude Code

[SmoothThunk]

These changes have been done in PR #100 I'll be merging them soon