chore: bump mathlib to be31cde, fix breaking changes

[mathlib-nightly-testing]

Bump mathlib dependency to be31cde: refactor(Probability/Distributions/Uniform): change uniformOfFinset and ofMultiset from PMF to Measure (#42909) (2026-10-05)
Previously at: 9a6fbe0: feat(MeasureTheory/Measure/Typeclasses/SFinite): finite sets have finite measure (#44381) (2026-10-03)

Closes #1078

Failure log from the validation run: download (link expires after 1 year)

---

This PR bumps mathlib to an identified incompatible (first-known-bad) commit (be31cde) so you can reproduce and fix the incompatibility locally by checking out this branch.

Opened automatically by downstream-reports/track-incompatibility via this workflow run.

[SamuelSchlesinger]

I've migrated to measure theory for the impacted aspects of this PR. Curious to get anyone else's perspective. For me, this lowers my comprehension and requires me to think about measures and what these terms mean more than I want to. However, I am not opposed to this if Mathlib is going to deprecate PMF after all.

Some more eyes other than me would be ideal, but I'll continue to think about this tonight and tomorrow.

[SamuelSchlesinger]

cc @crei

[chenson2018]

Just to repeat some conversation that Sam and I had earlier. There are a couple of short-term options:

• The first option is to keep the changes they've already pushed. I would do this if you're fairly certain that we'd like to head in the same direction as Mathlib here. (NB: if your pushed changes used AI, please edit to PR description to say so as usual)
• An alternative if you're not sure yet how you'd like to refactor: we can kick the can and have six months until these are removed from Mathlib. You would turn off warnings for just these specific theorems and merge essentially unchanged. I'd ask if you do this that you follow up on Zulip to make a more permanent decision.

I typically advocate very hard for staying aligned with Mathlib, and Sam mentioned some evidence that it could be useful here, along with innovations in do notation (see Lean Machine Learning > Do notation for Giry monad for instance) that might make working with things easier. I know there were some arguments from the other as as well though in CSLib > PMF monad and discrete probability.

I'll leave all this to your discretion, I just ask that one of these options gets merged in this PR fairly soon, please feel free to merge as soon as you decide. (There is not a rush, but I usually try to not go more than a couple of days before merging these.)