Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-19 18:47 730c6d4c

View on Github →

chore(order/initial_seg): tweak subsingleton_of_trichotomous_of_irrefl (#18749) We rename it, turn it into an instance, and golf the next instance with it.

Estimated changes