chore: update Lean to v4.33.1

[kim-em]

This PR updates the toolchain from leanprover/lean4:v4.29.0 to leanprover/lean4:v4.33.1, moving Mathlib and doc-gen4 to their matching releases. lake build and lake test both pass, and no sorry is introduced.

Four Lean changes account for most of the churn. rw [d] on a Prop-valued definition no longer finds its equation lemmas, so zCDPBound, ACNeighbour, PureDP and DP_singleton unfold with simp only instead; unfold probWhileCut likewise becomes simp only [probWhileCut]. A match no longer infers a non-dependent motive unaided, and simp is stronger in ways that make a number of rewrites, conv navigations and their successors redundant — those are dropped rather than repaired.

The Mathlib side is mostly renames and signature changes: Int.natAbs_ofNat' becomes Int.natAbs_natCast, List.foldl_eq_of_comm' becomes the instance-based List.foldl_cons_eq_apply_foldl (which brings a RightCommutative instance and an import of Mathlib.Data.List.Fold), and zero_le, DFunLike.coe_injective' and ENNReal.ofReal_pow all changed arity or field name. gauss_term_ℂ becomes a def: its return type C(ℝ, ℂ) is not a class, so it was never usable as an instance, and Lean now rejects it.

Three proofs are restated rather than patched. ereal_smul_le_left no longer degrades ↑s into raw some (some s) and back, which was what broke it. UniformSample_apply merges two rewrites into one, since simp now reaches the combined form directly, cutting 48 lines to 6. AboveThresh gains three small lemmas — sv4_probWhileCut_succ, sv4_probWhileCut_succ_false and tsum_indicator_pure — that state the loop's one-step unrolling and the mass of a point distribution once, where the inline versions had been repeated and were sensitive to how sv1_state and sv4_state display.

🤖 Prepared with Claude Code

[markusdemedeiros]

Thanks Kim!