Type classes related to Ord

This file provides several typeclasses encode properties of an Ord instance. For each typeclass, there is also a variant that does not depend on an Ord instance and takes an explicit comparison function cmp : α → α → Ordering instead.

class Std.ReflCmp {α : Type u} (cmp : α → α → Ordering) : Prop

A typeclass for comparison functions cmp for which cmp a a = .eq for all a.

• compare_self {a : α} : cmp a a = Ordering.eq

  Comparison is reflexive.

theorem Std.ReflCmp.cmp_eq_of_eq {α : Type u} {cmp : α → α → Ordering} [ReflCmp cmp] {a b : α} : a = b → cmp a b = Ordering.eq

@[reducible, inline]

abbrev Std.ReflOrd (α : Type u) [Ord α] : Prop

A typeclasses for ordered types for which compare a a = .eq for all a.

Equations

• Std.ReflOrd α = Std.ReflCmp compare

@[simp]

theorem Std.ReflOrd.compare_self {α : Type u} [Ord α] [ReflOrd α] {a : α} : compare a a = Ordering.eq

theorem Std.ReflCmp.isLE_rfl {α : Type u_1} {cmp : α → α → Ordering} [ReflCmp cmp] {a : α} : (cmp a a).isLE = true

@[simp]

theorem Std.ReflOrd.isLE_rfl {α : Type u_1} [Ord α] [ReflOrd α] {a : α} : (compare a a).isLE = true

class Std.OrientedCmp {α : Type u} (cmp : α → α → Ordering) : Prop

A typeclass for functions α → α → Ordering which are oriented: flipping the arguments amounts to applying Ordering.swap to the return value.

• eq_swap {a b : α} : cmp a b = (cmp b a).swap

  Swapping the arguments to cmp swaps the outcome.

@[reducible, inline]

abbrev Std.OrientedOrd (α : Type u) [Ord α] : Prop

A typeclass for types with an oriented comparison function: flipping the arguments amounts to applying Ordering.swap to the return value.

Equations

• Std.OrientedOrd α = Std.OrientedCmp compare

theorem Std.OrientedOrd.eq_swap {α : Type u} [Ord α] [OrientedOrd α] {a b : α} : compare a b = (compare b a).swap

instance Std.instReflCmpOfOrientedCmp {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] : ReflCmp cmp

instance Std.OrientedCmp.opposite {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] : OrientedCmp fun (a b : α) => cmp b a

instance Std.OrientedOrd.opposite {α : Type u} [Ord α] [OrientedOrd α] : OrientedOrd α

