doc-next-gen

Init.Data.Ord

Module docstring

{}

Ordering inductive
Full source 
/--
The result of a comparison according to a total order.

The relationship between the compared items may be:
 * `Ordering.lt`: less than
 * `Ordering.eq`: equal
 * `Ordering.gt`: greater than
-/
inductive Ordering where
  | /-- Less than. -/
    lt
  | /-- Equal. -/
    eq
  | /-- Greater than. -/
    gt
deriving Inhabited, DecidableEq
Comparison result in a total order
Informal description
The inductive type `Ordering` represents the possible results of a comparison in a total order. It has three constructors: - `Ordering.lt`: indicating that the first item is less than the second, - `Ordering.eq`: indicating that the two items are equal, - `Ordering.gt`: indicating that the first item is greater than the second.
instInhabitedOrdering instance
: Inhabited✝ (@Ordering)
Full source 
Inhabited, DecidableEq
The Inhabited Instance for Ordering
Informal description
The type `Ordering` is inhabited, with a default element.
instDecidableEqOrdering instance
: DecidableEq✝ Ordering
Full source 
DecidableEq
Decidable Equality for Ordering Results
Informal description
The type `Ordering` has decidable equality. That is, for any two comparison results `x` and `y` of type `Ordering`, it is constructively decidable whether `x = y` holds.
Ordering.swap definition
: Ordering → Ordering
Full source 
/--
Swaps less-than and greater-than ordering results.

Examples:
 * `Ordering.lt.swap = Ordering.gt`
 * `Ordering.eq.swap = Ordering.eq`
 * `Ordering.gt.swap = Ordering.lt`
-/
def swap : Ordering → Ordering
  | .lt => .gt
  | .eq => .eq
  | .gt => .lt
Swap of ordering results
Informal description
The function swaps the ordering results between less-than and greater-than while keeping equality unchanged. Specifically: - $\mathrm{swap}(\mathrm{lt}) = \mathrm{gt}$ - $\mathrm{swap}(\mathrm{eq}) = \mathrm{eq}$ - $\mathrm{swap}(\mathrm{gt}) = \mathrm{lt}$
Ordering.then definition
(a b : Ordering) : Ordering
Full source 
/--
If `a` and `b` are `Ordering`, then `a.then b` returns `a` unless it is `.eq`, in which case it
returns `b`. Additionally, it has “short-circuiting” behavior similar to boolean `&&`: if `a` is not
`.eq` then the expression for `b` is not evaluated.

This is a useful primitive for constructing lexicographic comparator functions. The `deriving Ord`
syntax on a structure uses the `Ord` instance to compare each field in order, combining the results
equivalently to `Ordering.then`.

Use `compareLex` to lexicographically combine two comparison functions.

Examples:
```lean example
structure Person where
  name : String
  age : Nat

-- Sort people first by name (in ascending order), and people with the same name by age (in
-- descending order)
instance : Ord Person where
  compare a b := (compare a.name b.name).then (compare b.age a.age)
```

```lean example
#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Dana", 50⟩
```
```output
Ordering.gt
```

```lean example
#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 50⟩
```
```output
Ordering.gt
```

```lean example
#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 20⟩
```
```output
Ordering.lt
```
-/
@[macro_inline] def «then» (a b : Ordering) : Ordering :=
  match a with
  | .eq => b
  | a => a
Lexicographic combination of comparison results
Informal description
Given two comparison results `a` and `b` of type `Ordering`, the operation `a.then b` returns `b` if `a` is `Ordering.eq`, and otherwise returns `a`. This operation is short-circuiting in that `b` is not evaluated when `a` is not `Ordering.eq`. This is particularly useful for constructing lexicographic comparison functions, where subsequent comparisons are only performed if prior comparisons yield equality.
Ordering.isEq definition
: Ordering → Bool
Full source 
/--
Checks whether the ordering is `eq`.
-/
def isEq : Ordering → Bool
  | eq => true
  | _ => false
Check for equality in comparison result
Informal description
The function checks if a given comparison result is equality. Specifically, it returns `true` if the input is `Ordering.eq`, and `false` otherwise (i.e., for `Ordering.lt` or `Ordering.gt`).
Ordering.isNe definition
: Ordering → Bool
Full source 
/--
Checks whether the ordering is not `eq`.
-/
def isNe : Ordering → Bool
  | eq => false
  | _ => true
Check for inequality in comparison result
Informal description
The function checks if a given comparison result is not equality. Specifically, it returns `false` if the input is `Ordering.eq`, and `true` otherwise (i.e., for `Ordering.lt` or `Ordering.gt`).
Ordering.isLE definition
: Ordering → Bool
Full source 
/--
Checks whether the ordering is `lt` or `eq`.
-/
def isLE : Ordering → Bool
  | gt => false
  | _ => true
Check for less-than-or-equal in comparison result
Informal description
The function checks if a given comparison result indicates "less than or equal to". Specifically, it returns `true` if the input is `Ordering.lt` or `Ordering.eq`, and `false` if the input is `Ordering.gt`.
Ordering.isLT definition
: Ordering → Bool
Full source 
/--
Checks whether the ordering is `lt`.
-/
def isLT : Ordering → Bool
  | lt => true
  | _ => false
Check for less-than in comparison result
Informal description
The function checks if a given comparison result indicates "less than". Specifically, it returns `true` if the input is `Ordering.lt`, and `false` otherwise (for `Ordering.eq` or `Ordering.gt`).
Ordering.isGT definition
: Ordering → Bool
Full source 
/--
Checks whether the ordering is `gt`.
-/
def isGT : Ordering → Bool
  | gt => true
  | _ => false
Check for greater-than in comparison result
Informal description
The function checks if a given comparison result indicates "greater than". Specifically, it returns `true` if the input is `Ordering.gt`, and `false` otherwise (for `Ordering.lt` or `Ordering.eq`).
Ordering.isGE definition
: Ordering → Bool
Full source 
/--
Checks whether the ordering is `gt` or `eq`.
-/
def isGE : Ordering → Bool
  | lt => false
  | _ => true
Check for greater-than-or-equal in comparison result
Informal description
The function checks if a given comparison result indicates "greater than or equal to". Specifically, it returns `false` if the input is `Ordering.lt`, and `true` otherwise (for `Ordering.eq` or `Ordering.gt`).
Ordering.isLT_lt theorem
: lt.isLT
Full source 
@[simp]
theorem isLT_lt : lt.isLT := rfl
`isLT` returns true for less-than comparison
Informal description
The function `isLT` applied to the comparison result `lt` (less than) returns `true`.
Ordering.isLE_lt theorem
: lt.isLE
Full source 
@[simp]
theorem isLE_lt : lt.isLE := rfl
Less-than comparison satisfies isLE condition
Informal description
For the comparison result `lt` (less than), the function `isLE` returns `true`.
Ordering.isEq_lt theorem
: lt.isEq = false
Full source 
@[simp]
theorem isEq_lt : lt.isEq = false := rfl
Equality Check for Less Than Comparison is False
Informal description
For the comparison result `lt` (less than), the equality check function `isEq` returns `false`.
Ordering.isNe_lt theorem
: lt.isNe = true
Full source 
@[simp]
theorem isNe_lt : lt.isNe = true := rfl
Inequality Check for Less Than Comparison is True
Informal description
For the comparison result `lt` (less than), the inequality check function `isNe` returns `true`.
Ordering.isGE_lt theorem
: lt.isGE = false
Full source 
@[simp]
theorem isGE_lt : lt.isGE = false := rfl
`isGE` returns false for less-than comparison
Informal description
For the comparison result `lt` (less than), the function `isGE` returns `false`.
Ordering.isGT_lt theorem
: lt.isGT = false
Full source 
@[simp]
theorem isGT_lt : lt.isGT = false := rfl
`isGT` returns false for less-than comparison
Informal description
For the comparison result `lt` (less than), the function `isGT` returns `false`.
Ordering.isLT_eq theorem
: eq.isLT = false
Full source 
@[simp]
theorem isLT_eq : eq.isLT = false := rfl
`isLT` returns false for equal comparison
Informal description
The function `isLT` applied to the ordering result `Ordering.eq` returns `false`.
Ordering.isLE_eq theorem
: eq.isLE
Full source 
@[simp]
theorem isLE_eq : eq.isLE := rfl
`isLE` Returns True for Equal Comparison
Informal description
The function `isLE` applied to the ordering result `Ordering.eq` returns `true`.
Ordering.isEq_eq theorem
: eq.isEq
Full source 
@[simp]
theorem isEq_eq : eq.isEq := rfl
Equality Check for `Ordering.eq` Returns True
Informal description
The function `isEq` applied to the ordering result `Ordering.eq` returns `true`.
Ordering.isNe_eq theorem
: eq.isNe = false
Full source 
@[simp]
theorem isNe_eq : eq.isNe = false := rfl
`isNe` returns false for equality comparison
Informal description
For the ordering result `Ordering.eq`, the function `isNe` returns `false`.
Ordering.isGE_eq theorem
: eq.isGE
Full source 
@[simp]
theorem isGE_eq : eq.isGE := rfl
`isGE` returns true for equality comparison
Informal description
For the equality comparison result `Ordering.eq`, the function `isGE` returns `true`.
Ordering.isGT_eq theorem
: eq.isGT = false
Full source 
@[simp]
theorem isGT_eq : eq.isGT = false := rfl
`isGT` returns false for equality comparison
Informal description
For the equality comparison result `Ordering.eq`, the function `isGT` returns `false`.
Ordering.isLT_gt theorem
: gt.isLT = false
Full source 
@[simp]
theorem isLT_gt : gt.isLT = false := rfl
`isLT` returns false for greater-than comparison
Informal description
For the comparison result `Ordering.gt`, the function `isLT` returns `false`.
Ordering.isLE_gt theorem
: gt.isLE = false
Full source 
@[simp]
theorem isLE_gt : gt.isLE = false := rfl
`isLE` returns false for greater-than comparison
Informal description
For the comparison result `Ordering.gt`, the function `isLE` returns `false`.
Ordering.isEq_gt theorem
: gt.isEq = false
Full source 
@[simp]
theorem isEq_gt : gt.isEq = false := rfl
Equality Check for Greater-Than Ordering is False
Informal description
For the greater-than ordering result `gt`, the function `isEq` evaluates to `false`.
Ordering.isNe_gt theorem
: gt.isNe = true
Full source 
@[simp]
theorem isNe_gt : gt.isNe = true := rfl
Inequality Check for Greater-Than Ordering
Informal description
For the greater-than ordering result `gt`, the function `isNe` evaluates to `true`.
Ordering.isGE_gt theorem
: gt.isGE
Full source 
@[simp]
theorem isGE_gt : gt.isGE := rfl
Greater-Than Ordering Satisfies Greater-or-Equal Condition
Informal description
For the greater-than ordering result `gt`, the function `isGE` evaluates to `true`.
Ordering.isGT_gt theorem
: gt.isGT
Full source 
@[simp]
theorem isGT_gt : gt.isGT := rfl
Greater-Than Ordering Satisfies Greater-Than Condition
Informal description
For the greater-than ordering result `gt`, the function `isGT` evaluates to `true`.
Ordering.swap_lt theorem
: lt.swap = .gt
Full source 
@[simp]
theorem swap_lt : lt.swap = .gt := rfl
Swap of Less-Than Yields Greater-Than
Informal description
The swap of the `lt` (less-than) ordering result equals `gt` (greater-than), i.e., $\mathrm{swap}(\mathrm{lt}) = \mathrm{gt}$.
Ordering.swap_eq theorem
: eq.swap = .eq
Full source 
@[simp]
theorem swap_eq : eq.swap = .eq := rfl
Swap Preserves Equality Ordering
Informal description
The swap of the equality ordering result `eq` is itself, i.e., $\mathrm{swap}(\mathrm{eq}) = \mathrm{eq}$.
Ordering.swap_gt theorem
: gt.swap = .lt
Full source 
@[simp]
theorem swap_gt : gt.swap = .lt := rfl
Swap of Greater-Than Yields Less-Than
Informal description
The swap of the `gt` (greater-than) ordering result equals `lt` (less-than), i.e., $\mathrm{swap}(\mathrm{gt}) = \mathrm{lt}$.
Ordering.isLE_eq_false theorem
{o : Ordering} : o.isLE = false ↔ o = .gt
Full source 
@[simp]
theorem isLE_eq_false {o : Ordering} : o.isLE = false ↔ o = .gt := by
  cases o <;> simp
