class Lake.EqOfCmp (α : Type u) (cmp : α → α → Ordering) : Type

• eq_of_cmp : ∀ {a a' : α}, cmp a a' = Ordering.eq → a = a'

Proof that the equality of a compare function corresponds to propositional equality.

class Lake.LawfulCmpEq (α : Type u) (cmp : α → α → Ordering) extends Lake.EqOfCmp : Type

• eq_of_cmp : ∀ {a a' : α}, cmp a a' = Ordering.eq → a = a'
• cmp_rfl : ∀ {a : α}, cmp a a = Ordering.eq

Proof that the equality of a compare function corresponds to propositional equality and vice versa.

@[simp]

theorem Lake.cmp_iff_eq {α : Type u_1} {cmp : α → α → Ordering} {a : α} {a' : α} [Lake.LawfulCmpEq α cmp] : cmp a a' = Ordering.eq ↔ a = a'

class Lake.EqOfCmpWrt (α : Type u) {β : Type v} (f : α → β) (cmp : α → α → Ordering) : Type

• eq_of_cmp_wrt : ∀ {a a' : α}, cmp a a' = Ordering.eq → f a = f a'

Proof that the equality of a compare function corresponds to propositional equality with respect to a given function.

instance Lake.instEqOfCmpWrtType {α : Type u_1} {cmp : α → α → Ordering} : Lake.EqOfCmpWrt α (fun x => α) cmp

instance Lake.instEqOfCmpWrt {α : Type u_1} {cmp : α → α → Ordering} : {β : Type u_2} → {f : α → β} → [inst : Lake.EqOfCmp α cmp] → Lake.EqOfCmpWrt α f cmp

instance Lake.instEqOfCmp {α : Type u_1} {cmp : α → α → Ordering} [Lake.EqOfCmpWrt α (fun a => a) cmp] : Lake.EqOfCmp α cmp

theorem Lake.eq_of_compareOfLessAndEq {α : Type u_1} [LT α] [DecidableEq α] {a : α} {a' : α} [Decidable (a < a')] (h : compareOfLessAndEq a a' = Ordering.eq) : a = a'

theorem Lake.compareOfLessAndEq_rfl {α : Type u_1} [LT α] [DecidableEq α] {a : α} [Decidable (a < a)] (lt_irrefl : ¬a < a) : compareOfLessAndEq a a = Ordering.eq

instance Lake.instLawfulCmpEqNatCompareInstOrdNat : Lake.LawfulCmpEq Nat compare

theorem Lake.Fin.eq_of_compare {m : Nat} {n : Fin m} {n' : Fin m} (h : compare n n' = Ordering.eq) : n = n'

instance Lake.instLawfulCmpEqFinCompareInstOrdFin {n : Nat} : Lake.LawfulCmpEq (Fin n) compare

instance Lake.instLawfulCmpEqUInt64CompareInstOrdUInt64 : Lake.LawfulCmpEq UInt64 compare

theorem Lake.List.lt_irrefl {α : Type u_1} [LT α] (irrefl_α : ∀ (a : α), ¬a < a) (a : List α) : ¬a < a

@[simp]

theorem Lake.String.lt_irrefl (s : String) : ¬s < s

instance Lake.instLawfulCmpEqStringCompareInstOrdString : Lake.LawfulCmpEq String compare

@[macro_inline]

def Lake.Option.compareWith {α : Type u_1} (cmp : α → α → Ordering) : Option α → Option α → Ordering

instance Lake.instEqOfCmpOptionCompareWith {α : Type u_1} {cmp : α → α → Ordering} [Lake.EqOfCmp α cmp] : Lake.EqOfCmp (Option α) (Lake.Option.compareWith cmp)

instance Lake.instLawfulCmpEqOptionCompareWith {α : Type u_1} {cmp : α → α → Ordering} [Lake.LawfulCmpEq α cmp] : Lake.LawfulCmpEq (Option α) (Lake.Option.compareWith cmp)

def Lake.Prod.compareWith {α : Type u_1} {β : Type u_2} (cmpA : α → α → Ordering) (cmpB : β → β → Ordering) : α × β → α × β → Ordering

instance Lake.instEqOfCmpProdCompareWith {α : Type u_1} {cmpA : α → α → Ordering} {β : Type u_2} {cmpB : β → β → Ordering} [Lake.EqOfCmp α cmpA] [Lake.EqOfCmp β cmpB] : Lake.EqOfCmp (α × β) (Lake.Prod.compareWith cmpA cmpB)

instance Lake.instLawfulCmpEqProdCompareWith {α : Type u_1} {cmpA : α → α → Ordering} {β : Type u_2} {cmpB : β → β → Ordering} [Lake.LawfulCmpEq α cmpA] [Lake.LawfulCmpEq β cmpB] : Lake.LawfulCmpEq (α × β) (Lake.Prod.compareWith cmpA cmpB)