Bumping lean versions

Stream: Formal conjectures

[Bolton Bailey]

What is the formal conjectures policy on bumping lean versions? I see that the repo is currently on v4.22.0, and when I experiment with bumping it to v4.25.2, I notice that there are a few changes that need to be made and that a few "ForMathlib" lemmas can be deleted. Does the repo accept bumping PRs?

[Moritz Firsching]

We are happy to about pull requests bumping the lean version (@Kim Morrison has made one for bumping to v4.18), but might take a bit to actually merge them.
Also we strive to provide all intermediate versions, so best would be a chain of commits bumping to all intermediate versions. We have done so ever since v4.17, so there are tags for for versions in between up to v4.22 currently.