$\text{isLE}(o) = \text{false} \leftrightarrow o = \text{gt}$
Informal description
For any comparison result `o` of type `Ordering`, the function `isLE` returns `false` if and only if `o` is `Ordering.gt`. In other words, $\text{isLE}(o) = \text{false} \leftrightarrow o = \text{Ordering.gt}$.
Ordering.isGE_eq_false theorem
{o : Ordering} : o.isGE = false ↔ o = .lt
Full source 
@[simp]
theorem isGE_eq_false {o : Ordering} : o.isGE = false ↔ o = .lt := by
  cases o <;> simp
Characterization of `isGE` False Condition: $o.\text{isGE} = \text{false} \leftrightarrow o = \text{lt}$
Informal description
For any comparison result `o` of type `Ordering`, the predicate `isGE` evaluates to `false` if and only if `o` is the `Ordering.lt` constructor (indicating "less than").
Ordering.swap_eq_gt theorem
{o : Ordering} : o.swap = .gt ↔ o = .lt
Full source 
@[simp]
theorem swap_eq_gt {o : Ordering} : o.swap = .gt ↔ o = .lt := by
  cases o <;> simp
Swap of Ordering Equals Greater-Than if and Only if Original Equals Less-Than
Informal description
For any ordering result $o$, the swap of $o$ equals `gt` if and only if $o$ equals `lt$.
Ordering.swap_eq_lt theorem
{o : Ordering} : o.swap = .lt ↔ o = .gt
Full source 
@[simp]
theorem swap_eq_lt {o : Ordering} : o.swap = .lt ↔ o = .gt := by
  cases o <;> simp
Swap of Ordering Results: $o.\mathrm{swap} = \mathrm{lt} \leftrightarrow o = \mathrm{gt}$
Informal description
For any comparison result $o$ of type `Ordering`, the swapped ordering $o.\mathrm{swap}$ equals `lt` if and only if $o$ equals `gt$.
Ordering.swap_eq_eq theorem
{o : Ordering} : o.swap = .eq ↔ o = .eq
Full source 
@[simp]
theorem swap_eq_eq {o : Ordering} : o.swap = .eq ↔ o = .eq := by
  cases o <;> simp
Equivalence of Swapped Ordering Equality: $o.\mathrm{swap} = \mathrm{eq} \leftrightarrow o = \mathrm{eq}$
Informal description
For any comparison result $o$ of type `Ordering`, the swapped ordering $o.\mathrm{swap}$ is equal to `.eq` if and only if $o$ is equal to `.eq$.
Ordering.isLT_swap theorem
{o : Ordering} : o.swap.isLT = o.isGT
Full source 
@[simp]
theorem isLT_swap {o : Ordering} : o.swap.isLT = o.isGT := by
  cases o <;> simp
Swapped Ordering Preserves Less-Than/Greater-Than Relation: $o.\mathrm{swap}.\mathrm{isLT} = o.\mathrm{isGT}$
Informal description
For any comparison result $o$ of type `Ordering`, the result of checking if the swapped ordering $o.\mathrm{swap}$ is less than is equal to checking if $o$ is greater than, i.e., $o.\mathrm{swap}.\mathrm{isLT} = o.\mathrm{isGT}$.
Ordering.isLE_swap theorem
{o : Ordering} : o.swap.isLE = o.isGE
Full source 
@[simp]
theorem isLE_swap {o : Ordering} : o.swap.isLE = o.isGE := by
  cases o <;> simp
Swapped Ordering Preserves Inequality Relation: $o.\mathrm{swap}.\mathrm{isLE} = o.\mathrm{isGE}$
Informal description
For any comparison result $o$ of type `Ordering`, the result of checking if the swapped ordering $o.\mathrm{swap}$ is less than or equal to is equal to checking if $o$ is greater than or equal to, i.e., $o.\mathrm{swap}.\mathrm{isLE} = o.\mathrm{isGE}$.
Ordering.isEq_swap theorem
{o : Ordering} : o.swap.isEq = o.isEq
Full source 
@[simp]
theorem isEq_swap {o : Ordering} : o.swap.isEq = o.isEq := by
  cases o <;> simp
Swapped Ordering Preserves Equality Check: $o.\mathrm{swap}.\mathrm{isEq} = o.\mathrm{isEq}$
Informal description
For any comparison result $o$ of type `Ordering`, the result of checking if the swapped ordering $o.\mathrm{swap}$ is equal is the same as checking if $o$ is equal, i.e., $o.\mathrm{swap}.\mathrm{isEq} = o.\mathrm{isEq}$.
Ordering.isNe_swap theorem
{o : Ordering} : o.swap.isNe = o.isNe
Full source 
@[simp]
theorem isNe_swap {o : Ordering} : o.swap.isNe = o.isNe := by
  cases o <;> simp
Swapped Ordering Preserves Inequality Check: $o.\mathrm{swap}.\mathrm{isNe} = o.\mathrm{isNe}$
Informal description
For any comparison result $o$ of type `Ordering`, the result of checking if the swapped ordering $o.\mathrm{swap}$ is not equal is the same as checking if $o$ is not equal, i.e., $o.\mathrm{swap}.\mathrm{isNe} = o.\mathrm{isNe}$.
Ordering.isGE_swap theorem
{o : Ordering} : o.swap.isGE = o.isLE
Full source 
@[simp]
theorem isGE_swap {o : Ordering} : o.swap.isGE = o.isLE := by
  cases o <;> simp
Swapped Ordering Preserves Less-Than-or-Equal Check: $o.\mathrm{swap}.\mathrm{isGE} = o.\mathrm{isLE}$
Informal description
For any comparison result $o$ of type `Ordering`, the result of checking if the swapped ordering $o.\mathrm{swap}$ is greater than or equal to is equal to checking if $o$ is less than or equal to, i.e., $o.\mathrm{swap}.\mathrm{isGE} = o.\mathrm{isLE}$.
Ordering.isGT_swap theorem
{o : Ordering} : o.swap.isGT = o.isLT
Full source 
@[simp]
theorem isGT_swap {o : Ordering} : o.swap.isGT = o.isLT := by
  cases o <;> simp
Swapped Ordering Preserves Less-Than Check: $o.\mathrm{swap}.\mathrm{isGT} = o.\mathrm{isLT}$
Informal description
For any comparison result $o$ of type `Ordering`, the result of checking if the swapped ordering $o.\mathrm{swap}$ is greater than is equal to checking if $o$ is less than, i.e., $o.\mathrm{swap}.\mathrm{isGT} = o.\mathrm{isLT}$.
Ordering.isLT_iff_eq_lt theorem
{o : Ordering} : o.isLT ↔ o = .lt
Full source 
theorem isLT_iff_eq_lt {o : Ordering} : o.isLT ↔ o = .lt := by
  cases o <;> simp
Characterization of Less-Than Check in Ordering: $o.\mathrm{isLT} \leftrightarrow o = \mathrm{lt}$
Informal description
For any comparison result $o$ of type `Ordering`, the function `isLT` applied to $o$ returns `true` if and only if $o$ is equal to `Ordering.lt`.
Ordering.isLE_iff_eq_lt_or_eq_eq theorem
{o : Ordering} : o.isLE ↔ o = .lt ∨ o = .eq
Full source 
theorem isLE_iff_eq_lt_or_eq_eq {o : Ordering} : o.isLE ↔ o = .lt ∨ o = .eq := by
  cases o <;> simp
Characterization of Less-Than-or-Equal Comparison: $o.\mathrm{isLE} \leftrightarrow o = \mathrm{lt} \lor o = \mathrm{eq}$
Informal description
For any comparison result $o$ of type `Ordering`, the function `isLE` applied to $o$ returns `true` if and only if $o$ is equal to `Ordering.lt` or `Ordering.eq`.
Ordering.isLE_of_eq_lt theorem
{o : Ordering} : o = .lt → o.isLE
Full source 
theorem isLE_of_eq_lt {o : Ordering} : o = .lt → o.isLE := by
  rintro rfl; rfl
Less-than comparison implies less-than-or-equal result
Informal description
For any comparison result $o$ of type `Ordering`, if $o$ is equal to `Ordering.lt`, then the function `isLE` applied to $o$ returns `true`.
Ordering.isLE_of_eq_eq theorem
{o : Ordering} : o = .eq → o.isLE
Full source 
theorem isLE_of_eq_eq {o : Ordering} : o = .eq → o.isLE := by
  rintro rfl; rfl
Equality comparison implies less-than-or-equal result
Informal description
For any comparison result $o$ of type `Ordering`, if $o$ is equal to `Ordering.eq`, then the function `isLE` applied to $o$ returns `true`.
Ordering.isEq_iff_eq_eq theorem
{o : Ordering} : o.isEq ↔ o = .eq
Full source 
theorem isEq_iff_eq_eq {o : Ordering} : o.isEq ↔ o = .eq := by
  cases o <;> simp
Characterization of Equality Check in Ordering: $o.\text{isEq} \leftrightarrow o = \text{eq}$
Informal description
For any comparison result $o$ of type `Ordering`, the function `isEq` returns `true` if and only if $o$ is equal to `Ordering.eq`.
Ordering.isNe_iff_ne_eq theorem
{o : Ordering} : o.isNe ↔ o ≠ .eq
Full source 
theorem isNe_iff_ne_eq {o : Ordering} : o.isNe ↔ o ≠ .eq := by
  cases o <;> simp
Inequality Check in Comparison Results: $o.\text{isNe} \leftrightarrow o \neq \text{eq}$
Informal description
For any comparison result $o$ of type `Ordering`, the function `isNe` returns `true` if and only if $o$ is not equal to `Ordering.eq`.
Ordering.isGE_iff_eq_gt_or_eq_eq theorem
{o : Ordering} : o.isGE ↔ o = .gt ∨ o = .eq
Full source 
theorem isGE_iff_eq_gt_or_eq_eq {o : Ordering} : o.isGE ↔ o = .gt ∨ o = .eq := by
  cases o <;> simp
Characterization of Greater-Than-Or-Equal in Comparison Results: $o.\text{isGE} \leftrightarrow o = \text{gt} \lor o = \text{eq}$
Informal description
For any comparison result $o$ of type `Ordering`, the function `isGE` applied to $o$ returns `true` if and only if $o$ is equal to `Ordering.gt` or `Ordering.eq`.
Ordering.isGE_of_eq_gt theorem
{o : Ordering} : o = .gt → o.isGE
Full source 
theorem isGE_of_eq_gt {o : Ordering} : o = .gt → o.isGE := by
  rintro rfl; rfl
Greater-than implies greater-than-or-equal in comparison results
Informal description
For any comparison result $o$ of type `Ordering`, if $o$ is equal to `Ordering.gt`, then the function `isGE` applied to $o$ returns `true`.
Ordering.isGE_of_eq_eq theorem
{o : Ordering} : o = .eq → o.isGE
Full source 
theorem isGE_of_eq_eq {o : Ordering} : o = .eq → o.isGE := by
  rintro rfl; rfl
Equality implies greater-than-or-equal in comparison results
Informal description
For any comparison result $o$ of type `Ordering`, if $o$ is equal to `Ordering.eq`, then the function `isGE` applied to $o$ returns `true`.
Ordering.isGT_iff_eq_gt theorem
{o : Ordering} : o.isGT ↔ o = .gt
Full source 
theorem isGT_iff_eq_gt {o : Ordering} : o.isGT ↔ o = .gt := by
  cases o <;> simp
Characterization of Greater-Than Ordering: $o.\text{isGT} \leftrightarrow o = \text{gt}$
Informal description
For any comparison result $o$ of type `Ordering`, the predicate `isGT` applied to $o$ holds if and only if $o$ is equal to `Ordering.gt`.
Ordering.swap_swap theorem
{o : Ordering} : o.swap.swap = o
Full source 
@[simp]
theorem swap_swap {o : Ordering} : o.swap.swap = o := by
  cases o <;> simp
Double Swap of Ordering is Identity
Informal description
For any ordering comparison result $o$, swapping it twice returns the original result, i.e., $\mathrm{swap}(\mathrm{swap}(o)) = o$.
Ordering.swap_inj theorem
{o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂
Full source 
@[simp] theorem swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂ :=
  ⟨fun h => by simpa using congrArg swap h, congrArg _⟩
Swap of Ordering Results is Injective: $o_1.\text{swap} = o_2.\text{swap} \leftrightarrow o_1 = o_2$
Informal description
For any two ordering comparison results $o_1$ and $o_2$, the swap of $o_1$ equals the swap of $o_2$ if and only if $o_1$ equals $o_2$.
Ordering.swap_then theorem
(o₁ o₂ : Ordering) : (o₁.then o₂).swap = o₁.swap.then o₂.swap
Full source 
theorem swap_then (o₁ o₂ : Ordering) : (o₁.then o₂).swap = o₁.swap.then o₂.swap := by
  cases o₁ <;> rfl
Swap Commutes with Lexicographic Combination of Orderings
Informal description
For any two comparison results $o_1$ and $o_2$ of type `Ordering`, swapping the lexicographic combination of $o_1$ and $o_2$ is equal to the lexicographic combination of the swapped $o_1$ and the swapped $o_2$. In other words, $(o_1 \text{ then } o_2).\text{swap} = o_1.\text{swap} \text{ then } o_2.\text{swap}$.
Ordering.then_eq_lt theorem
{o₁ o₂ : Ordering} : o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt
Full source 
theorem then_eq_lt {o₁ o₂ : Ordering} : o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt := by
  cases o₁ <;> cases o₂ <;> decide
Lexicographic Combination Equals Less-Than Condition: $o_1 \text{ then } o_2 = \text{lt} \leftrightarrow o_1 = \text{lt} \lor (o_1 = \text{eq} \land o_2 = \text{lt})$
Informal description
For any two comparison results $o_1$ and $o_2$ of type `Ordering`, the lexicographic combination $o_1 \text{ then } o_2$ equals `lt` if and only if either $o_1$ equals `lt`, or $o_1$ equals `eq` and $o_2$ equals `lt`.
Ordering.then_eq_eq theorem
{o₁ o₂ : Ordering} : o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq
Full source 
theorem then_eq_eq {o₁ o₂ : Ordering} : o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq := by
  cases o₁ <;> simp [«then»]
Lexicographic Combination Equals Equality Condition: $o_1 \text{ then } o_2 = \text{eq} \leftrightarrow o_1 = \text{eq} \land o_2 = \text{eq}$
Informal description
For any two comparison results $o_1$ and $o_2$ of type `Ordering`, the lexicographic combination $o_1 \text{ then } o_2$ equals `eq` if and only if both $o_1$ and $o_2$ equal `eq$.
Ordering.then_eq_gt theorem
{o₁ o₂ : Ordering} : o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt
Full source 
theorem then_eq_gt {o₁ o₂ : Ordering} : o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt := by
  cases o₁ <;> cases o₂ <;> decide
