Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-17 14:58 88b8a77d

View on Github →

chore(topology/basic): backport a generalization to Sort (#18544) mathport currently complains that these don't align.

Estimated changes