theorem Std.OrientedCmp.gt_iff_lt {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.gt ↔ cmp b a = Ordering.lt

theorem Std.OrientedCmp.isGT_eq_isLT {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : (cmp a b).isGT = (cmp b a).isLT

theorem Std.OrientedCmp.lt_of_gt {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.gt → cmp b a = Ordering.lt

theorem Std.OrientedCmp.gt_of_lt {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.lt → cmp b a = Ordering.gt

theorem Std.OrientedCmp.isGE_eq_isLE {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : (cmp a b).isGE = (cmp b a).isLE

theorem Std.OrientedCmp.isGE_iff_isLE {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : (cmp a b).isGE = true ↔ (cmp b a).isLE = true

theorem Std.OrientedCmp.isLE_of_isGE {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : (cmp b a).isGE = true → (cmp a b).isLE = true

theorem Std.OrientedCmp.isGE_of_isLE {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : (cmp b a).isLE = true → (cmp a b).isGE = true

theorem Std.OrientedCmp.eq_comm {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.eq ↔ cmp b a = Ordering.eq

theorem Std.OrientedCmp.eq_symm {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.eq → cmp b a = Ordering.eq

theorem Std.OrientedCmp.not_isLE_of_lt {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.lt → ¬(cmp b a).isLE = true

theorem Std.OrientedCmp.not_isGE_of_gt {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.gt → ¬(cmp b a).isGE = true

theorem Std.OrientedCmp.not_lt_of_isLE {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : (cmp a b).isLE = true → cmp b a ≠ Ordering.lt

theorem Std.OrientedCmp.not_gt_of_isGE {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : (cmp a b).isGE = true → cmp b a ≠ Ordering.gt

theorem Std.OrientedCmp.not_lt_of_lt {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.lt → cmp b a ≠ Ordering.lt

theorem Std.OrientedCmp.not_gt_of_gt {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : cmp a b = Ordering.gt → cmp b a ≠ Ordering.gt

theorem Std.OrientedCmp.lt_of_not_isLE {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : ¬(cmp a b).isLE = true → cmp b a = Ordering.lt

theorem Std.OrientedCmp.gt_of_not_isGE {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} : ¬(cmp a b).isGE = true → cmp b a = Ordering.gt

theorem Std.OrientedCmp.isLE_antisymm {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} (h₁ : (cmp a b).isLE = true) (h₂ : (cmp b a).isLE = true) : cmp a b = Ordering.eq

theorem Std.OrientedCmp.isGE_antisymm {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] {a b : α} (h₁ : (cmp a b).isGE = true) (h₂ : (cmp b a).isGE = true) : cmp a b = Ordering.eq

class Std.TransCmp {α : Type u} (cmp : α → α → Ordering) extends Std.OrientedCmp cmp : Prop

A typeclass for functions α → α → Ordering which are transitive.

• eq_swap {a b : α} : cmp a b = (cmp b a).swap
• isLE_trans {a b c : α} : (cmp a b).isLE = true → (cmp b c).isLE = true → (cmp a c).isLE = true

  Transitivity of cmp, expressed via Ordering.isLE.

@[reducible, inline]

abbrev Std.TransOrd (α : Type u) [Ord α] : Prop

A typeclass for types with a transitive ordering function.

Equations

• Std.TransOrd α = Std.TransCmp compare

theorem Std.TransOrd.isLE_trans {α : Type u} [Ord α] [TransOrd α] {a b c : α} : (compare a b).isLE = true → (compare b c).isLE = true → (compare a c).isLE = true

theorem Std.TransCmp.isGE_trans {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (h₁ : (cmp a b).isGE = true) (h₂ : (cmp b c).isGE = true) : (cmp a c).isGE = true

theorem Std.TransOrd.isGE_trans {α : Type u} [Ord α] [TransOrd α] {a b c : α} : (compare a b).isGE = true → (compare b c).isGE = true → (compare a c).isGE = true

instance Std.TransCmp.opposite {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] : TransCmp fun (a b : α) => cmp b a

instance Std.TransOrd.opposite {α : Type u} [Ord α] [TransOrd α] : TransOrd α

theorem Std.TransCmp.lt_of_lt_of_eq {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.lt) (hbc : cmp b c = Ordering.eq) : cmp a c = Ordering.lt

theorem Std.TransCmp.lt_of_eq_of_lt {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.eq) (hbc : cmp b c = Ordering.lt) : cmp a c = Ordering.lt

theorem Std.TransCmp.gt_of_eq_of_gt {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.eq) (hbc : cmp b c = Ordering.gt) : cmp a c = Ordering.gt

theorem Std.TransCmp.gt_of_gt_of_eq {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.gt) (hbc : cmp b c = Ordering.eq) : cmp a c = Ordering.gt

theorem Std.TransCmp.lt_trans {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.lt) (hbc : cmp b c = Ordering.lt) : cmp a c = Ordering.lt

theorem Std.TransCmp.gt_trans {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.gt) (hbc : cmp b c = Ordering.gt) : cmp a c = Ordering.gt

theorem Std.TransCmp.lt_of_lt_of_isLE {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.lt) (hbc : (cmp b c).isLE = true) : cmp a c = Ordering.lt

theorem Std.TransCmp.lt_of_isLE_of_lt {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : (cmp a b).isLE = true) (hbc : cmp b c = Ordering.lt) : cmp a c = Ordering.lt

theorem Std.TransCmp.gt_of_gt_of_isGE {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.gt) (hbc : (cmp b c).isGE = true) : cmp a c = Ordering.gt

theorem Std.TransCmp.gt_of_gt_of_gt {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.gt) (hbc : cmp b c = Ordering.gt) : cmp a c = Ordering.gt

theorem Std.TransCmp.gt_of_isGE_of_gt {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : (cmp a b).isGE = true) (hbc : cmp b c = Ordering.gt) : cmp a c = Ordering.gt

theorem Std.TransCmp.eq_trans {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.eq) (hbc : cmp b c = Ordering.eq) : cmp a c = Ordering.eq

theorem Std.TransCmp.congr_left {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hab : cmp a b = Ordering.eq) : cmp a c = cmp b c

theorem Std.TransCmp.congr_right {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a b c : α} (hbc : cmp b c = Ordering.eq) : cmp a b = cmp a c

class Std.LawfulEqCmp {α : Type u} (cmp : α → α → Ordering) extends Std.ReflCmp cmp : Prop

A typeclass for comparison functions satisfying cmp a b = .eq if and only if the logical equality a = b holds.

This typeclass distinguishes itself from LawfulBEqCmp by using logical equality (=) instead of boolean equality (==).

• compare_self {a : α} : cmp a a = Ordering.eq
• eq_of_compare {a b : α} : cmp a b = Ordering.eq → a = b

  If two values compare equal, then they are logically equal.

@[reducible, inline]

abbrev Std.LawfulEqOrd (α : Type u) [Ord α] : Prop

A typeclass for types with a comparison function that satisfies compare a b = .eq if and only if the logical equality a = b holds.

This typeclass distinguishes itself from LawfulBEqOrd by using logical equality (=) instead of boolean equality (==).

Equations

• Std.LawfulEqOrd α = Std.LawfulEqCmp compare

theorem Std.LawfulEqOrd.eq_of_compare {α : Type u} [Ord α] [LawfulEqOrd α] {a b : α} : compare a b = Ordering.eq → a = b

instance Std.LawfulEqCmp.opposite {α : Type u} {cmp : α → α → Ordering} [OrientedCmp cmp] [LawfulEqCmp cmp] : LawfulEqCmp fun (a b : α) => cmp b a

instance Std.LawfulEqOrd.opposite {α : Type u} [Ord α] [OrientedOrd α] [LawfulEqOrd α] : LawfulEqOrd α

@[simp]

theorem Std.LawfulEqCmp.compare_eq_iff_eq {α : Type u} {cmp : α → α → Ordering} [LawfulEqCmp cmp] {a b : α} : cmp a b = Ordering.eq ↔ a = b

theorem Std.LawfulEqCmp.compare_beq_iff_eq {α : Type u} {cmp : α → α → Ordering} [LawfulEqCmp cmp] {a b : α} : (cmp a b == Ordering.eq) = true ↔ a = b

@[simp]

theorem Std.LawfulEqOrd.compare_eq_iff_eq {α : Type u} [Ord α] [LawfulEqOrd α] {a b : α} : compare a b = Ordering.eq ↔ a = b

The corresponding lemma for LawfulEqCmp is LawfulEqCmp.compare_eq_iff_eq

theorem Std.LawfulEqOrd.compare_beq_iff_eq {α : Type u} [Ord α] [LawfulEqOrd α] {a b : α} : (compare a b == Ordering.eq) = true ↔ a = b

The corresponding lemma for LawfulEqCmp is LawfulEqCmp.compare_beq_iff_eq

class Std.LawfulBEqCmp {α : Type u} [BEq α] (cmp : α → α → Ordering) : Prop

A typeclass for comparison functions satisfying cmp a b = .eq if and only if the boolean equality a == b holds.

This typeclass distinguishes itself from LawfulEqCmp by using boolean equality (==) instead of logical equality (=).

• compare_eq_iff_beq {a b : α} : cmp a b = Ordering.eq ↔ (a == b) = true

  If two values compare equal, then they are boolean equal.

theorem Std.LawfulBEqCmp.not_compare_eq_iff_beq_eq_false {α : Type u} [BEq α] {cmp : α → α → Ordering} [LawfulBEqCmp cmp] {a b : α} : ¬cmp a b = Ordering.eq ↔ (a == b) = false

theorem Std.LawfulBEqCmp.compare_beq_eq_beq {α : Type u} [BEq α] {cmp : α → α → Ordering} [LawfulBEqCmp cmp] {a b : α} : (cmp a b == Ordering.eq) = (a == b)

theorem Std.LawfulBEqCmp.isEq_compare_eq_beq {α : Type u} [BEq α] {cmp : α → α → Ordering} [LawfulBEqCmp cmp] {a b : α} : (cmp a b).isEq = (a == b)

@[reducible, inline]

abbrev Std.LawfulBEqOrd (α : Type u) [BEq α] [Ord α] : Prop

A typeclass for types with a comparison function that satisfies compare a b = .eq if and only if the boolean equality a == b holds.

This typeclass distinguishes itself from LawfulEqOrd by using boolean equality (==) instead of logical equality (=).

Equations

• Std.LawfulBEqOrd α = Std.LawfulBEqCmp compare

theorem Std.LawfulBEqOrd.compare_eq_iff_beq {α : Type u} {x✝ : Ord α} {x✝¹ : BEq α} [LawfulBEqOrd α] {a b : α} : compare a b = Ordering.eq ↔ (a == b) = true

theorem Std.LawfulBEqOrd.not_compare_eq_iff_beq_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Ord α} [LawfulBEqOrd α] {a b : α} : ¬compare a b = Ordering.eq ↔ (a == b) = false

theorem Std.LawfulBEqOrd.compare_beq_eq_beq {α : Type u} {x✝ : Ord α} {x✝¹ : BEq α} [LawfulBEqOrd α] {a b : α} : (compare a b == Ordering.eq) = (a == b)

theorem Std.LawfulBEqOrd.isEq_compare_eq_beq {α : Type u} {x✝ : Ord α} {x✝¹ : BEq α} [LawfulBEqOrd α] {a b : α} : (compare a b).isEq = (a == b)

instance Std.instLawfulBEqCmpOfLawfulEqCmpOfLawfulBEq {α : Type u} [BEq α] {cmp : α → α → Ordering} [LawfulEqCmp cmp] [LawfulBEq α] : LawfulBEqCmp cmp

theorem Std.LawfulBEqCmp.reflBEq {α : Type u} [BEq α] {cmp : α → α → Ordering} [inst : LawfulBEqCmp cmp] [ReflCmp cmp] : ReflBEq α

theorem Std.LawfulBEqCmp.equivBEq {α : Type u} [BEq α] {cmp : α → α → Ordering} [inst : LawfulBEqCmp cmp] [TransCmp cmp] : EquivBEq α

instance Std.LawfulBEqOrd.equivBEq {α : Type u} [BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] : EquivBEq α

theorem Std.LawfulBEqCmp.lawfulBEq {α : Type u} [BEq α] {cmp : α → α → Ordering} [inst : LawfulBEqCmp cmp] [LawfulEqCmp cmp] : LawfulBEq α

instance Std.LawfulBEqOrd.lawfulBEq {α : Type u} [BEq α] [Ord α] [LawfulBEqOrd α] [LawfulEqOrd α] : LawfulBEq α

instance Std.LawfulBEqCmp.lawfulEqCmp {α : Type u} [BEq α] {cmp : α → α → Ordering} [inst : LawfulBEqCmp cmp] [LawfulBEq α] : LawfulEqCmp cmp

theorem Std.LawfulBEqOrd.lawfulEqOrd {α : Type u} [BEq α] [Ord α] [LawfulBEqOrd α] [LawfulBEq α] : LawfulEqOrd α

instance Std.LawfulBEqCmp.opposite {α : Type u} [BEq α] {cmp : α → α → Ordering} [OrientedCmp cmp] [LawfulBEqCmp cmp] : LawfulBEqCmp fun (a b : α) => cmp b a

instance Std.LawfulBEqOrd.opposite {α : Type u} [BEq α] [Ord α] [OrientedOrd α] [LawfulBEqOrd α] : LawfulBEqOrd α

instance Std.instLawfulBEqOrd {α : Type u} {x✝ : Ord α} : LawfulBEqOrd α

theorem Std.TransOrd.compareOfLessAndEq_of_lt_trans_of_lt_iff {α : Type u} [LT α] [DecidableLT α] [DecidableEq α] (lt_trans : ∀ {a b c : α}, a < b → b < c → a < c) (h : ∀ (x y : α), x < y ↔ ¬y < x ∧ x ≠ y) : TransCmp fun (x y : α) => compareOfLessAndEq x y

theorem Std.TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α] (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y) (trans : ∀ {x y z : α}, x ≤ y → y ≤ z → x ≤ z) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬x ≤ y ↔ y < x) : TransCmp fun (x y : α) => compareOfLessAndEq x y

instance Bool.instTransOrd : Std.TransOrd Bool

instance Bool.instLawfulEqOrd : Std.LawfulEqOrd Bool

instance Nat.instTransOrd : Std.TransOrd Nat

instance Nat.instLawfulEqOrd : Std.LawfulEqOrd Nat

instance Int.instTransOrd : Std.TransOrd Int

instance Int.instLawfulEqOrd : Std.LawfulEqOrd Int

instance Fin.instOrientedOrd (n : Nat) : Std.OrientedOrd (Fin n)

instance Fin.instTransOrd (n : Nat) : Std.TransOrd (Fin n)

instance Fin.instLawfulEqOrd (n : Nat) : Std.LawfulEqOrd (Fin n)

instance Option.instOrientedOrd {α : Type u_1} [Ord α] [Std.OrientedOrd α] : Std.OrientedOrd (Option α)

instance Option.instTransOrd {α : Type u_1} [Ord α] [Std.TransOrd α] : Std.TransOrd (Option α)

instance Option.instReflOrd {α : Type u_1} [Ord α] [Std.ReflOrd α] : Std.ReflOrd (Option α)

instance Option.instLawfulEqOrd {α : Type u_1} [Ord α] [Std.LawfulEqOrd α] : Std.LawfulEqOrd (Option α)

instance Option.instLawfulBEqOrd {α : Type u_1} [Ord α] [BEq α] [Std.LawfulBEqOrd α] : Std.LawfulBEqOrd (Option α)

instance Std.instReflCmpCompareLex {α : Type u_1} {cmp₁ cmp₂ : α → α → Ordering} [ReflCmp cmp₁] [ReflCmp cmp₂] : ReflCmp (compareLex cmp₁ cmp₂)

instance Std.instOrientedCmpCompareLex {α : Type u_1} {cmp₁ cmp₂ : α → α → Ordering} [OrientedCmp cmp₁] [OrientedCmp cmp₂] : OrientedCmp (compareLex cmp₁ cmp₂)

instance Std.instTransCmpCompareLex {α : Type u_1} {cmp₁ cmp₂ : α → α → Ordering} [TransCmp cmp₁] [TransCmp cmp₂] : TransCmp (compareLex cmp₁ cmp₂)

instance Std.instReflCmpCompareOnOfReflOrd {α : Type u_1} {β : Type u_2} {f : α → β} [Ord β] [ReflOrd β] : ReflCmp (compareOn f)

instance Std.instOrientedCmpCompareOnOfOrientedOrd {α : Type u_1} {β : Type u_2} {f : α → β} [Ord β] [OrientedOrd β] : OrientedCmp (compareOn f)

instance Std.instTransCmpCompareOnOfTransOrd {α : Type u_1} {β : Type u_2} {f : α → β} [Ord β] [TransOrd β] : TransCmp (compareOn f)

instance Std.instReflOrdProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [ReflOrd α] [ReflOrd β] : ReflOrd (α × β)

instance Std.instOrientedOrdProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [OrientedOrd α] [OrientedOrd β] : OrientedOrd (α × β)

instance Std.instTransOrdProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [TransOrd α] [TransOrd β] : TransOrd (α × β)

instance Std.instLawfulEqOrdProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [LawfulEqOrd α] [LawfulEqOrd β] : LawfulEqOrd (α × β)

instance List.instReflCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.ReflCmp cmp] : Std.ReflCmp (List.compareLex cmp)

instance List.instLawfulEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] : Std.LawfulEqCmp (List.compareLex cmp)

instance List.instLawfulBEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [BEq α] [Std.LawfulBEqCmp cmp] : Std.LawfulBEqCmp (List.compareLex cmp)

instance List.instOrientedCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] : Std.OrientedCmp (List.compareLex cmp)

instance List.instTransCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] : Std.TransCmp (List.compareLex cmp)

instance List.instReflOrd {α : Type u_1} [Ord α] [Std.ReflOrd α] : Std.ReflOrd (List α)

instance List.instLawfulEqOrd {α : Type u_1} [Ord α] [Std.LawfulEqOrd α] : Std.LawfulEqOrd (List α)

instance List.instLawfulBEqOrd {α : Type u_1} [Ord α] [BEq α] [Std.LawfulBEqOrd α] : Std.LawfulBEqOrd (List α)

instance List.instOrientedOrd {α : Type u_1} [Ord α] [Std.OrientedOrd α] : Std.OrientedOrd (List α)

instance List.instTransOrd {α : Type u_1} [Ord α] [Std.TransOrd α] : Std.TransOrd (List α)

instance Array.instReflCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.ReflCmp cmp] : Std.ReflCmp (Array.compareLex cmp)

instance Array.instLawfulEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] : Std.LawfulEqCmp (Array.compareLex cmp)

instance Array.instLawfulBEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [BEq α] [Std.LawfulBEqCmp cmp] : Std.LawfulBEqCmp (Array.compareLex cmp)

instance Array.instOrientedCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] : Std.OrientedCmp (Array.compareLex cmp)

instance Array.instTransCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] : Std.TransCmp (Array.compareLex cmp)

instance Array.instReflOrd {α : Type u_1} [Ord α] [Std.ReflOrd α] : Std.ReflOrd (Array α)

instance Array.instLawfulEqOrd {α : Type u_1} [Ord α] [Std.LawfulEqOrd α] : Std.LawfulEqOrd (Array α)

instance Array.instLawfulBEqOrd {α : Type u_1} [Ord α] [BEq α] [Std.LawfulBEqOrd α] : Std.LawfulBEqOrd (Array α)

instance Array.instOrientedOrd {α : Type u_1} [Ord α] [Std.OrientedOrd α] : Std.OrientedOrd (Array α)

instance Array.instTransOrd {α : Type u_1} [Ord α] [Std.TransOrd α] : Std.TransOrd (Array α)