Lexicographic Combination Yields Greater-Than: $o_1.\text{then}\ o_2 = \text{gt} \leftrightarrow o_1 = \text{gt} \lor (o_1 = \text{eq} \land o_2 = \text{gt})$
Informal description
For any two comparison results $o_1$ and $o_2$ of type `Ordering`, the lexicographic combination $o_1.\text{then}\ o_2$ equals `gt` if and only if either $o_1$ is `gt`, or $o_1$ is `eq` and $o_2$ is `gt$.
Ordering.lt_then theorem
{o : Ordering} : lt.then o = lt
Full source 
@[simp]
theorem lt_then {o : Ordering} : lt.then o = lt := rfl
Lexicographic Combination Preserves Less-Than Comparison
Informal description
For any comparison result $o$ of type `Ordering`, the lexicographic combination `lt.then o` is equal to `lt`.
Ordering.gt_then theorem
{o : Ordering} : gt.then o = gt
Full source 
@[simp]
theorem gt_then {o : Ordering} : gt.then o = gt := rfl
Lexicographic Combination Preserves Greater-Than Comparison
Informal description
For any comparison result $o$ of type `Ordering`, the lexicographic combination `gt.then o` is equal to `gt`.
Ordering.isLE_then_iff_or theorem
{o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁ = lt ∨ (o₁ = eq ∧ o₂.isLE)
Full source 
theorem isLE_then_iff_or {o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁ = lt ∨ (o₁ = eq ∧ o₂.isLE) := by
  cases o₁ <;> simp
Lexicographic Combination is Less-Than-Or-Equal if and only if Left is Less or (Equal and Right is Less-Than-Or-Equal)
Informal description
For any comparison results $o_1$ and $o_2$ of type `Ordering`, the lexicographic combination $o_1.\text{then}\ o_2$ is less than or equal (i.e., `(o₁.then o₂).isLE` holds) if and only if either $o_1$ is strictly less than (`Ordering.lt`), or $o_1$ is equal (`Ordering.eq`) and $o_2$ is less than or equal (`o₂.isLE` holds).
Ordering.isLE_then_iff_and theorem
{o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁.isLE ∧ (o₁ = lt ∨ o₂.isLE)
Full source 
theorem isLE_then_iff_and {o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁.isLE ∧ (o₁ = lt ∨ o₂.isLE) := by
  cases o₁ <;> simp
Lexicographic Comparison Condition for Less-Than-Or-Equal: $(o_1.\text{then}\ o_2).\text{isLE} \leftrightarrow o_1.\text{isLE} \land (o_1 = \text{lt} \lor o_2.\text{isLE})$
Informal description
For any comparison results $o_1$ and $o_2$ of type `Ordering`, the lexicographic combination $o_1.\text{then}\ o_2$ is less than or equal (i.e., `(o₁.then o₂).isLE` holds) if and only if both: 1. $o_1$ is less than or equal (i.e., `o₁.isLE` holds), and 2. either $o_1$ is strictly less than (i.e., `o₁ = lt`) or $o_2$ is less than or equal (i.e., `o₂.isLE` holds).
Ordering.isLE_left_of_isLE_then theorem
{o₁ o₂ : Ordering} (h : (o₁.then o₂).isLE) : o₁.isLE
Full source 
theorem isLE_left_of_isLE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isLE) : o₁.isLE := by
  cases o₁ <;> simp_all
Lexicographic Comparison Preserves Less-Than-Or-Equal on Left Component
Informal description
For any comparison results $o_1$ and $o_2$ of type `Ordering`, if the lexicographic combination $o_1.\text{then}\ o_2$ is less than or equal (i.e., `(o₁.then o₂).isLE` holds), then $o_1$ itself must be less than or equal (i.e., `o₁.isLE` holds).
Ordering.isGE_left_of_isGE_then theorem
{o₁ o₂ : Ordering} (h : (o₁.then o₂).isGE) : o₁.isGE
Full source 
theorem isGE_left_of_isGE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isGE) : o₁.isGE := by
  cases o₁ <;> simp_all
Lexicographic Comparison Preserves Greater-Than-Or-Equal on Left Component
Informal description
For any comparison results $o_1$ and $o_2$ of type `Ordering`, if the lexicographic combination $o_1.\text{then}\ o_2$ is greater than or equal (i.e., `(o₁.then o₂).isGE` holds), then $o_1$ itself must be greater than or equal (i.e., `o₁.isGE` holds).
compareOfLessAndEq definition
{α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering
Full source 
/--
Uses decidable less-than and equality relations to find an `Ordering`.

In particular, if `x < y` then the result is `Ordering.lt`. If `x = y` then the result is
`Ordering.eq`. Otherwise, it is `Ordering.gt`.

`compareOfLessAndBEq` uses `BEq` instead of `DecidableEq`.
-/
@[inline] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
  if x < y then Ordering.lt
  else if x = y then Ordering.eq
  else Ordering.gt
Comparison of elements using decidable less-than and equality
Informal description
Given a type $\alpha$ with a decidable less-than relation `[LT α]` and decidable equality `[DecidableEq α]`, the function `compareOfLessAndEq` compares two elements $x, y \in \alpha$ and returns an `Ordering` result: - `Ordering.lt` if $x < y$, - `Ordering.eq` if $x = y$, - `Ordering.gt` otherwise. This function uses the decidable instances to determine the ordering between $x$ and $y$.
compareOfLessAndBEq definition
{α} (x y : α) [LT α] [Decidable (x < y)] [BEq α] : Ordering
Full source 
/--
Uses a decidable less-than relation and Boolean equality to find an `Ordering`.

In particular, if `x < y` then the result is `Ordering.lt`. If `x == y` then the result is
`Ordering.eq`. Otherwise, it is `Ordering.gt`.

`compareOfLessAndEq` uses `DecidableEq` instead of `BEq`.
-/
@[inline] def compareOfLessAndBEq {α} (x y : α) [LT α] [Decidable (x < y)] [BEq α] : Ordering :=
  if x < y then .lt
  else if x == y then .eq
  else .gt
Comparison using decidable less-than and boolean equality
Informal description
Given a type $\alpha$ with a decidable less-than relation `[LT α]` and boolean equality `[BEq α]`, the function `compareOfLessAndBEq` compares two elements $x, y \in \alpha$ and returns an `Ordering` result: - `\text{Ordering.lt}` if $x < y$, - `\text{Ordering.eq}` if $x$ and $y$ are equal according to the boolean equality `==`, - `\text{Ordering.gt}` otherwise.
compareLex definition
(cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) : Ordering
Full source 
/--
Compares `a` and `b` lexicographically by `cmp₁` and `cmp₂`.

`a` and `b` are first compared by `cmp₁`. If this returns `Ordering.eq`, `a` and `b` are compared
by `cmp₂` to break the tie.

To lexicographically combine two `Ordering`s, use `Ordering.then`.
-/
@[inline] def compareLex (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) : Ordering :=
  (cmp₁ a b).then (cmp₂ a b)
Lexicographic comparison of two elements using two comparison functions
Informal description
Given two comparison functions `cmp₁` and `cmp₂` from types `α` and `β` to `Ordering`, and elements `a : α` and `b : β`, the function `compareLex cmp₁ cmp₂ a b` first compares `a` and `b` using `cmp₁`. If the result is `Ordering.eq`, it then compares `a` and `b` using `cmp₂` to break the tie. Otherwise, it returns the result of `cmp₁`.
compareLex_eq_eq theorem
{α} {cmp₁ cmp₂} {a b : α} : compareLex cmp₁ cmp₂ a b = .eq ↔ cmp₁ a b = .eq ∧ cmp₂ a b = .eq
Full source 
@[simp]
theorem compareLex_eq_eq {α} {cmp₁ cmp₂} {a b : α} :
    compareLexcompareLex cmp₁ cmp₂ a b = .eq ↔ cmp₁ a b = .eq ∧ cmp₂ a b = .eq := by
  simp [compareLex, Ordering.then_eq_eq]
Lexicographic Comparison Yields Equality if and only if Both Comparisons Yield Equality
Informal description
For any type $\alpha$ with comparison functions `cmp₁` and `cmp₂` from $\alpha$ to `Ordering`, and elements $a, b \in \alpha$, the lexicographic comparison `compareLex cmp₁ cmp₂ a b` yields `Ordering.eq` if and only if both `cmp₁ a b` and `cmp₂ a b` yield `Ordering.eq`.
compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne theorem
{α : Type u} [LT α] [DecidableLT α] [DecidableEq α] (h : ∀ x y : α, x < y ↔ ¬y < x ∧ x ≠ y) {x y : α} : compareOfLessAndEq x y = (compareOfLessAndEq y x).swap
Full source 
theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne {α : Type u} [LT α] [DecidableLT α] [DecidableEq α]
    (h : ∀ x y : α, x < y ↔ ¬ y < x ∧ x ≠ y) {x y : α} :
    compareOfLessAndEq x y = (compareOfLessAndEq y x).swap := by
  simp only [compareOfLessAndEq]
  split
  · rename_i h'
    rw [h] at h'
    simp only [h'.1, h'.2.symm, reduceIte, Ordering.swap_gt]
  · split
    · rename_i h'
      have : ¬ y < y := Not.imp (·.2 rfl) <| (h y y).mp
      simp only [h', this, reduceIte, Ordering.swap_eq]
    · rename_i h' h''
      replace h' := (h y x).mpr ⟨h', Ne.symm h''⟩
      simp only [h', Ne.symm h'', reduceIte, Ordering.swap_lt]
Comparison Result Swap Under Symmetric Strict Order Condition: $\text{compareOfLessAndEq}(x, y) = \text{swap}(\text{compareOfLessAndEq}(y, x))$ when $x < y \leftrightarrow \neg(y < x) \land x \neq y$
Informal description
Let $\alpha$ be a type with a decidable less-than relation $<$ and decidable equality. Suppose that for any $x, y \in \alpha$, the relation $x < y$ holds if and only if both $\neg (y < x)$ and $x \neq y$ hold. Then, for any $x, y \in \alpha$, the comparison result $\text{compareOfLessAndEq}(x, y)$ is equal to the swap of $\text{compareOfLessAndEq}(y, x)$.
lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le theorem
{α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) (x y : α) : x < y ↔ ¬y < x ∧ x ≠ y
Full source 
theorem lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le
    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
    (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y¬ x ≤ y ↔ y < x) (x y : α) :
    x < y ↔ ¬ y < x ∧ x ≠ y := by
  simp only [← not_le, Classical.not_not]
  constructor
  · intro h
    have refl := by cases total y y <;> assumption
    exact ⟨(total _ _).resolve_left h, fun h' => (h' ▸ h) refl⟩
  · intro ⟨h₁, h₂⟩ h₃
    exact h₂ (antisymm h₁ h₃)
Characterization of Strict Order via Antisymmetry, Totality, and Negation of $\leq$
Informal description
Let $\alpha$ be a type equipped with a less-than relation $<$ and a less-than-or-equal relation $\leq$, both of which are decidable. Assume the following properties hold: 1. **Antisymmetry**: For any $x, y \in \alpha$, if $x \leq y$ and $y \leq x$, then $x = y$. 2. **Totality**: For any $x, y \in \alpha$, either $x \leq y$ or $y \leq x$ holds. 3. **Negation of $\leq$**: For any $x, y \in \alpha$, $\neg (x \leq y)$ is equivalent to $y < x$. Then, for any $x, y \in \alpha$, the relation $x < y$ holds if and only if both $\neg (y < x)$ and $x \neq y$ hold.
compareOfLessAndEq_eq_swap theorem
{α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) {x y : α} : compareOfLessAndEq x y = (compareOfLessAndEq y x).swap
Full source 
theorem compareOfLessAndEq_eq_swap
    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
    (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y¬ x ≤ y ↔ y < x) {x y : α} :
    compareOfLessAndEq x y = (compareOfLessAndEq y x).swap := by
  apply compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne
  exact lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le antisymm total not_le
Comparison Result Swap in Total Order with Antisymmetry and Negation Condition
Informal description
Let $\alpha$ be a type equipped with decidable less-than ($<$) and equality relations, and a less-than-or-equal relation ($\leq$). Suppose the following properties hold: 1. **Antisymmetry**: For any $x, y \in \alpha$, if $x \leq y$ and $y \leq x$, then $x = y$. 2. **Totality**: For any $x, y \in \alpha$, either $x \leq y$ or $y \leq x$ holds. 3. **Negation of $\leq$**: For any $x, y \in \alpha$, $\neg (x \leq y)$ is equivalent to $y < x$. Then, for any $x, y \in \alpha$, the comparison result $\text{compareOfLessAndEq}(x, y)$ is equal to the swap of $\text{compareOfLessAndEq}(y, x)$.
compareOfLessAndEq_eq_lt theorem
{α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α} : compareOfLessAndEq x y = .lt ↔ x < y
Full source 
@[simp]
theorem compareOfLessAndEq_eq_lt
    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α} :
    compareOfLessAndEqcompareOfLessAndEq x y = .lt ↔ x < y := by
  rw [compareOfLessAndEq]
  repeat' split <;> simp_all
Comparison Result Equals Less-Than if and only if $x < y$
Informal description
For any type $\alpha$ with decidable less-than ($<$) and equality relations, and for any elements $x, y \in \alpha$, the comparison result $\text{compareOfLessAndEq}(x, y)$ is equal to $\text{Ordering.lt}$ if and only if $x < y$.
compareOfLessAndEq_eq_eq theorem
{α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α] (refl : ∀ (x : α), x ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) {x y : α} : compareOfLessAndEq x y = .eq ↔ x = y
Full source 
theorem compareOfLessAndEq_eq_eq
    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α]
    (refl : ∀ (x : α), x ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y¬ x ≤ y ↔ y < x) {x y : α} :
    compareOfLessAndEqcompareOfLessAndEq x y = .eq ↔ x = y := by
  rw [compareOfLessAndEq]
  repeat' split <;> try (simp_all; done)
  simp only [reduceCtorEq, false_iff]
  rintro rfl
  rename_i hlt
  simp [← not_le] at hlt
  exact hlt (refl x)
Equivalence of Comparison Equality with Element Equality in Decidable Order
Informal description
Let $\alpha$ be a type equipped with decidable less-than ($<$), less-than-or-equal ($\leq$), and equality relations. Suppose the following properties hold: 1. **Reflexivity of $\leq$**: For any $x \in \alpha$, $x \leq x$. 2. **Negation of $\leq$**: For any $x, y \in \alpha$, $\neg (x \leq y)$ is equivalent to $y < x$. Then, for any $x, y \in \alpha$, the comparison result $\text{compareOfLessAndEq}(x, y)$ equals $\text{Ordering.eq}$ if and only if $x = y$.
compareOfLessAndEq_eq_gt_of_lt_iff_not_gt_and_ne theorem
{α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α} (h : ∀ x y : α, x < y ↔ ¬y < x ∧ x ≠ y) : compareOfLessAndEq x y = .gt ↔ y < x
Full source 
theorem compareOfLessAndEq_eq_gt_of_lt_iff_not_gt_and_ne
    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α}
    (h : ∀ x y : α, x < y ↔ ¬ y < x ∧ x ≠ y) :
    compareOfLessAndEqcompareOfLessAndEq x y = .gt ↔ y < x := by
  rw [compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne h, Ordering.swap_eq_gt]
  exact compareOfLessAndEq_eq_lt
Comparison Result Equals Greater-Than Under Symmetric Strict Order Condition: $\text{compareOfLessAndEq}(x, y) = \text{gt} \leftrightarrow y < x$
Informal description
Let $\alpha$ be a type with decidable less-than ($<$) and equality relations, and let $x, y \in \alpha$. Suppose that for any $x, y \in \alpha$, the relation $x < y$ holds if and only if both $\neg (y < x)$ and $x \neq y$ hold. Then, the comparison result $\text{compareOfLessAndEq}(x, y)$ equals $\text{Ordering.gt}$ if and only if $y < x$.
compareOfLessAndEq_eq_gt theorem
{α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) (x y : α) : compareOfLessAndEq x y = .gt ↔ y < x
Full source 
theorem compareOfLessAndEq_eq_gt
    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
    (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y¬ x ≤ y ↔ y < x) (x y : α) :
    compareOfLessAndEqcompareOfLessAndEq x y = .gt ↔ y < x := by
  apply compareOfLessAndEq_eq_gt_of_lt_iff_not_gt_and_ne
  exact lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le antisymm total not_le
Characterization of Greater-Than Comparison in Decidable Total Orders: $\text{compareOfLessAndEq}(x, y) = \text{gt} \leftrightarrow y < x$
Informal description
Let $\alpha$ be a type equipped with decidable less-than ($<$) and equality relations, and let $x, y \in \alpha$. Suppose the following properties hold: 1. **Antisymmetry**: For any $x, y \in \alpha$, if $x \leq y$ and $y \leq x$, then $x = y$. 2. **Totality**: For any $x, y \in \alpha$, either $x \leq y$ or $y \leq x$ holds. 3. **Negation of $\leq$**: For any $x, y \in \alpha$, $\neg (x \leq y)$ is equivalent to $y < x$. Then, the comparison result $\text{compareOfLessAndEq}(x, y)$ equals $\text{Ordering.gt}$ if and only if $y < x$.
isLE_compareOfLessAndEq theorem
{α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) {x y : α} : (compareOfLessAndEq x y).isLE ↔ x ≤ y
Full source 
theorem isLE_compareOfLessAndEq
    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α]
    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
    (not_le : ∀ {x y : α}, ¬ x ≤ y¬ x ≤ y ↔ y < x) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) {x y : α} :
    (compareOfLessAndEq x y).isLE ↔ x ≤ y := by
  have refl (a : α) := by cases total a a <;> assumption
  rw [Ordering.isLE_iff_eq_lt_or_eq_eq, compareOfLessAndEq_eq_lt,
    compareOfLessAndEq_eq_eq refl not_le]
  constructor
  · rintro (h | rfl)
    · rw [← not_le] at h
      exact total _ _ |>.resolve_left h
    · exact refl x
  · intro hle
    by_cases hge : x ≥ y
    · exact Or.inr <| antisymm hle hge
    · exact Or.inl <| not_le.mp hge
Characterization of $\text{isLE}$ for $\text{compareOfLessAndEq}$ in Decidable Total Orders
Informal description
Let $\alpha$ be a type equipped with decidable less-than ($<$), less-than-or-equal ($\leq$), and equality relations, satisfying the following properties: 1. **Antisymmetry**: For any $x, y \in \alpha$, if $x \leq y$ and $y \leq x$, then $x = y$. 2. **Negation of $\leq$**: For any $x, y \in \alpha$, $\neg (x \leq y)$ is equivalent to $y < x$. 3. **Totality**: For any $x, y \in \alpha$, either $x \leq y$ or $y \leq x$ holds. Then, for any $x, y \in \alpha$, the comparison result $\text{compareOfLessAndEq}(x, y)$ has its $\text{isLE}$ flag set to true if and only if $x \leq y$.
Ord structure
(α : Type u)
Full source 
/--
`Ord α` provides a computable total order on `α`, in terms of the
`compare : α → α → Ordering` function.

Typically instances will be transitive, reflexive, and antisymmetric,
but this is not enforced by the typeclass.

There is a derive handler, so appending `deriving Ord` to an inductive type or structure
will attempt to create an `Ord` instance.
-/
class Ord (α : Type u) where
  /-- Compare two elements in `α` using the comparator contained in an `[Ord α]` instance. -/
  compare : α → α → Ordering
Computable Total Order Structure
Informal description
The structure `Ord α` provides a computable total order on a type `α` via a function `compare : α → α → Ordering`. While instances typically satisfy transitivity, reflexivity, and antisymmetry, these properties are not enforced by the typeclass. The `compare` function returns an `Ordering` (either `lt`, `eq`, or `gt`) indicating the relationship between two elements of `α`. Instances of `Ord` can be automatically derived for inductive types or structures using the `deriving Ord` mechanism.
compareOn definition
[ord : Ord β] (f : α → β) (x y : α) : Ordering
Full source 
/--
Compares two values by comparing the results of applying a function.

In particular, `x` is compared to `y` by comparing `f x` and `f y`.

Examples:
 * `compareOn (·.length) "apple" "banana" = .lt`
 * `compareOn (· % 3) 5 6 = .gt`
 * `compareOn (·.foldl max 0) [1, 2, 3] [3, 2, 1] = .eq`
-/
@[inline] def compareOn [ord : Ord β] (f : α → β) (x y : α) : Ordering :=
  compare (f x) (f y)
Comparison via function application
Informal description
Given a function \( f : \alpha \to \beta \) and two elements \( x, y \) of type \( \alpha \), the function `compareOn` compares \( x \) and \( y \) by comparing their images \( f(x) \) and \( f(y) \) under \( f \). The result is an `Ordering` value (`lt`, `eq`, or `gt`) indicating whether \( f(x) \) is less than, equal to, or greater than \( f(y) \).
instOrdNat instance
: Ord Nat
Full source 
instance : Ord Nat where
  compare x y := compareOfLessAndEq x y
The Computable Total Order on Natural Numbers
Informal description
The natural numbers $\mathbb{N}$ have a canonical computable total order structure, where the `compare` function returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the standard ordering of natural numbers.
instOrdInt instance
: Ord Int
Full source 
instance : Ord Int where
  compare x y := compareOfLessAndEq x y
The Computable Total Order on Integers
Informal description
The integers $\mathbb{Z}$ have a canonical computable total order structure, where the `compare` function returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the standard ordering of integers.
instOrdBool instance
: Ord Bool
Full source 
instance : Ord Bool where
  compare
  | false, true => Ordering.lt
  | true, false => Ordering.gt
  | _, _ => Ordering.eq
Canonical Total Order on Boolean Values
Informal description
The Boolean type `Bool` with values `true` and `false` has a canonical computable total order structure, where `false` is considered less than `true`.
instOrdString instance
: Ord String
Full source 
instance : Ord String where
  compare x y := compareOfLessAndEq x y
Lexicographic Order on Strings
Informal description
The type of strings has a canonical computable total order structure, where the `compare` function returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the lexicographic ordering of strings.
instOrdFin instance
(n : Nat) : Ord (Fin n)
Full source 
instance (n : Nat) : Ord (Fin n) where
  compare x y := compare x.val y.val
Canonical Total Order on Finite Types $\mathrm{Fin}\,n$
Informal description
For any natural number $n$, the finite type $\mathrm{Fin}\,n$ of natural numbers less than $n$ has a canonical computable total order structure inherited from the natural numbers.
instOrdUInt8 instance
: Ord UInt8
Full source 
instance : Ord UInt8 where
  compare x y := compareOfLessAndEq x y
Canonical Total Order on Unsigned 8-bit Integers
Informal description
The type of unsigned 8-bit integers $\mathbb{UInt8}$ has a canonical computable total order structure, where the comparison function `compare` returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the ordering of two elements.
instOrdUInt16 instance
: Ord UInt16
Full source 
instance : Ord UInt16 where
  compare x y := compareOfLessAndEq x y
Computable Total Order on 16-bit Unsigned Integers
Informal description
The type of unsigned 16-bit integers has a computable total order structure, where the comparison between two elements is determined using the decidable less-than and equality relations.
instOrdUInt32 instance
: Ord UInt32
Full source 
instance : Ord UInt32 where
  compare x y := compareOfLessAndEq x y
Computable Total Order on 32-bit Unsigned Integers
Informal description
The type of unsigned 32-bit integers is equipped with a computable total order structure, where the comparison function `compare` determines the ordering between two elements by first checking if one is less than the other (using the decidable less-than relation) and then checking for equality (using the decidable equality relation). The result is either `Ordering.lt`, `Ordering.eq`, or `Ordering.gt`.
instOrdUInt64 instance
: Ord UInt64
Full source 
instance : Ord UInt64 where
  compare x y := compareOfLessAndEq x y
Computable Total Order on 64-bit Unsigned Integers
Informal description
The type of unsigned 64-bit integers has a computable total order structure, where the comparison between two elements is determined using the decidable less-than and equality relations.
instOrdUSize instance
: Ord USize
Full source 
instance : Ord USize where
  compare x y := compareOfLessAndEq x y
Total Order Structure on Platform-Dependent Unsigned Integers
Informal description
The type `USize` of platform-dependent unsigned word-size integers is equipped with a computable total order structure, where the comparison function `compare` returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the relative order of two elements.
instOrdChar instance
: Ord Char
Full source 
instance : Ord Char where
  compare x y := compareOfLessAndEq x y
Total Order Structure on Unicode Characters
Informal description
The type of Unicode characters is equipped with a computable total order structure, where the comparison function `compare` returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the relative order of two characters. The order is determined by comparing their underlying Unicode code point values.
instOrdInt8 instance
: Ord Int8
Full source 
instance : Ord Int8 where
  compare x y := compareOfLessAndEq x y
Total Order Structure on 8-bit Signed Integers
Informal description
The 8-bit signed integers `Int8` are equipped with a computable total order structure, where the comparison function `compare` returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the relative order of two elements.
instOrdInt16 instance
: Ord Int16
Full source 
instance : Ord Int16 where
  compare x y := compareOfLessAndEq x y
Computable Total Order on 16-bit Integers
Informal description
The 16-bit integers `Int16` are equipped with a computable total order structure, where the comparison function `compare` returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the relative order of two elements.
instOrdInt32 instance
: Ord Int32
Full source 
instance : Ord Int32 where
  compare x y := compareOfLessAndEq x y
Total Order on 32-bit Integers
Informal description
The 32-bit integers $\text{Int32}$ have a computable total order structure, where the comparison function `compare` returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the relative order of two elements.
instOrdInt64 instance
: Ord Int64
Full source 
instance : Ord Int64 where
  compare x y := compareOfLessAndEq x y
Computable Total Order on 64-bit Integers
Informal description
The 64-bit integers `Int64` are equipped with a computable total order structure, where the comparison function `compare` returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` depending on whether the first argument is less than, equal to, or greater than the second argument.
instOrdISize instance
: Ord ISize
Full source 
instance : Ord ISize where
  compare x y := compareOfLessAndEq x y
