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.

Instances

• Array.instReflCmpCompareLex
• Array.instReflOrd
• List.instReflCmpCompareLex
• List.instReflOrd
• Option.instReflOrd
• Std.instReflCmpCompareLex
• Std.instReflCmpCompareOnOfReflOrd
• Std.instReflCmpOfOrientedCmp
• Std.instReflOrdProd
• Vector.instReflCmpCompareLex
• Vector.instReflOrd

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.

Instances

• Array.instOrientedCmpCompareLex
• Array.instOrientedOrd
• Fin.instOrientedOrd
• List.instOrientedCmpCompareLex
• List.instOrientedOrd
• Option.instOrientedOrd
• Std.OrientedCmp.opposite
• Std.OrientedOrd.opposite
• Std.Time.Internal.Bounded.instOrientedOrd
• Std.Time.Internal.instOrientedOrdUnitVal
• Std.Time.instOrientedOrdHourMarker
• Std.Time.instOrientedOrdValidDate
• Std.instOrientedCmpCompareLex
• Std.instOrientedCmpCompareOnOfOrientedOrd
• Std.instOrientedOrdProd
• Vector.instOrientedCmpCompareLex
• Vector.instOrientedOrd

@[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.

Instances

• Array.instTransCmpCompareLex
• Array.instTransOrd
• BitVec.instTransOrd
• Bool.instTransOrd
• Char.instTransOrd
• Fin.instTransOrd
• ISize.instTransOrd
• Int.instTransOrd
• Int16.instTransOrd
• Int32.instTransOrd
• Int64.instTransOrd
• Int8.instTransOrd
• List.instTransCmpCompareLex
• List.instTransOrd
• Nat.instTransOrd
• Option.instTransOrd
• Std.Time.Day.Ordinal.instTransOrdOfYear
• Std.Time.Day.instTransOrdOffset
• Std.Time.Day.instTransOrdOrdinal
• Std.Time.Hour.instTransOrdOffset
• Std.Time.Hour.instTransOrdOrdinal
• Std.Time.Internal.Bounded.instTransOrd
• Std.Time.Internal.instTransOrdUnitVal
• Std.Time.Millisecond.instTransOrdOffset
• Std.Time.Millisecond.instTransOrdOrdinal
• Std.Time.Minute.instTransOrdOffset
• Std.Time.Minute.instTransOrdOrdinal
• Std.Time.Month.instTransOrdOffset
• Std.Time.Month.instTransOrdOrdinal
• Std.Time.Month.instTransOrdQuarter
• Std.Time.Nanosecond.Ordinal.instTransOrdOfDay
• Std.Time.Nanosecond.instTransOrdOffset
• Std.Time.Nanosecond.instTransOrdOrdinal
• Std.Time.Nanosecond.instTransOrdSpan
• Std.Time.Second.instTransOrdOffset
• Std.Time.Second.instTransOrdOrdinal
• Std.Time.TimeZone.instTransOrdOffset
• Std.Time.Week.Ordinal.instTransOrdOfMonth
• Std.Time.Week.instTransOrdOffset
• Std.Time.Week.instTransOrdOrdinal
• Std.Time.Weekday.instTransOrd
• Std.Time.Weekday.instTransOrdOrdinal
• Std.Time.Year.instTransOrdOffset
• Std.Time.instTransOrdDateTime
• Std.Time.instTransOrdDuration
• Std.Time.instTransOrdHourMarker
• Std.Time.instTransOrdPlainDate
• Std.Time.instTransOrdPlainDateTime
• Std.Time.instTransOrdPlainTime
• Std.Time.instTransOrdTimestamp
• Std.Time.instTransOrdValidDate
• Std.TransCmp.opposite
• Std.TransOrd.opposite
• Std.instTransCmpCompareLex
• Std.instTransCmpCompareOnOfTransOrd
• Std.instTransOrdProd
• String.instTransOrd
• UInt16.instTransOrd
• UInt32.instTransOrd
• UInt64.instTransOrd
• UInt8.instTransOrd
• USize.instTransOrd
• Vector.instTransCmpCompareLex
• Vector.instTransOrd

@[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.

Instances

• Array.instLawfulEqCmpCompareLex
• Array.instLawfulEqOrd
• BitVec.instLawfulEqOrd
• Bool.instLawfulEqOrd
• Char.instLawfulEqOrd
• Fin.instLawfulEqOrd
• ISize.instLawfulEqOrd
• Int.instLawfulEqOrd
• Int16.instLawfulEqOrd
• Int32.instLawfulEqOrd
• Int64.instLawfulEqOrd
• Int8.instLawfulEqOrd
• List.instLawfulEqCmpCompareLex
• List.instLawfulEqOrd
• Nat.instLawfulEqOrd
• Option.instLawfulEqOrd
• Std.LawfulBEqCmp.lawfulBEqCmp
• Std.LawfulEqCmp.opposite
• Std.LawfulEqOrd.opposite
• Std.Time.Day.Ordinal.instLawfulEqOrdOfYear
• Std.Time.Day.instLawfulEqOrdOffset
• Std.Time.Day.instLawfulEqOrdOrdinal
• Std.Time.Hour.instLawfulEqOrdOffset
• Std.Time.Hour.instLawfulEqOrdOrdinal
• Std.Time.Internal.Bounded.instLawfulEqOrd
• Std.Time.Internal.instLawfulEqOrdUnitVal
• Std.Time.Millisecond.instLawfulEqOrdOffset
• Std.Time.Millisecond.instLawfulEqOrdOrdinal
• Std.Time.Minute.instLawfulEqOrdOffset
• Std.Time.Minute.instLawfulEqOrdOrdinal
• Std.Time.Month.instLawfulEqOrdOffset
• Std.Time.Month.instLawfulEqOrdOrdinal
• Std.Time.Month.instLawfulEqOrdQuarter
• Std.Time.Nanosecond.Ordinal.instLawfulEqOrdOfDay
• Std.Time.Nanosecond.instLawfulEqOrdOffset
• Std.Time.Nanosecond.instLawfulEqOrdOrdinal
• Std.Time.Nanosecond.instLawfulEqOrdSpan
• Std.Time.Second.instLawfulEqOrdOffset
• Std.Time.Second.instLawfulEqOrdOrdinal
• Std.Time.TimeZone.instLawfulEqOrdOffset
• Std.Time.Week.Ordinal.instLawfulEqOrdOfMonth
• Std.Time.Week.instLawfulEqOrdOffset
• Std.Time.Week.instLawfulEqOrdOrdinal
• Std.Time.Weekday.instLawfulEqOrd
• Std.Time.Weekday.instLawfulEqOrdOrdinal
• Std.Time.Year.instLawfulEqOrdOffset
• Std.Time.instLawfulEqOrdDuration
• Std.Time.instLawfulEqOrdHourMarker
• Std.Time.instLawfulEqOrdPlainDate
• Std.Time.instLawfulEqOrdPlainDateTime
• Std.Time.instLawfulEqOrdPlainTime
• Std.Time.instLawfulEqOrdTimestamp
• Std.Time.instLawfulEqOrdValidDate
• Std.instLawfulEqOrdProd
• String.instLawfulEqOrd
• UInt16.instLawfulEqOrd
• UInt32.instLawfulEqOrd
• UInt64.instLawfulEqOrd
• UInt8.instLawfulEqOrd
• USize.instLawfulEqOrd
• Vector.instLawfulEqCmpCompareLex
• Vector.instLawfulEqOrd

@[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 α

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

@[simp]

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.

Instances

• Array.instLawfulBEqCmpCompareLex
• Array.instLawfulBEqOrd
• List.instLawfulBEqCmpCompareLex
• List.instLawfulBEqOrd
• Option.instLawfulBEqOrd
• Std.LawfulBEqCmp.opposite
• Std.LawfulBEqOrd.opposite
• Std.Time.instLawfulBEqOrdDateTime
• Std.instLawfulBEqCmpOfLawfulEqCmpOfLawfulBEq
• Std.instLawfulBEqOrd
• Vector.instLawfulBEqCmpCompareLex
• Vector.instLawfulBEqOrd

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.lawfulBEqCmp {α : Type u} [BEq α] {cmp : α → α → Ordering} [inst : LawfulBEqCmp cmp] [LawfulBEq α] : LawfulEqCmp cmp

theorem Std.LawfulBEqOrd.lawfulBEqOrd {α : 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 α)