Unifying relation typeclasses

Stream: mathlib4

[Violeta Hernández]

Hopefully I'm not opening Pandora's box here, but I think we have somewhat of an unfortunate situation around unbundled relation typeclasses. Instead of having one single spelling, we seem to have three spellings used throughout different parts of Lean/Mathlib.

a) What appears to be the most common one, the docs#IsRefl, docs#IsIrrefl, etc. typeclasses defined in Mathlib.Order.Defs.Unbundled.
b) The predicates docs#Reflexive, docs#Irreflexive, etc. also defined lower in the file, which see some but seemingly not nearly as much use.
c) The Core typeclasses docs#Std.Refl, docs#Std.Irrefl, etc. which see zero use in Mathlib.

This became a particular annoyance to me recently, when I found out I couldn't use the new List.le lemmas in Core because there's no useful instances for the Std typeclasses they use.

[Violeta Hernández]

Personally I think the predicates from (b) can just be deprecated, since using a typeclass rather than a "raw" proposition provides useful functionality (for instance, one can use theorems about List.sort (· < ·) or List.sort (· ≤ ·) and have transitivity inferred). Whether we replace the core predicates by the Mathlib ones or the other way around I don't really care for.