Computable Total Order on `ISize` Integers
Informal description
The type `ISize` (a fixed-width integer type) has a computable total order structure, where the comparison function `compare` returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the values of the integers being compared.
instOrdBitVec instance
{n} : Ord (BitVec n)
Full source 
instance {n} : Ord (BitVec n) where
  compare x y := compareOfLessAndEq x y
Computable Total Order on Bitvectors
Informal description
For any bitvector width $n$, the type `BitVec n` has a computable total order structure, where the comparison function `compare` returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the underlying natural number representations of the bitvectors.
instOrdOption instance
[Ord α] : Ord (Option α)
Full source 
instance [Ord α] : Ord (Option α) where
  compare
  | none,   none   => .eq
  | none,   some _ => .lt
  | some _, none   => .gt
  | some x, some y => compare x y
Total Order on Optional Values
Informal description
For any type $\alpha$ with a computable total order structure, the type `Option α` of optional values of $\alpha$ inherits a computable total order structure. In this order, `none` is considered less than any `some x`, and two `some` values are compared according to the order on $\alpha$.
instOrdOrdering instance
: Ord Ordering
Full source 
instance : Ord Ordering where
  compare := compareOn (·.toCtorIdx)
The Computable Total Order on Comparison Results
Informal description
The type `Ordering` has a canonical computable total order structure, where the `compare` function returns `Ordering.lt`, `Ordering.eq`, or `Ordering.gt` based on the standard ordering of comparison results (with `lt < eq < gt`).
List.compareLex definition
{α} (cmp : α → α → Ordering) : List α → List α → Ordering
Full source 
@[specialize]
protected def compareLex {α} (cmp : α → α → Ordering) :
    List α → List α → Ordering
  | [], [] => .eq
  | [], _ => .lt
  | _, [] => .gt
  | x :: xs, y :: ys => match cmp x y with
    | .lt => .lt
    | .eq => xs.compareLex cmp ys
    | .gt => .gt
