chore: bump version to 4.32

[ayhon]

Description

Bump Lean version to v4.32, with some fixes that were required by the bump in version.

[ayhon]

I seem to be getting a bunch of errors from linters. I'm surprised these were not a problem before, is this a consequence of bumping versions?

[ayhon]

I addressed the linter issues. They can be summarized as:

1. Using def instead of theorem (which also meant that we needed to give an extra @[reducible] or @[implicit_reducible] annotation)
2. Universe polymorphic definitions which are always used by setting all universes to the same value.

For 1 I opted to simply change def to theorem. For 2 I have opted to just disable the linter where necessary for now, until we make a decision on whether having, for example, IProp.{u} instead of IProp.{u1,u2,u3} makes sense.

[lzy0505]

Thanks for the PR. Can you open an issue for 2?

[markusdemedeiros]

@ayhon Thanks for being on top of this!