bump to v4.33.1

[taterowney]

Description

Good afternoon! I'm using IrisLean for a project, but wanted to use some features of Lean 4.33.1. I've bumped the toolchains and made minimal edits to ensure it all builds.
A summary of what was changed:

• Mark a few definitions implicit_reducible (A in Iris.Algebra.COFESolver, MaxPrefixList in Iris.Algebra.MaxPrefixList, and MonoList in Iris.Algebra.Lib.MonoList) to ensure later unfolding-related proofs still typecheck
• Change a couple of explicitly provided (i)simp lemmas in Iris.Instances.IProp.Instance and Iris.ProgramLogic.Atomic to make proofs still work
• Fixing a bunch of linter.ambiguousOpen warnings in ~70 files by explicitly providing the full namespace to be opened (this is the only reason the diff touches so many files). Disclaimer: AI was used to automatically do this boilerplate stuff.

Would greatly appreciate feedback/suggestions. Thank you very much!

Fixes # (issue number)

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.

[markusdemedeiros]

Thank you for your PR! There are one or two features we are hoping to land before making this change, and we want to make some changes re. linters and namespacing in order to do it properly. Expect a week or two before this is picked up. In the meantime, I hope this means you can continue your project, thank you for the start :)