Lexicographic comparison of lists
Informal description
The function `List.compareLex` takes a comparison function `cmp : α → α → Ordering` and two lists `xs ys : List α`, and returns the lexicographic ordering of the lists based on the given comparison function. Specifically: - If both lists are empty, it returns `Ordering.eq`. - If the first list is empty and the second is not, it returns `Ordering.lt`. - If the first list is non-empty and the second is empty, it returns `Ordering.gt`. - For non-empty lists `x :: xs` and `y :: ys`, it first compares `x` and `y` using `cmp`: - If the result is `Ordering.lt` or `Ordering.gt`, it returns that result. - If the result is `Ordering.eq`, it recursively compares `xs` and `ys`.
List.instOrd instance
{α} [Ord α] : Ord (List α)
Full source 
instance {α} [Ord α] : Ord (List α) where
  compare := List.compareLex compare
Lexicographic Order on Lists
Informal description
For any type $\alpha$ with a computable total order, the type of lists over $\alpha$ inherits a lexicographic order. Specifically, given two lists, they are compared element-wise from left to right using the order on $\alpha$, with the empty list considered smaller than any non-empty list.
List.compare_eq_compareLex theorem
{α} [Ord α] : compare (α := List α) = List.compareLex compare
Full source 
protected theorem compare_eq_compareLex {α} [Ord α] :
    compare (α := List α) = List.compareLex compare := rfl
Lexicographic Order on Lists is Implemented via `compareLex`
Informal description
For any type $\alpha$ with a computable total order, the lexicographic comparison function `compare` on lists of elements of $\alpha$ is equal to the lexicographic comparison function `List.compareLex` applied to the base comparison function `compare` on $\alpha$. In symbols: $$\text{compare} = \text{List.compareLex}\ \text{compare}$$
List.compareLex_cons_cons theorem
{α} {cmp} {x y : α} {xs ys : List α} : (x :: xs).compareLex cmp (y :: ys) = (cmp x y).then (xs.compareLex cmp ys)
Full source 
protected theorem compareLex_cons_cons {α} {cmp} {x y : α} {xs ys : List α} :
    (x :: xs).compareLex cmp (y :: ys) = (cmp x y).then (xs.compareLex cmp ys) := by
  rw [List.compareLex]
  split <;> simp_all
Lexicographic Comparison of Cons Lists
Informal description
For any type $\alpha$, comparison function $\text{cmp} : \alpha \to \alpha \to \text{Ordering}$, elements $x, y \in \alpha$, and lists $xs, ys \in \text{List } \alpha$, the lexicographic comparison of the lists $x :: xs$ and $y :: ys$ is equal to the result of first comparing $x$ and $y$ using $\text{cmp}$, and if they are equal, then comparing $xs$ and $ys$ lexicographically using $\text{cmp}$. In symbols: $$(x :: xs).\text{compareLex}\ \text{cmp}\ (y :: ys) = (\text{cmp}\ x\ y).\text{then}\ (xs.\text{compareLex}\ \text{cmp}\ ys)$$
List.compare_cons_cons theorem
{α} [Ord α] {x y : α} {xs ys : List α} : compare (x :: xs) (y :: ys) = (compare x y).then (compare xs ys)
Full source 
@[simp]
protected theorem compare_cons_cons {α} [Ord α] {x y : α} {xs ys : List α} :
    compare (x :: xs) (y :: ys) = (compare x y).then (compare xs ys) :=
  List.compareLex_cons_cons
