Make `LE` extend `LT`

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The LE and LT classes are independent of each other but they are very often used as a pair. In the same spirit as issue #1777, I propose to have LE extend LT with a default value as follows:

/-- `LE α` is the typeclass which supports the notation `x ≤ y` where `x y : α`.-/
class LE (α : Type u) extends LT α where
  /-- The less-equal relation: `x ≤ y` -/
  le : α → α → Prop
  /-- Default less-than relation -/
  lt x y := And (le x y) (Not (le y x))

(Since this is in Init.Prelude notations for And and Not cannot be used yet.) I have a PR candidate that shows that the resulting changes to Lean are relatively minor: https://github.com/fgdorais/lean4/tree/le_lt

The main benefit is, of course, to simplify a common use case where LE and LT are intended to be used together.

Existing user code would not require much change. Indeed,

instance : LT α where lt := myLt
instance : LE α where le := myLe

has exactly the same effect as

instance : LE α where
  le := myLe
  lt := myLt

Unfortunately,

instance : LE α where le := myLe
instance : LT α where lt := myLt

would result in two LT instances but the second one would shadow the default instance from LE. This means that existing code will compile as before, but there is a gotcha for new declarations that require LE but not LT where < would mean the default instance in the context of this declaration.

The default definition of LE.lt is correct in nearly all use cases in the sense that the default is logically equivalent to the intended one (although different definition is sometimes preferable). The ≤ relation is rarely used in a context where a companion < doesn't make sense, so having LE extend LT would rarely lead to spurious definitions. In contrast, < is sometimes used in contexts where there is no clear choice for a companion ≤ ("less-than or equal" is not always the right choice) or where such a companion doesn't make sense (when < is not irreflexive, for example). Thus it makes sense to keep LT as a standalone class for cases where a companion LE class is not desirable.

Start in Init.Prelude, where the LE and LT classes and their notations are defined. Compare the proposed implementation with the existing le_lt branch, then trace affected instance declarations and compile the relevant Lean sources. Done means LE extends LT with the proposed default lt behavior while preserving existing user code and avoiding unintended instance shadowing.