Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-20 01:45 cd343474

View on Github →

chore(*): remove uses of universe variable (#9794) Most of these uses are relics of when the distinction between universe and universe variable was more significant. There is still a difference inside sections, but it's an edge case and I don't think any of these uses are consciously trying to handle the edge case.

Estimated changes

modified theorem classical.nonempty_pi
modified theorem nonempty.exists
modified theorem nonempty.forall
modified theorem nonempty.map
modified theorem nonempty_plift
modified theorem nonempty_pprod
modified theorem nonempty_psigma
modified theorem nonempty_psum
modified theorem nonempty_subtype