Lexicographic Comparison of Non-Empty Lists
Informal description
For any type $\alpha$ with a computable total order, and for any elements $x, y \in \alpha$ and lists $xs, ys \in \text{List } \alpha$, the lexicographic comparison of the lists $x :: xs$ and $y :: ys$ is equal to the result of first comparing $x$ and $y$, and if they are equal, then comparing $xs$ and $ys$. In symbols: $$\text{compare}(x :: xs, y :: ys) = (\text{compare}(x, y)).\text{then}(\text{compare}(xs, ys))$$
List.compareLex_nil_cons theorem
{α} {cmp} {x : α} {xs : List α} : [].compareLex cmp (x :: xs) = .lt
Full source 
protected theorem compareLex_nil_cons {α} {cmp} {x : α} {xs : List α} :
    [].compareLex cmp (x :: xs) = .lt :=
  rfl
Lexicographic comparison: empty list is less than any non-empty list
Informal description
For any type $\alpha$, comparison function $\mathrm{cmp} : \alpha \to \alpha \to \mathrm{Ordering}$, element $x \in \alpha$, and list $\mathrm{xs} : \mathrm{List}\ \alpha$, the lexicographic comparison of the empty list `[]` with the non-empty list `x :: xs` using `cmp` yields the result $\mathrm{lt}$ (less than).
List.compare_nil_cons theorem
{α} [Ord α] {x : α} {xs : List α} : compare [] (x :: xs) = .lt
Full source 
@[simp]
protected theorem compare_nil_cons {α} [Ord α] {x : α} {xs : List α} :
    compare [] (x :: xs) = .lt :=
  rfl
Empty List is Less Than Any Non-Empty List in Lexicographic Order
Informal description
For any type $\alpha$ with a computable total order, and for any element $x \in \alpha$ and list $xs$ of type $\text{List } \alpha$, the lexicographic comparison of the empty list `[]` with the non-empty list $x :: xs$ yields `Ordering.lt`. That is, $\text{compare}~[]~(x :: xs) = \text{lt}$.
List.compareLex_cons_nil theorem
{α} {cmp} {x : α} {xs : List α} : (x :: xs).compareLex cmp [] = .gt
Full source 
protected theorem compareLex_cons_nil {α} {cmp} {x : α} {xs : List α} :
    (x :: xs).compareLex cmp [] = .gt :=
  rfl
Lexicographic Comparison of Non-Empty List with Empty List Yields Greater Than
Informal description
For any type $\alpha$, comparison function `cmp : α → α → Ordering`, element $x \in \alpha$, and list $xs$ of type $\text{List } \alpha$, the lexicographic comparison of the non-empty list $x :: xs$ with the empty list `[]` yields `Ordering.gt`. That is, $(x :: xs).\text{compareLex}~cmp~[] = \text{gt}$.
List.compare_cons_nil theorem
{α} [Ord α] {x : α} {xs : List α} : compare (x :: xs) [] = .gt
Full source 
@[simp]
protected theorem compare_cons_nil {α} [Ord α] {x : α} {xs : List α} :
    compare (x :: xs) [] = .gt :=
  rfl
Non-Empty List is Greater Than Empty List in Lexicographic Order
Informal description
For any type $\alpha$ with a computable total order, and for any element $x \in \alpha$ and list $xs$ of type $\text{List } \alpha$, the lexicographic comparison of the non-empty list $x :: xs$ with the empty list `[]` yields `Ordering.gt`. That is, $\text{compare}(x :: xs, []) = \text{gt}$.
List.compareLex_nil_nil theorem
{α} {cmp} : [].compareLex (α := α) cmp [] = .eq
Full source 
protected theorem compareLex_nil_nil {α} {cmp} :
    [].compareLex (α := α) cmp [] = .eq :=
  rfl
Lexicographic Comparison of Empty Lists Yields Equality
Informal description
For any type $\alpha$ and comparison function `cmp : α → α → Ordering`, the lexicographic comparison of two empty lists is equality, i.e., `[].compareLex cmp [] = Ordering.eq`.
List.compare_nil_nil theorem
{α} [Ord α] : compare (α := List α) [] [] = .eq
Full source 
@[simp]
protected theorem compare_nil_nil {α} [Ord α] :
    compare (α := List α) [] [] = .eq :=
  rfl
Empty Lists Compare Equal in Lexicographic Order
Informal description
For any type $\alpha$ with a computable total order, the lexicographic comparison of two empty lists of type $\alpha$ yields equality, i.e., $\text{compare}([], []) = \text{Ordering.eq}$.
List.isLE_compareLex_nil_left theorem
{α} {cmp} {xs : List α} : (List.compareLex (cmp := cmp) [] xs).isLE
Full source 
protected theorem isLE_compareLex_nil_left {α} {cmp} {xs : List α} :
    (List.compareLex (cmp := cmp) [] xs).isLE := by
  cases xs <;> simp [List.compareLex_nil_nil, List.compareLex_nil_cons]
Lexicographic Comparison of Empty List is Less Than or Equal to Any List
Informal description
For any type $\alpha$, any comparison function `cmp : α → α → Ordering`, and any list `xs : List α`, the lexicographic comparison of the empty list `[]` with `xs` using `cmp` results in a value that satisfies `isLE` (i.e., the result is either `Ordering.lt` or `Ordering.eq`).
List.isLE_compare_nil_left theorem
{α} [Ord α] {xs : List α} : (compare [] xs).isLE
Full source 
protected theorem isLE_compare_nil_left {α} [Ord α] {xs : List α} :
    (compare [] xs).isLE :=
  List.isLE_compareLex_nil_left
Empty List is Lexicographically Less Than or Equal to Any List
Informal description
For any type $\alpha$ with a computable total order and any list $\text{xs} : \text{List } \alpha$, the lexicographic comparison of the empty list `[]` with $\text{xs}$ yields a result that is less than or equal (i.e., $\text{Ordering.lt}$ or $\text{Ordering.eq}$).
List.isLE_compareLex_nil_right theorem
{α} {cmp} {xs : List α} : (List.compareLex (cmp := cmp) xs []).isLE ↔ xs = []
Full source 
protected theorem isLE_compareLex_nil_right {α} {cmp} {xs : List α} :
    (List.compareLex (cmp := cmp) xs []).isLE ↔ xs = [] := by
  cases xs <;> simp [List.compareLex_nil_nil, List.compareLex_cons_nil]
Lexicographic Comparison with Empty List Yields LE iff List is Empty
Informal description
For any type $\alpha$, any comparison function $\text{cmp} : \alpha \to \alpha \to \text{Ordering}$, and any list $\text{xs} : \text{List } \alpha$, the lexicographic comparison of $\text{xs}$ with the empty list `[]` yields a result that is less than or equal (i.e., $\text{Ordering.lt}$ or $\text{Ordering.eq}$) if and only if $\text{xs}$ is itself the empty list. In other words, $\text{List.compareLex cmp xs []}. \text{isLE} \leftrightarrow \text{xs} = []$.
List.isLE_compare_nil_right theorem
{α} [Ord α] {xs : List α} : (compare xs []).isLE ↔ xs = []
Full source 
@[simp]
protected theorem isLE_compare_nil_right {α} [Ord α] {xs : List α} :
    (compare xs []).isLE ↔ xs = [] :=
  List.isLE_compareLex_nil_right
Empty List Comparison: $\text{compare}(xs, []).\text{isLE} \leftrightarrow xs = []$
Informal description
For any type $\alpha$ with a computable total order and any list $xs$ of elements of $\alpha$, the comparison result of $xs$ with the empty list `[]` is less than or equal (i.e., `Ordering.lt` or `Ordering.eq`) if and only if $xs$ is the empty list. In other words, $\text{compare}(xs, []).\text{isLE} \leftrightarrow xs = []$.
List.isGE_compareLex_nil_left theorem
{α} {cmp} {xs : List α} : (List.compareLex (cmp := cmp) [] xs).isGE ↔ xs = []
Full source 
protected theorem isGE_compareLex_nil_left {α} {cmp} {xs : List α} :
    (List.compareLex (cmp := cmp) [] xs).isGE ↔ xs = [] := by
  cases xs <;> simp [List.compareLex_nil_nil, List.compareLex_nil_cons]
Lexicographic Comparison of Empty List is Greater-Than-or-Equal if and only if Compared List is Empty
Informal description
For any type $\alpha$, any comparison function $\text{cmp} : \alpha \to \alpha \to \text{Ordering}$, and any list $xs : \text{List } \alpha$, the lexicographic comparison of the empty list `[]` with $xs$ yields a result indicating "greater than or equal to" (i.e., $\text{isGE}$ returns $\text{true}$) if and only if $xs$ is the empty list.
List.isGE_compare_nil_left theorem
{α} [Ord α] {xs : List α} : (compare [] xs).isGE ↔ xs = []
Full source 
@[simp]
protected theorem isGE_compare_nil_left {α} [Ord α] {xs : List α} :
    (compare [] xs).isGE ↔ xs = [] :=
  List.isGE_compareLex_nil_left
Empty List Comparison: `compare [] xs` is greater-than-or-equal iff $xs = []$
Informal description
For any type $\alpha$ with a computable total order and any list $xs$ of elements of type $\alpha$, the lexicographic comparison of the empty list `[]` with $xs$ yields a result indicating "greater than or equal to" (i.e., `isGE` returns `true`) if and only if $xs$ is the empty list.
List.isGE_compareLex_nil_right theorem
{α} {cmp} {xs : List α} : (List.compareLex (cmp := cmp) xs []).isGE
Full source 
protected theorem isGE_compareLex_nil_right {α} {cmp} {xs : List α} :
    (List.compareLex (cmp := cmp) xs []).isGE := by
  cases xs <;> simp [List.compareLex_nil_nil, List.compareLex_cons_nil]
Lexicographic Comparison of Non-Empty List with Empty List is Greater-Than-or-Equal
Informal description
For any type $\alpha$, any comparison function $\text{cmp} : \alpha \to \alpha \to \text{Ordering}$, and any list $\text{xs} : \text{List } \alpha$, the lexicographic comparison of $\text{xs}$ with the empty list $[]$ results in an ordering that is either greater than or equal to (i.e., $\text{Ordering.isGE}$ returns $\text{true}$).
List.isGE_compare_nil_right theorem
{α} [Ord α] {xs : List α} : (compare xs []).isGE
Full source 
protected theorem isGE_compare_nil_right {α} [Ord α] {xs : List α} :
    (compare xs []).isGE :=
  List.isGE_compareLex_nil_right
Comparison of Non-Empty List with Empty List is Greater-Than-or-Equal
Informal description
For any type $\alpha$ with a computable total order and any list $xs$ of elements of type $\alpha$, the result of comparing $xs$ with the empty list $[]$ is greater than or equal to (i.e., `Ordering.isGE` returns `true`).
List.compareLex_nil_left_eq_eq theorem
{α} {cmp} {xs : List α} : List.compareLex cmp [] xs = .eq ↔ xs = []
Full source 
protected theorem compareLex_nil_left_eq_eq {α} {cmp} {xs : List α} :
    List.compareLexList.compareLex cmp [] xs = .eq ↔ xs = [] := by
  cases xs <;> simp [List.compareLex_nil_nil, List.compareLex_nil_cons]
Empty List Lexicographic Comparison Equality Criterion: $[] \equiv_{\text{lex}} \text{xs} \leftrightarrow \text{xs} = []$
Informal description
For any type $\alpha$, any comparison function $\text{cmp} : \alpha \to \alpha \to \text{Ordering}$, and any list $\text{xs} : \text{List } \alpha$, the lexicographic comparison of the empty list $[]$ with $\text{xs}$ results in equality (i.e., $\text{Ordering.eq}$) if and only if $\text{xs}$ is the empty list $[]$.
List.compare_nil_left_eq_eq theorem
{α} [Ord α] {xs : List α} : compare [] xs = .eq ↔ xs = []
Full source 
@[simp]
protected theorem compare_nil_left_eq_eq {α} [Ord α] {xs : List α} :
    comparecompare [] xs = .eq ↔ xs = [] :=
  List.compareLex_nil_left_eq_eq
