lean-pr-testing-7352

Stream: PR reviews

[Kim Morrison]

The branch#lean-pr-testing-7352 makes adaptations for lean4#7352, which fixes defeq abuse around the Id monad.

There are few places in the "Haskell" corner of Mathlib where the existing proof rely on this defeq abuse, and need to be rewritten. As these places are unused elsewhere, and have not received any attention for a while, for now I am simply commenting them out, leaving an adaptation note in place. Search for https://github.com/leanprover/lean4/pull/7352 to find these.

Contributors are very welcome to restore these facts by fixing them. Please insert Id.run wherever needed to convert from Id α to α

You can push changes directly to branch#lean-pr-testing-7352 for now.

[Kim Morrison]

Oh --- and here's the diff: https://github.com/leanprover-community/mathlib4/compare/nightly-testing-2025-05-16...lean-pr-testing-7352

[Eric Wieser]

Maybe it makes sense to let #25098 land first, and wait for the next nightly testing branch?