Empty List Lexicographic Comparison Criterion: $[] \equiv_{\text{lex}} xs \leftrightarrow xs = []$
Informal description
For any type $\alpha$ with a computable total order and any list $xs$ of elements of type $\alpha$, the lexicographic comparison of the empty list $[]$ with $xs$ yields equality (i.e., $\text{Ordering.eq}$) if and only if $xs$ is the empty list $[]$.
List.compareLex_nil_right_eq_eq theorem
{α} {cmp} {xs : List α} : xs.compareLex cmp [] = .eq ↔ xs = []
Full source 
protected theorem compareLex_nil_right_eq_eq {α} {cmp} {xs : List α} :
    xs.compareLex cmp [] = .eq ↔ xs = [] := by
  cases xs <;> simp [List.compareLex_nil_nil, List.compareLex_cons_nil]
Lexicographic Comparison of List with Empty List Yields Equality if and only if List is Empty
Informal description
For any type $\alpha$, comparison function $\text{cmp} : \alpha \to \alpha \to \text{Ordering}$, and list $\text{xs} : \text{List } \alpha$, the lexicographic comparison of $\text{xs}$ with the empty list `[]` using $\text{cmp}$ returns $\text{Ordering.eq}$ if and only if $\text{xs}$ is the empty list.
List.compare_nil_right_eq_eq theorem
{α} [Ord α] {xs : List α} : compare xs [] = .eq ↔ xs = []
Full source 
@[simp]
protected theorem compare_nil_right_eq_eq {α} [Ord α] {xs : List α} :
    comparecompare xs [] = .eq ↔ xs = [] :=
  List.compareLex_nil_right_eq_eq
Lexicographic Comparison of List with Empty List Yields Equality if and only if List is Empty
Informal description
For any type $\alpha$ with a computable total order and any list $\text{xs}$ of elements of $\alpha$, the lexicographic comparison of $\text{xs}$ with the empty list `[]` returns `Ordering.eq` if and only if $\text{xs}$ is the empty list.
Array.compareLex definition
{α} (cmp : α → α → Ordering) (a₁ a₂ : Array α) : Ordering
Full source 
@[specialize]
protected def compareLex {α} (cmp : α → α → Ordering) (a₁ a₂ : Array α) : Ordering :=
  go 0
where go i :=
  if h₁ : a₁.size <= i then
    if a₂.size <= i then .eq else .lt
  else
    if h₂ : a₂.size <= i then
      .gt
    else match cmp a₁[i] a₂[i] with
      | .lt => .lt
      | .eq => go (i + 1)
      | .gt => .gt
termination_by a₁.size - i
Lexicographic comparison of arrays
Informal description
The function `Array.compareLex` compares two arrays `a₁` and `a₂` lexicographically using a given comparison function `cmp : α → α → Ordering`. The comparison proceeds element-wise from index 0: - If both arrays are exhausted at the current index, they are equal (`Ordering.eq`). - If only the first array is exhausted, it is considered less than the second (`Ordering.lt`). - If only the second array is exhausted, the first is considered greater (`Ordering.gt`). - Otherwise, the elements at the current index are compared using `cmp`: - If the result is `Ordering.lt` or `Ordering.gt`, that result is returned immediately. - If the result is `Ordering.eq`, the comparison continues to the next index. The function terminates because the difference between the array size and the current index decreases with each recursive call.
Array.instOrd instance
{α} [Ord α] : Ord (Array α)
Full source 
instance {α} [Ord α] : Ord (Array α) where
  compare := Array.compareLex compare
Lexicographic Order on Arrays
Informal description
For any type $\alpha$ with a computable total order structure `Ord α`, the type `Array α` of dynamic arrays over $\alpha$ inherits a computable total order structure via lexicographic comparison.
Array.compare_eq_compareLex theorem
{α} [Ord α] : compare (α := Array α) = Array.compareLex compare
Full source 
protected theorem compare_eq_compareLex {α} [Ord α] :
    compare (α := Array α) = Array.compareLex compare := rfl
Equality of Default and Lexicographic Array Comparison
Informal description
For any type $\alpha$ equipped with a computable total order structure `Ord α`, the default comparison function `compare` for arrays of type `Array α` is equal to the lexicographic comparison function `Array.compareLex compare`. In symbols: $$\text{compare} = \text{Array.compareLex}\ \text{compare}$$
List.compareLex_eq_compareLex_toArray theorem
{α} {cmp} {l₁ l₂ : List α} : List.compareLex cmp l₁ l₂ = Array.compareLex cmp l₁.toArray l₂.toArray
Full source 
protected theorem _root_.List.compareLex_eq_compareLex_toArray {α} {cmp} {l₁ l₂ : List α} :
    List.compareLex cmp l₁ l₂ = Array.compareLex cmp l₁.toArray l₂.toArray := by
  simp only [Array.compareLex]
  induction l₁ generalizing l₂ with
  | nil =>
    cases l₂
    · simp [Array.compareLex.go, List.compareLex_nil_nil]
    · simp [Array.compareLex.go, List.compareLex_nil_cons]
  | cons x xs ih =>
    cases l₂
    · simp [Array.compareLex.go, List.compareLex_cons_nil]
    · rw [Array.compareLex.go, List.compareLex_cons_cons]
      simp only [List.size_toArray, List.length_cons, Nat.le_zero_eq, Nat.add_one_ne_zero,
        ↓reduceDIte, List.getElem_toArray, List.getElem_cons_zero, Nat.zero_add]
      split <;> simp_all [compareLex.go_succ]
Equality of Lexicographic Comparisons Between Lists and Their Array Conversions
Informal description
For any type $\alpha$, comparison function $\text{cmp} : \alpha \to \alpha \to \text{Ordering}$, and lists $l_1, l_2 : \text{List } \alpha$, the lexicographic comparison of $l_1$ and $l_2$ using $\text{cmp}$ is equal to the lexicographic comparison of their array conversions $l_1.\text{toArray}$ and $l_2.\text{toArray}$ using the same comparison function $\text{cmp}$. In symbols: $$\text{List.compareLex}\ \text{cmp}\ l_1\ l_2 = \text{Array.compareLex}\ \text{cmp}\ l_1.\text{toArray}\ l_2.\text{toArray}$$
List.compare_eq_compare_toArray theorem
{α} [Ord α] {l₁ l₂ : List α} : compare l₁ l₂ = compare l₁.toArray l₂.toArray
Full source 
protected theorem _root_.List.compare_eq_compare_toArray {α} [Ord α] {l₁ l₂ : List α} :
    compare l₁ l₂ = compare l₁.toArray l₂.toArray :=
  List.compareLex_eq_compareLex_toArray
Equality of Lexicographic Comparisons Between Lists and Their Array Conversions
Informal description
For any type $\alpha$ with a computable total order, and for any two lists $l_1, l_2$ of elements of type $\alpha$, the lexicographic comparison of $l_1$ and $l_2$ is equal to the lexicographic comparison of their array conversions $l_1.\text{toArray}$ and $l_2.\text{toArray}$. In symbols: $$\text{compare}\ l_1\ l_2 = \text{compare}\ l_1.\text{toArray}\ l_2.\text{toArray}$$
Array.compareLex_eq_compareLex_toList theorem
{α} {cmp} {a₁ a₂ : Array α} : Array.compareLex cmp a₁ a₂ = List.compareLex cmp a₁.toList a₂.toList
Full source 
protected theorem compareLex_eq_compareLex_toList {α} {cmp} {a₁ a₂ : Array α} :
    Array.compareLex cmp a₁ a₂ = List.compareLex cmp a₁.toList a₂.toList := by
  rw [List.compareLex_eq_compareLex_toArray]
Equality of Lexicographic Comparisons Between Arrays and Their List Conversions
Informal description
For any type $\alpha$, comparison function $\text{cmp} : \alpha \to \alpha \to \text{Ordering}$, and arrays $a_1, a_2 : \text{Array } \alpha$, the lexicographic comparison of $a_1$ and $a_2$ using $\text{cmp}$ is equal to the lexicographic comparison of their list conversions $a_1.\text{toList}$ and $a_2.\text{toList}$ using the same comparison function $\text{cmp}$. In symbols: $$\text{Array.compareLex}\ \text{cmp}\ a_1\ a_2 = \text{List.compareLex}\ \text{cmp}\ a_1.\text{toList}\ a_2.\text{toList}$$
Array.compare_eq_compare_toList theorem
{α} [Ord α] {a₁ a₂ : Array α} : compare a₁ a₂ = compare a₁.toList a₂.toList
Full source 
protected theorem compare_eq_compare_toList {α} [Ord α] {a₁ a₂ : Array α} :
    compare a₁ a₂ = compare a₁.toList a₂.toList :=
  Array.compareLex_eq_compareLex_toList
Equality of Lexicographic Comparisons Between Arrays and Their List Conversions
Informal description
For any type $\alpha$ with a computable total order, and for any two arrays $a_1, a_2$ of elements of type $\alpha$, the lexicographic comparison of $a_1$ and $a_2$ is equal to the lexicographic comparison of their list conversions $a_1.\text{toList}$ and $a_2.\text{toList}$. In symbols: $$\text{compare}\ a_1\ a_2 = \text{compare}\ a_1.\text{toList}\ a_2.\text{toList}$$
Vector.compareLex definition
{α n} (cmp : α → α → Ordering) (a b : Vector α n) : Ordering
Full source 
protected def compareLex {α n} (cmp : α → α → Ordering) (a b : Vector α n) : Ordering :=
  Array.compareLex cmp a.toArray b.toArray
Lexicographic comparison of vectors
Informal description
The function compares two vectors `a` and `b` of the same length `n` lexicographically using a given comparison function `cmp : α → α → Ordering`. The comparison is performed by converting the vectors to arrays and then applying the lexicographic comparison function `Array.compareLex` on these arrays.
Vector.instOrd instance
{α n} [Ord α] : Ord (Vector α n)
Full source 
instance {α n} [Ord α] : Ord (Vector α n) where
  compare := Vector.compareLex compare
Lexicographic Order on Vectors
Informal description
For any type $\alpha$ with a computable total order and any natural number $n$, the type of vectors $\text{Vector}\,\alpha\,n$ (vectors of length $n$ with elements in $\alpha$) inherits a computable total order structure. The ordering is defined lexicographically using the given comparison function on $\alpha$.
Vector.compareLex_eq_compareLex_toArray theorem
{α n cmp} {a b : Vector α n} : Vector.compareLex cmp a b = Array.compareLex cmp a.toArray b.toArray
Full source 
protected theorem compareLex_eq_compareLex_toArray {α n cmp} {a b : Vector α n} :
    Vector.compareLex cmp a b = Array.compareLex cmp a.toArray b.toArray :=
  rfl
Equality of Vector and Array Lexicographic Comparisons
Informal description
For any type $\alpha$, natural number $n$, and comparison function $\text{cmp} : \alpha \to \alpha \to \text{Ordering}$, the lexicographic comparison of two vectors $a$ and $b$ of length $n$ using $\text{cmp}$ is equal to the lexicographic comparison of their array representations $a.\text{toArray}$ and $b.\text{toArray}$ using the same comparison function $\text{cmp}$.
Vector.compareLex_eq_compareLex_toList theorem
{α n cmp} {a b : Vector α n} : Vector.compareLex cmp a b = List.compareLex cmp a.toList b.toList
Full source 
protected theorem compareLex_eq_compareLex_toList {α n cmp} {a b : Vector α n} :
    Vector.compareLex cmp a b = List.compareLex cmp a.toList b.toList :=
  Array.compareLex_eq_compareLex_toList
Equality of Vector and List Lexicographic Comparisons
Informal description
For any type $\alpha$, natural number $n$, comparison function $\text{cmp} : \alpha \to \alpha \to \text{Ordering}$, and vectors $a, b : \text{Vector}\,\alpha\,n$, the lexicographic comparison of $a$ and $b$ using $\text{cmp}$ is equal to the lexicographic comparison of their list representations $a.\text{toList}$ and $b.\text{toList}$ using the same comparison function $\text{cmp}$. In symbols: $$\text{Vector.compareLex}\ \text{cmp}\ a\ b = \text{List.compareLex}\ \text{cmp}\ a.\text{toList}\ b.\text{toList}$$
Vector.compare_eq_compare_toArray theorem
{α n} [Ord α] {a b : Vector α n} : compare a b = compare a.toArray b.toArray
Full source 
protected theorem compare_eq_compare_toArray {α n} [Ord α] {a b : Vector α n} :
    compare a b = compare a.toArray b.toArray :=
  rfl
Equality of Vector and Array Lexicographic Comparisons
Informal description
For any type $\alpha$ with a computable total order and any natural number $n$, the comparison of two vectors $a$ and $b$ of length $n$ using the lexicographic order on $\text{Vector}\,\alpha\,n$ is equal to the comparison of their array representations $a.\text{toArray}$ and $b.\text{toArray}$ using the lexicographic order on $\text{Array}\,\alpha$.
Vector.compare_eq_compare_toList theorem
{α n} [Ord α] {a b : Vector α n} : compare a b = compare a.toList b.toList
Full source 
protected theorem compare_eq_compare_toList {α n} [Ord α] {a b : Vector α n} :
    compare a b = compare a.toList b.toList :=
  Array.compare_eq_compare_toList
Equality of Vector and List Lexicographic Comparisons
Informal description
For any type $\alpha$ with a computable total order and any natural number $n$, the lexicographic comparison of two vectors $a, b \in \text{Vector}\,\alpha\,n$ is equal to the lexicographic comparison of their list representations $a.\text{toList}$ and $b.\text{toList}$. In symbols: $$\text{compare}\,a\,b = \text{compare}\,a.\text{toList}\,b.\text{toList}$$
lexOrd definition
[Ord α] [Ord β] : Ord (α × β)
Full source 
/-- The lexicographic order on pairs. -/
def lexOrd [Ord α] [Ord β] : Ord (α × β) where
  compare := compareLex (compareOn (·.1)) (compareOn (·.2))
Lexicographic order on pairs
Informal description
The lexicographic order on the product type $\alpha \times \beta$, where two pairs $(a_1, b_1)$ and $(a_2, b_2)$ are compared by first comparing their first components $a_1$ and $a_2$ using the order on $\alpha$, and if they are equal, then comparing their second components $b_1$ and $b_2$ using the order on $\beta$.
ltOfOrd definition
[Ord α] : LT α
Full source 
/--
Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
`Ordering.lt`.
-/
def ltOfOrd [Ord α] : LT α where
  lt a b := compare a b = Ordering.lt
"Less than" relation derived from a computable total order
Informal description
Given a type `α` with a computable total order structure `Ord α`, the definition `ltOfOrd` constructs a "less than" relation `LT α` such that for any two elements `a` and `b` of type `α`, `a < b` holds if and only if the result of comparing `a` and `b` using the `compare` function is `Ordering.lt`.
instDecidableRelLt instance
[Ord α] : DecidableRel (@LT.lt α ltOfOrd)
Full source 
instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
  inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
Decidability of the Derived "Less Than" Relation from a Computable Total Order
Informal description
For any type $\alpha$ equipped with a computable total order structure `Ord α`, the "less than" relation derived from this order is decidable. That is, for any two elements $a, b \in \alpha$, the proposition $a < b$ can be constructively decided using the `compare` function from the `Ord` instance.
leOfOrd definition
[Ord α] : LE α
Full source 
/--
Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare`
satisfies `Ordering.isLE`.
-/
def leOfOrd [Ord α] : LE α where
  le a b := (compare a b).isLE
"Less than or equal to" relation derived from a computable total order
Informal description
Given a type $\alpha$ with a computable total order structure `Ord α`, the definition `leOfOrd` constructs a "less than or equal to" relation `LE α` such that for any two elements $a$ and $b$ of type $\alpha$, $a \leq b$ holds if and only if the result of comparing $a$ and $b$ using the `compare` function satisfies `Ordering.isLE` (i.e., the comparison yields `Ordering.lt` or `Ordering.eq`).
instDecidableRelLe instance
[Ord α] : DecidableRel (@LE.le α leOfOrd)
Full source 
instance [Ord α] : DecidableRel (@LE.le α leOfOrd) :=
  inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))
Decidability of the Derived "Less Than or Equal To" Relation from a Computable Total Order
Informal description
For any type $\alpha$ equipped with a computable total order structure `Ord α`, the "less than or equal to" relation derived from this order is decidable. That is, for any two elements $a, b \in \alpha$, the proposition $a \leq b$ can be constructively decided using the `compare` function from the `Ord` instance.
Ord.toBEq definition
(ord : Ord α) : BEq α
Full source 
/--
Constructs a `BEq` instance from an `Ord` instance.
-/
protected def toBEq (ord : Ord α) : BEq α where
  beq x y := ord.compare x y == .eq
Boolean equality from a computable total order
Informal description
Given a computable total order structure `ord` on a type `α`, the boolean equality relation `==` is defined such that for any two elements `x` and `y` of type `α`, `x == y` holds (i.e., returns `true`) if and only if the result of comparing `x` and `y` using the `compare` function from `ord` is `Ordering.eq`.
Ord.toLT definition
(ord : Ord α) : LT α
Full source 
/--
Constructs an `LT` instance from an `Ord` instance.
-/
protected def toLT (ord : Ord α) : LT α :=
  ltOfOrd
"Less than" relation from a computable total order
Informal description
Given a computable total order structure `ord` on a type `α`, the definition constructs a "less than" relation `LT α` such that for any two elements `a` and `b` of type `α`, `a < b` holds if and only if the result of comparing `a` and `b` using the `compare` function from `ord` is `Ordering.lt`.
Ord.instDecidableRelLt instance
[i : Ord α] : DecidableRel (@LT.lt _ (Ord.toLT i))
Full source 
instance [i : Ord α] : DecidableRel (@LT.lt _ (Ord.toLT i)) :=
  inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
Decidability of the "less than" relation in computable total orders
Informal description
For any type $\alpha$ with a computable total order structure `Ord α`, the "less than" relation $<$ derived from this order is decidable. That is, for any two elements $x, y \in \alpha$, the proposition $x < y$ can be constructively determined to be true or false.
Ord.toLE definition
(ord : Ord α) : LE α
Full source 
/--
Constructs an `LE` instance from an `Ord` instance.
-/
protected def toLE (ord : Ord α) : LE α :=
  leOfOrd
"Less than or equal to" relation from a computable total order
Informal description
Given a computable total order structure `ord` on a type `α`, the definition constructs a "less than or equal to" relation `LE α` such that for any two elements $a$ and $b$ of type $\alpha$, $a \leq b$ holds if and only if the result of comparing $a$ and $b$ using the `compare` function from `ord` satisfies `Ordering.isLE` (i.e., the comparison yields `Ordering.lt` or `Ordering.eq`).
Ord.instDecidableRelLe instance
[i : Ord α] : DecidableRel (@LE.le _ (Ord.toLE i))
Full source 
instance [i : Ord α] : DecidableRel (@LE.le _ (Ord.toLE i)) :=
  inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))
Decidability of the "less than or equal to" relation in computable total orders
Informal description
For any type $\alpha$ with a computable total order structure `Ord α`, the "less than or equal to" relation $\leq$ derived from this order is decidable. That is, for any two elements $x, y \in \alpha$, the proposition $x \leq y$ can be constructively determined to be true or false.
Ord.opposite definition
(ord : Ord α) : Ord α
Full source 
/--
Inverts the order of an `Ord` instance.

The result is an `Ord α` instance that returns `Ordering.lt` when `ord` would return `Ordering.gt`
and that returns `Ordering.gt` when `ord` would return `Ordering.lt`.
-/
protected def opposite (ord : Ord α) : Ord α where
  compare x y := ord.compare y x
Opposite order of a computable total order
Informal description
Given a computable total order structure `Ord α`, the function `Ord.opposite` constructs a new order on `α` where the comparison of any two elements $x$ and $y$ is the reverse of the original order. Specifically, if the original `compare` function returns `Ordering.lt` for $y$ and $x$, the opposite order will return `Ordering.gt` for $x$ and $y$, and vice versa.
Ord.on definition
(_ : Ord β) (f : α → β) : Ord α
Full source 
/--
Constructs an `Ord` instance that compares values according to the results of `f`.

In particular, `ord.on f` compares `x` and `y` by comparing `f x` and `f y` according to `ord`.

The function `compareOn` can be used to perform this comparison without constructing an intermediate
`Ord` instance.
-/
protected def on (_ : Ord β) (f : α → β) : Ord α where
  compare := compareOn f
Order induced by a function
Informal description
Given a computable total order structure on a type $\beta$ and a function $f : \alpha \to \beta$, the function `Ord.on` constructs a computable total order structure on $\alpha$ where two elements $x$ and $y$ are compared by applying $f$ to them and comparing the results using the order on $\beta$.
Ord.lex definition
(_ : Ord α) (_ : Ord β) : Ord (α × β)
Full source 
/--
Constructs the lexicographic order on products `α × β` from orders for `α` and `β`.
-/
protected def lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
  lexOrd
Lexicographic order on pairs
Informal description
The lexicographic order on the product type $\alpha \times \beta$, where two pairs $(a_1, b_1)$ and $(a_2, b_2)$ are compared by first comparing their first components $a_1$ and $a_2$ using the order on $\alpha$, and if they are equal, then comparing their second components $b_1$ and $b_2$ using the order on $\beta$.
Ord.lex' definition
(ord₁ ord₂ : Ord α) : Ord α
Full source 
/--
Constructs an `Ord` instance from two existing instances by combining them lexicographically.

The resulting instance compares elements first by `ord₁` and then, if this returns `Ordering.eq`, by
`ord₂`.

The function `compareLex` can be used to perform this comparison without constructing an
intermediate `Ord` instance. `Ordering.then` can be used to lexicographically combine the results of
comparisons.
-/
protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
  compare := compareLex ord₁.compare ord₂.compare
Lexicographic combination of two computable total orders
Informal description
Given two computable total order structures `ord₁` and `ord₂` on a type `α`, the function `Ord.lex'` constructs a new computable total order structure on `α` that compares elements lexicographically. Specifically, it first compares elements using `ord₁`, and if they are equal according to `ord₁`, it then compares them using `ord₂` to break the tie.
Ord.arrayOrd definition
[a : Ord α] : Ord (Array α)
Full source 
/--
Constructs an order which compares elements of an `Array` in lexicographic order.
-/
protected def arrayOrd [a : Ord α] : Ord (Array α) where
  compare x y :=
    let _ : LT α := a.toLT
    let _ : BEq α := a.toBEq
    if List.lex x.toList y.toList then .lt else if x == y then .eq else .gt
Lexicographic order on arrays
Informal description
Given a type $\alpha$ with a computable total order structure `Ord α`, the function constructs a lexicographic order on arrays of type `Array α`. Two arrays $x$ and $y$ are compared by first converting them to lists and then using the lexicographic order on these lists. The comparison result is `Ordering.lt` if $x$ is lexicographically less than $y$, `Ordering.eq` if they are equal, and `Ordering.gt` otherwise.