Documentation

Std.Data.Internal.List.Associative

This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.

File contents: Verification of associative lists

theorem Std.Internal.List.assoc_induction {α : Type u} {β : αType v} {motive : List ((a : α) × β a)Prop} (nil : motive []) (cons : ∀ (k : α) (v : β k) (tail : List ((a : α) × β a)), motive tailmotive (k, v :: tail)) (t : List ((a : α) × β a)) :
motive t
def Std.Internal.List.getEntry? {α : Type u} {β : αType v} [BEq α] (a : α) :
List ((a : α) × β a)Option ((a : α) × β a)

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.getEntry?_nil {α : Type u} {β : αType v} [BEq α] {a : α} :
theorem Std.Internal.List.getEntry?_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getEntry? a (k, v :: l) = bif k == a then some k, v else getEntry? a l
theorem Std.Internal.List.getEntry?_eq_find {α : Type u} {β : αType v} [BEq α] {k : α} {l : List ((a : α) × β a)} :
getEntry? k l = List.find? (fun (x : (a : α) × β a) => x.fst == k) l
theorem Std.Internal.List.getEntry?_cons_of_true {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) :
getEntry? a (k, v :: l) = some k, v
theorem Std.Internal.List.getEntry?_cons_of_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = false) :
getEntry? a (k, v :: l) = getEntry? a l
@[simp]
theorem Std.Internal.List.getEntry?_cons_self {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
getEntry? k (k, v :: l) = some k, v
theorem Std.Internal.List.beq_of_getEntry?_eq_some {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} {p : (a : α) × β a} (h : getEntry? a l = some p) :
(p.fst == a) = true
theorem Std.Internal.List.getEntry?_congr {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α} (h : (a == b) = true) :
theorem Std.Internal.List.keys_eq_map {α : Type u} {β : αType v} {l : List ((a : α) × β a)} :
keys l = List.map (fun (x : (a : α) × β a) => x.fst) l
theorem Std.Internal.List.getEntry?_eq_some_iff {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {e : (a : α) × β a} {k : α} (hd : DistinctKeys l) :
getEntry? k l = some e (k == e.fst) = true e l
theorem Std.Internal.List.mem_iff_getEntry?_eq_some {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a} (h : DistinctKeys l) :
theorem Std.Internal.List.isEmpty_eq_false_iff_exists_isSome_getEntry? {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.isEmpty_iff_forall_isSome_getEntry? {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} :
l.isEmpty = true ∀ (a : α), (getEntry? a l).isSome = false
def Std.Internal.List.getValue? {α : Type u} {β : Type v} [BEq α] (a : α) :
List ((_ : α) × β)Option β

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.getValue?_nil {α : Type u} {β : Type v} [BEq α] {a : α} :
theorem Std.Internal.List.getValue?_cons {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} :
getValue? a (k, v :: l) = bif k == a then some v else getValue? a l
theorem Std.Internal.List.getValue?_cons_of_true {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = true) :
getValue? a (k, v :: l) = some v
theorem Std.Internal.List.getValue?_cons_of_false {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = false) :
getValue? a (k, v :: l) = getValue? a l
@[simp]
theorem Std.Internal.List.getValue?_cons_self {α : Type u} {β : Type v} [BEq α] [ReflBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} :
getValue? k (k, v :: l) = some v
theorem Std.Internal.List.getValue?_eq_getEntry? {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} :
getValue? a l = Option.map (fun (x : (_ : α) × β) => x.snd) (getEntry? a l)
theorem Std.Internal.List.getValue?_congr {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α} (h : (a == b) = true) :
def Std.Internal.List.getValueCast? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (a : α) :
List ((a : α) × β a)Option (β a)

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.getValueCast?_nil {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} :
theorem Std.Internal.List.getValueCast?_cons {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getValueCast? a (k, v :: l) = if h : (k == a) = true then some (cast v) else getValueCast? a l
theorem Std.Internal.List.getValueCast?_cons_of_true {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) :
getValueCast? a (k, v :: l) = some (cast v)
theorem Std.Internal.List.getValueCast?_cons_of_false {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = false) :
getValueCast? a (k, v :: l) = getValueCast? a l
@[simp]
theorem Std.Internal.List.getValueCast?_cons_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
getValueCast? k (k, v :: l) = some v
theorem Std.Internal.List.getValue?_eq_getValueCast? {α : Type u} [BEq α] [LawfulBEq α] {β : Type v} {l : List ((_ : α) × β)} {a : α} :
theorem Std.Internal.List.getValueCast?_eq_getEntry? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} :
getValueCast? a l = Std.Internal.List.Option.dmap✝ (getEntry? a l) fun (p : (a : α) × β a) (h : getEntry? a l = some p) => cast p.snd
theorem Std.Internal.List.isSome_getValueCast?_eq_isSome_getEntry? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} :
theorem Std.Internal.List.isEmpty_eq_false_iff_exists_isSome_getValueCast? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} :
def Std.Internal.List.containsKey {α : Type u} {β : αType v} [BEq α] (a : α) :
List ((a : α) × β a)Bool

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.containsKey_nil {α : Type u} {β : αType v} [BEq α] {a : α} :
@[simp]
theorem Std.Internal.List.containsKey_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
containsKey a (k, v :: l) = (k == a || containsKey a l)
theorem Std.Internal.List.containsKey_cons_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
containsKey a (k, v :: l) = false (k == a) = false containsKey a l = false
theorem Std.Internal.List.containsKey_cons_eq_true {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
containsKey a (k, v :: l) = true (k == a) = true containsKey a l = true
theorem Std.Internal.List.containsKey_cons_of_beq {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) :
containsKey a (k, v :: l) = true
@[simp]
theorem Std.Internal.List.containsKey_cons_self {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
containsKey k (k, v :: l) = true
theorem Std.Internal.List.containsKey_cons_of_containsKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : containsKey a l = true) :
containsKey a (k, v :: l) = true
theorem Std.Internal.List.containsKey_of_containsKey_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (k, v :: l) = true) (h₂ : (k == a) = false) :
theorem Std.Internal.List.containsKey_eq_isSome_getEntry? {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} :
theorem Std.Internal.List.containsKey_eq_contains_map_fst {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} :
theorem Std.Internal.List.isEmpty_eq_false_of_containsKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
theorem Std.Internal.List.isEmpty_eq_false_iff_exists_containsKey {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.isEmpty_iff_forall_containsKey {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} :
l.isEmpty = true ∀ (a : α), containsKey a l = false
@[simp]
theorem Std.Internal.List.getEntry?_eq_none {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} :
@[simp]
theorem Std.Internal.List.getValue?_eq_none {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} :
theorem Std.Internal.List.containsKey_eq_isSome_getValue? {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} :
theorem Std.Internal.List.containsKey_eq_isSome_getValueCast? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} :
theorem Std.Internal.List.getValueCast?_eq_none {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = false) :
theorem Std.Internal.List.containsKey_congr {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α} (h : (a == b) = true) :
theorem Std.Internal.List.containsKey_of_beq {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α} (hla : containsKey a l = true) (hab : (a == b) = true) :
def Std.Internal.List.getEntry {α : Type u} {β : αType v} [BEq α] (a : α) (l : List ((a : α) × β a)) (h : containsKey a l = true) :
(a : α) × β a

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.getEntry?_eq_some_getEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
getEntry? a l = some (getEntry a l h)
theorem Std.Internal.List.getEntry_eq_of_getEntry?_eq_some {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : getEntry? a l = some k, v) {h' : containsKey a l = true} :
getEntry a l h' = k, v
theorem Std.Internal.List.getEntry_cons_of_beq {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) :
getEntry a (k, v :: l) = k, v
@[simp]
theorem Std.Internal.List.getEntry_cons_self {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
getEntry k (k, v :: l) = k, v
theorem Std.Internal.List.getEntry_cons_of_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h₁ : containsKey a (k, v :: l) = true} (h₂ : (k == a) = false) :
getEntry a (k, v :: l) h₁ = getEntry a l
def Std.Internal.List.getValue {α : Type u} {β : Type v} [BEq α] (a : α) (l : List ((_ : α) × β)) (h : containsKey a l = true) :
β

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.getValue?_eq_some_getValue {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} (h : containsKey a l = true) :
getValue? a l = some (getValue a l h)
theorem Std.Internal.List.getValue_cons_of_beq {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = true) :
getValue a (k, v :: l) = v
@[simp]
theorem Std.Internal.List.getValue_cons_self {α : Type u} {β : Type v} [BEq α] [ReflBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} :
getValue k (k, v :: l) = v
theorem Std.Internal.List.getValue_cons_of_false {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} {h₁ : containsKey a (k, v :: l) = true} (h₂ : (k == a) = false) :
getValue a (k, v :: l) h₁ = getValue a l
theorem Std.Internal.List.getValue_cons {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} {h : containsKey a (k, v :: l) = true} :
getValue a (k, v :: l) h = if h' : (k == a) = true then v else getValue a l
theorem Std.Internal.List.getValue_congr {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α} (hab : (a == b) = true) {h : containsKey a l = true} :
getValue a l h = getValue b l
def Std.Internal.List.getValueCast {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (a : α) (l : List ((a : α) × β a)) (h : containsKey a l = true) :
β a

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.getValueCast?_eq_some_getValueCast {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
theorem Std.Internal.List.Option.get_congr {α : Type u} {o o' : Option α} {ho : o.isSome = true} (h : o = o') :
o.get ho = o'.get
theorem Std.Internal.List.getValueCast_cons {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : containsKey a (k, v :: l) = true) :
getValueCast a (k, v :: l) h = if h' : (k == a) = true then cast v else getValueCast a l
theorem Std.Internal.List.getValue_eq_getValueCast {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] {l : List ((_ : α) × β)} {a : α} {h : containsKey a l = true} :
getValue a l h = getValueCast a l h
def Std.Internal.List.getValueCastD {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (a : α) (l : List ((a : α) × β a)) (fallback : β a) :
β a

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.getValueCastD_nil {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {fallback : β a} :
getValueCastD a [] fallback = fallback
theorem Std.Internal.List.getValueCastD_eq_getValueCast? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {fallback : β a} :
getValueCastD a l fallback = (getValueCast? a l).getD fallback
theorem Std.Internal.List.getValueCastD_eq_fallback {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {fallback : β a} (h : containsKey a l = false) :
getValueCastD a l fallback = fallback
theorem Std.Internal.List.getValueCast_eq_getValueCastD {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {fallback : β a} (h : containsKey a l = true) :
getValueCast a l h = getValueCastD a l fallback
theorem Std.Internal.List.getValueCast?_eq_some_getValueCastD {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {fallback : β a} (h : containsKey a l = true) :
getValueCast? a l = some (getValueCastD a l fallback)
def Std.Internal.List.getValueCast! {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (a : α) [Inhabited (β a)] (l : List ((a : α) × β a)) :
β a

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.getValueCast!_nil {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} [Inhabited (β a)] :
theorem Std.Internal.List.getValueCast!_eq_getValueCast? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] :
theorem Std.Internal.List.getValueCast!_eq_default {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (h : containsKey a l = false) :
theorem Std.Internal.List.getValueCast_eq_getValueCast! {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (h : containsKey a l = true) :
theorem Std.Internal.List.getValueCast?_eq_some_getValueCast! {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (h : containsKey a l = true) :
theorem Std.Internal.List.getValueCast!_eq_getValueCastD_default {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] :
def Std.Internal.List.getValueD {α : Type u} {β : Type v} [BEq α] (a : α) (l : List ((_ : α) × β)) (fallback : β) :
β

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.getValueD_nil {α : Type u} {β : Type v} [BEq α] {a : α} {fallback : β} :
getValueD a [] fallback = fallback
theorem Std.Internal.List.getValueD_eq_getValue? {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} :
getValueD a l fallback = (getValue? a l).getD fallback
theorem Std.Internal.List.getValueD_eq_fallback {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} (h : containsKey a l = false) :
getValueD a l fallback = fallback
theorem Std.Internal.List.getValue_eq_getValueD {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} (h : containsKey a l = true) :
getValue a l h = getValueD a l fallback
theorem Std.Internal.List.getValue?_eq_some_getValueD {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} (h : containsKey a l = true) :
getValue? a l = some (getValueD a l fallback)
theorem Std.Internal.List.getValueD_eq_getValueCastD {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} :
getValueD a l fallback = getValueCastD a l fallback
theorem Std.Internal.List.getValueD_congr {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α} {fallback : β} (hab : (a == b) = true) :
getValueD a l fallback = getValueD b l fallback
def Std.Internal.List.getValue! {α : Type u} {β : Type v} [BEq α] [Inhabited β] (a : α) (l : List ((_ : α) × β)) :
β

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.getValue!_nil {α : Type u} {β : Type v} [BEq α] [Inhabited β] {a : α} :
theorem Std.Internal.List.getValue!_eq_getValue? {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} :
theorem Std.Internal.List.getValue!_eq_default {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} (h : containsKey a l = false) :
theorem Std.Internal.List.getValue_eq_getValue! {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} (h : containsKey a l = true) :
getValue a l h = getValue! a l
theorem Std.Internal.List.getValue?_eq_some_getValue! {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} (h : containsKey a l = true) :
theorem Std.Internal.List.getValue!_eq_getValueCast! {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} :
theorem Std.Internal.List.getValue!_congr {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {a b : α} (hab : (a == b) = true) :
theorem Std.Internal.List.getValue!_eq_getValueD_default {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} :
def Std.Internal.List.getKey? {α : Type u} {β : αType v} [BEq α] (a : α) :
List ((a : α) × β a)Option α

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.getKey?_nil {α : Type u} {β : αType v} [BEq α] {a : α} :
@[simp]
theorem Std.Internal.List.getKey?_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getKey? a (k, v :: l) = bif k == a then some k else getKey? a l
theorem Std.Internal.List.getKey?_cons_of_true {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) :
getKey? a (k, v :: l) = some k
theorem Std.Internal.List.getKey?_cons_of_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = false) :
getKey? a (k, v :: l) = getKey? a l
theorem Std.Internal.List.getKey?_eq_getEntry? {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} :
getKey? a l = Option.map (fun (x : (a : α) × β a) => x.fst) (getEntry? a l)
theorem Std.Internal.List.fst_mem_keys_of_mem {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {a : (a : α) × β a} {l : List ((a : α) × β a)} (hm : a l) :
theorem Std.Internal.List.getKey?_eq_some_iff {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k k' : α} (hd : DistinctKeys l) :
getKey? k l = some k' (k == k') = true k' keys l
theorem Std.Internal.List.getKey?_beq {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} :
Option.all (fun (x : α) => x == a) (getKey? a l) = true
theorem Std.Internal.List.getKey?_congr {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k k' : α} (h : (k == k') = true) :
getKey? k l = getKey? k' l
theorem Std.Internal.List.containsKey_eq_isSome_getKey? {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} :
theorem Std.Internal.List.getEntry?_eq_some_iff_getKey?_eq_some_getValue?_eq_some {α : Type u} [BEq α] {β : Type v} {l : List ((_ : α) × β)} {k k' : α} {v : β} :
getEntry? k l = some k', v getKey? k l = some k' getValue? k l = some v
def Std.Internal.List.getKey {α : Type u} {β : αType v} [BEq α] (a : α) (l : List ((a : α) × β a)) (h : containsKey a l = true) :
α

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.getKey?_eq_some_getKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
getKey? a l = some (getKey a l h)
theorem Std.Internal.List.getKey_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (k, v :: l) = true} :
getKey a (k, v :: l) h = if h' : (k == a) = true then k else getKey a l
theorem Std.Internal.List.getKey_beq {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
(getKey a l h == a) = true
@[simp]
theorem Std.Internal.List.getKey_eq {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
getKey a l h = a
theorem Std.Internal.List.getKey?_eq_some {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
getKey? a l = some a
theorem Std.Internal.List.getKey_congr {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k k' : α} (h : (k == k') = true) {h' : containsKey k l = true} {h'' : containsKey k' l = true} :
getKey k l h' = getKey k' l h''
theorem Std.Internal.List.getKey_eq_getEntry_fst {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {h : containsKey a l = true} :
getKey a l h = (getEntry a l h).fst
def Std.Internal.List.getKeyD {α : Type u} {β : αType v} [BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α) :
α

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.getKeyD_nil {α : Type u} {β : αType v} [BEq α] {a fallback : α} :
getKeyD a [] fallback = fallback
theorem Std.Internal.List.getKeyD_eq_getKey? {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a fallback : α} :
getKeyD a l fallback = (getKey? a l).getD fallback
theorem Std.Internal.List.getKeyD_eq_fallback {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α} (h : containsKey a l = false) :
getKeyD a l fallback = fallback
theorem Std.Internal.List.getKey_eq_getKeyD {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α} (h : containsKey a l = true) :
getKey a l h = getKeyD a l fallback
theorem Std.Internal.List.getKeyD_congr {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k k' fallback : α} (h : (k == k') = true) :
getKeyD k l fallback = getKeyD k' l fallback
theorem Std.Internal.List.getKeyD_eq_of_containsKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k fallback : α} (h : containsKey k l = true) :
getKeyD k l fallback = k
theorem Std.Internal.List.getKey?_eq_some_getKeyD {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α} (h : containsKey a l = true) :
getKey? a l = some (getKeyD a l fallback)
def Std.Internal.List.getKey! {α : Type u} {β : αType v} [BEq α] [Inhabited α] (a : α) (l : List ((a : α) × β a)) :
α

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.getKey!_nil {α : Type u} {β : αType v} [BEq α] [Inhabited α] {a : α} :
theorem Std.Internal.List.getKey!_eq_getKey? {α : Type u} {β : αType v} [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} :
getKey! a l = (getKey? a l).get!
theorem Std.Internal.List.getKey!_eq_default {α : Type u} {β : αType v} [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = false) :
theorem Std.Internal.List.getKey_eq_getKey! {α : Type u} {β : αType v} [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
getKey a l h = getKey! a l
theorem Std.Internal.List.getKey!_congr {α : Type u} {β : αType v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {k k' : α} (h : (k == k') = true) :
getKey! k l = getKey! k' l
theorem Std.Internal.List.getKey!_eq_of_containsKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (h : containsKey k l = true) :
getKey! k l = k
theorem Std.Internal.List.getKey?_eq_some_getKey! {α : Type u} {β : αType v} [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
getKey? a l = some (getKey! a l)
theorem Std.Internal.List.getKey!_eq_getKeyD_default {α : Type u} {β : αType v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} :
theorem Std.Internal.List.getEntry?_eq_getValueCast? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} :
getEntry? a l = Option.map (fun (v : β a) => a, v) (getValueCast? a l)
theorem Std.Internal.List.getEntry_eq_getKey_getValue {α : Type u} [BEq α] {β : Type v} {l : List ((_ : α) × β)} {a : α} (h : containsKey a l = true) :
getEntry a l h = getKey a l h, getValue a l h
def Std.Internal.List.replaceEntry {α : Type u} {β : αType v} [BEq α] (k : α) (v : β k) :
List ((a : α) × β a)List ((a : α) × β a)

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.replaceEntry_nil {α : Type u} {β : αType v} [BEq α] {k : α} {v : β k} :
theorem Std.Internal.List.replaceEntry_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} :
replaceEntry k v (k', v' :: l) = bif k' == k then k, v :: l else k', v' :: replaceEntry k v l
theorem Std.Internal.List.replaceEntry_cons_of_true {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} (h : (k' == k) = true) :
replaceEntry k v (k', v' :: l) = k, v :: l
theorem Std.Internal.List.replaceEntry_cons_of_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} (h : (k' == k) = false) :
replaceEntry k v (k', v' :: l) = k', v' :: replaceEntry k v l
theorem Std.Internal.List.replaceEntry_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = false) :
replaceEntry k v l = l
@[simp]
theorem Std.Internal.List.isEmpty_replaceEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.mem_replaceEntry_of_beq_eq_false {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : (p.fst == a) = false) :
p replaceEntry a b l p l
theorem Std.Internal.List.mem_replaceEntry_of_key_ne {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.fst a) :
p replaceEntry a b l p l
theorem Std.Internal.List.getEntry?_replaceEntry_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} (hl : containsKey k l = false) :
theorem Std.Internal.List.getEntry?_replaceEntry_of_false {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} (h : (k == a) = false) :
theorem Std.Internal.List.getEntry?_replaceEntry_of_true {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} (hl : containsKey k l = true) (h : (k == a) = true) :
getEntry? a (replaceEntry k v l) = some k, v
theorem Std.Internal.List.getEntry?_replaceEntry {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} :
getEntry? a (replaceEntry k v l) = if containsKey k l = true (k == a) = true then some k, v else getEntry? a l
@[simp]
theorem Std.Internal.List.containsKey_replaceEntry {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} :
theorem Std.Internal.List.getEntry_replaceEntry_of_true {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} (hl : containsKey a (replaceEntry k v l) = true) (h : (k == a) = true) :
getEntry a (replaceEntry k v l) hl = k, v
theorem Std.Internal.List.mem_getEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} (hl : containsKey k l = true) :
getEntry k l hl l
theorem Std.Internal.List.mem_replaceEntry_of_true {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (hl : containsKey k l = true) :
k, v replaceEntry k v l
@[simp]
theorem Std.Internal.List.length_replaceEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.getValue?_replaceEntry_of_containsKey_eq_false {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (hl : containsKey k l = false) :
theorem Std.Internal.List.getValue?_replaceEntry_of_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = false) :
theorem Std.Internal.List.getValue?_replaceEntry_of_true {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (hl : containsKey k l = true) (h : (k == a) = true) :
theorem Std.Internal.List.getValueCast?_replaceEntry {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} :
getValueCast? a (replaceEntry k v l) = if h : containsKey k l = true (k == a) = true then some (cast v) else getValueCast? a l
theorem Std.Internal.List.getKey?_replaceEntry {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} :
def Std.Internal.List.eraseKey {α : Type u} {β : αType v} [BEq α] (k : α) :
List ((a : α) × β a)List ((a : α) × β a)

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.eraseKey_nil {α : Type u} {β : αType v} [BEq α] {k : α} :
theorem Std.Internal.List.eraseKey_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'} :
eraseKey k (k', v' :: l) = bif k' == k then l else k', v' :: eraseKey k l
theorem Std.Internal.List.eraseKey_cons_of_beq {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'} (h : (k' == k) = true) :
eraseKey k (k', v' :: l) = l
@[simp]
theorem Std.Internal.List.eraseKey_cons_self {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
eraseKey k (k, v :: l) = l
theorem Std.Internal.List.eraseKey_cons_of_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'} (h : (k' == k) = false) :
eraseKey k (k', v' :: l) = k', v' :: eraseKey k l
theorem Std.Internal.List.eraseKey_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} (h : containsKey k l = false) :
eraseKey k l = l
theorem Std.Internal.List.mem_eraseKey_of_key_beq_eq_false {α : Type u} {β : αType v} [BEq α] {a : α} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : (p.fst == a) = false) :
p eraseKey a l p l
theorem Std.Internal.List.mem_eraseKey_of_key_ne {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.fst a) :
p eraseKey a l p l
theorem Std.Internal.List.sublist_eraseKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} :
theorem Std.Internal.List.length_eraseKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} :
theorem Std.Internal.List.length_eraseKey_le {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} :
theorem Std.Internal.List.length_le_length_eraseKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} :
theorem Std.Internal.List.isEmpty_eraseKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} :
@[simp]
theorem Std.Internal.List.keys_nil {α : Type u} {β : αType v} :
@[simp]
theorem Std.Internal.List.keys_cons {α : Type u} {β : αType v} {l : List ((a : α) × β a)} {k : α} {v : β k} :
keys (k, v :: l) = k :: keys l
theorem Std.Internal.List.length_keys_eq_length {α : Type u} {β : αType v} (l : List ((a : α) × β a)) :
theorem Std.Internal.List.isEmpty_keys_eq_isEmpty {α : Type u} {β : αType v} (l : List ((a : α) × β a)) :
theorem Std.Internal.List.containsKey_eq_keys_contains {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :
theorem Std.Internal.List.containsKey_eq_true_iff_exists_mem {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} :
containsKey a l = true (p : (a : α) × β a), p l (p.fst == a) = true
theorem Std.Internal.List.containsKey_of_mem {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a} (hp : p l) :
@[simp]
theorem Std.Internal.List.DistinctKeys.nil {α : Type u} {β : αType v} [BEq α] :
theorem Std.Internal.List.DistinctKeys.def {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} :
DistinctKeys l List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l
theorem Std.Internal.List.DistinctKeys.perm_keys {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} (h : (keys l').Perm (keys l)) :
theorem Std.Internal.List.DistinctKeys.perm {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} (h : l'.Perm l) :
theorem Std.Internal.List.DistinctKeys.congr {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} (h : l.Perm l') :
theorem Std.Internal.List.distinctKeys_of_sublist_keys {α : Type u} {β : αType v} {γ : αType w} [BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × γ a)} (h : (keys l').Sublist (keys l)) :
theorem Std.Internal.List.distinctKeys_of_sublist {α : Type u} {β : αType v} [BEq α] {l l' : List ((a : α) × β a)} (h : l'.Sublist l) :
theorem Std.Internal.List.DistinctKeys.of_keys_eq {α : Type u} {β : αType v} {γ : αType w} [BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × γ a)} (h : keys l = keys l') :
theorem Std.Internal.List.containsKey_iff_exists {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :
containsKey a l = true (a' : α), a' keys l (a == a') = true
theorem Std.Internal.List.containsKey_eq_false_iff_forall_mem_keys {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :
containsKey a l = false ∀ (a' : α), a' keys l → (a == a') = false
theorem Std.Internal.List.containsKey_eq_false_iff {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :
containsKey a l = false ∀ (b : (a : α) × β a), b l → (a == b.fst) = false
@[simp]
theorem Std.Internal.List.distinctKeys_cons_iff {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.DistinctKeys.tail {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
DistinctKeys (k, v :: l)DistinctKeys l
theorem Std.Internal.List.DistinctKeys.containsKey_eq_false {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
DistinctKeys (k, v :: l)containsKey k l = false
theorem Std.Internal.List.DistinctKeys.cons {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = false) :
DistinctKeys lDistinctKeys (k, v :: l)
theorem Std.Internal.List.DistinctKeys.replaceEntry {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : DistinctKeys l) :
theorem Std.Internal.List.getEntry?_of_mem {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} (hl : DistinctKeys l) {k k' : α} (hk : (k == k') = true) {v : β k} (hkv : k, v l) :
getEntry? k' l = some k, v
def Std.Internal.List.insertEntry {α : Type u} {β : αType v} [BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)) :
List ((a : α) × β a)

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.Internal.List.insertEntry_nil {α : Type u} {β : αType v} [BEq α] {k : α} {v : β k} :
insertEntry k v [] = [k, v]
theorem Std.Internal.List.insertEntry_cons_of_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} (h : (k' == k) = false) :
(insertEntry k v (k', v' :: l)).Perm (k', v' :: insertEntry k v l)
theorem Std.Internal.List.insertEntry_cons_of_beq {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} (h : (k' == k) = true) :
insertEntry k v (k', v' :: l) = k, v :: l
@[simp]
theorem Std.Internal.List.insertEntry_cons_self {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
insertEntry k v (k, v :: l) = k, v :: l
theorem Std.Internal.List.insertEntry_of_containsKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = true) :
theorem Std.Internal.List.insertEntry_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = false) :
insertEntry k v l = k, v :: l
theorem Std.Internal.List.mem_insertEntry_of_key_beq_eq_false {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : (p.fst == a) = false) :
p insertEntry a b l p l
theorem Std.Internal.List.mem_insertEntry_of_key_ne {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.fst a) :
p insertEntry a b l p l
theorem Std.Internal.List.DistinctKeys.insertEntry {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : DistinctKeys l) :
@[simp]
theorem Std.Internal.List.isEmpty_insertEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.length_insertEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.length_le_length_insertEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.length_insertEntry_le {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.getValue?_insertEntry_of_beq {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = true) :
theorem Std.Internal.List.getValue?_insertEntry_of_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} :
theorem Std.Internal.List.getValue?_insertEntry_of_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = false) :
theorem Std.Internal.List.getValue?_insertEntry {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} :
theorem Std.Internal.List.getValue?_insertEntry_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} :
theorem Std.Internal.List.getEntry?_insertEntry {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getEntry? a (insertEntry k v l) = if (k == a) = true then some k, v else getEntry? a l
theorem Std.Internal.List.getValueCast?_insertEntry {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getValueCast? a (insertEntry k v l) = if h : (k == a) = true then some (cast v) else getValueCast? a l
theorem Std.Internal.List.getValueCast?_insertEntry_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.getValueCast!_insertEntry {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} [Inhabited (β a)] {v : β k} :
getValueCast! a (insertEntry k v l) = if h : (k == a) = true then cast v else getValueCast! a l
theorem Std.Internal.List.getValueCast!_insertEntry_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] {v : β k} :
theorem Std.Internal.List.getValueCastD_insertEntry {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {fallback : β a} {v : β k} :
getValueCastD a (insertEntry k v l) fallback = if h : (k == a) = true then cast v else getValueCastD a l fallback
theorem Std.Internal.List.getValueCastD_insertEntry_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback v : β k} :
getValueCastD k (insertEntry k v l) fallback = v
theorem Std.Internal.List.getValue!_insertEntry {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k a : α} {v : β} :
theorem Std.Internal.List.getValue!_insertEntry_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k : α} {v : β} :
getValue! k (insertEntry k v l) = v
theorem Std.Internal.List.getValueD_insertEntry {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {fallback v : β} :
getValueD a (insertEntry k v l) fallback = if (k == a) = true then v else getValueD a l fallback
theorem Std.Internal.List.getValueD_insertEntry_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {fallback v : β} :
getValueD k (insertEntry k v l) fallback = v
theorem Std.Internal.List.getKey?_insertEntry {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getKey? a (insertEntry k v l) = if (k == a) = true then some k else getKey? a l
theorem Std.Internal.List.getKey?_insertEntry_self {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.getKey?_eq_none {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = false) :
theorem Std.Internal.List.getKey!_insertEntry {α : Type u} {β : αType v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getKey! a (insertEntry k v l) = if (k == a) = true then k else getKey! a l
theorem Std.Internal.List.getKey!_insertEntry_self {α : Type u} {β : αType v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
getKey! k (insertEntry k v l) = k
theorem Std.Internal.List.getKeyD_insertEntry {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α} {v : β k} :
getKeyD a (insertEntry k v l) fallback = if (k == a) = true then k else getKeyD a l fallback
theorem Std.Internal.List.getKeyD_insertEntry_self {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k fallback : α} {v : β k} :
getKeyD k (insertEntry k v l) fallback = k
theorem Std.Internal.List.containsKey_insertEntry {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
theorem Std.Internal.List.containsKey_insertEntry_of_beq {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) :
theorem Std.Internal.List.containsKey_insertEntry_self {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.containsKey_of_containsKey_insertEntry {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntry k v l) = true) (h₂ : (k == a) = false) :
theorem Std.Internal.List.getValueCast_insertEntry {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (insertEntry k v l) = true} :
getValueCast a (insertEntry k v l) h = if h' : (k == a) = true then cast v else getValueCast a l
theorem Std.Internal.List.getValueCast_insertEntry_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
getValueCast k (insertEntry k v l) = v
theorem Std.Internal.List.getValue_insertEntry {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} {h : containsKey a (insertEntry k v l) = true} :
getValue a (insertEntry k v l) h = if h' : (k == a) = true then v else getValue a l
theorem Std.Internal.List.getValue_insertEntry_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} :
getValue k (insertEntry k v l) = v
theorem Std.Internal.List.getKey_insertEntry {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (insertEntry k v l) = true} :
getKey a (insertEntry k v l) h = if h' : (k == a) = true then k else getKey a l
theorem Std.Internal.List.getKey_insertEntry_self {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
getKey k (insertEntry k v l) = k
def Std.Internal.List.insertEntryIfNew {α : Type u} {β : αType v} [BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)) :
List ((a : α) × β a)

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.insertEntryIfNew_of_containsKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = true) :
theorem Std.Internal.List.insertEntryIfNew_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = false) :
insertEntryIfNew k v l = k, v :: l
theorem Std.Internal.List.DistinctKeys.insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {k : α} {v : β k} {l : List ((a : α) × β a)} (h : DistinctKeys l) :
@[simp]
theorem Std.Internal.List.isEmpty_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.getEntry?_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getEntry? a (insertEntryIfNew k v l) = if (k == a && !containsKey k l) = true then some k, v else getEntry? a l
theorem Std.Internal.List.getValueCast?_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
getValueCast? a (insertEntryIfNew k v l) = if h : (k == a) = true containsKey k l = false then some (cast v) else getValueCast? a l
theorem Std.Internal.List.getValue?_insertEntryIfNew {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} :
theorem Std.Internal.List.containsKey_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
theorem Std.Internal.List.containsKey_insertEntryIfNew_self {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.containsKey_of_containsKey_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntryIfNew k v l) = true) (h₂ : (k == a) = false) :
theorem Std.Internal.List.containsKey_of_containsKey_insertEntryIfNew' {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntryIfNew k v l) = true) (h₂ : ¬((k == a) = true containsKey k l = false)) :

This is a restatement of containsKey_insertEntryIfNew that is written to exactly match the proof obligation in the statement of getValueCast_insertEntryIfNew.

theorem Std.Internal.List.getValueCast_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (insertEntryIfNew k v l) = true} :
getValueCast a (insertEntryIfNew k v l) h = if h' : (k == a) = true containsKey k l = false then cast v else getValueCast a l
theorem Std.Internal.List.getValue_insertEntryIfNew {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} {h : containsKey a (insertEntryIfNew k v l) = true} :
getValue a (insertEntryIfNew k v l) h = if h' : (k == a) = true containsKey k l = false then v else getValue a l
theorem Std.Internal.List.getValueCast!_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} [Inhabited (β a)] :
getValueCast! a (insertEntryIfNew k v l) = if h : (k == a) = true containsKey k l = false then cast v else getValueCast! a l
theorem Std.Internal.List.getValue!_insertEntryIfNew {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k a : α} {v : β} :
theorem Std.Internal.List.getValueCastD_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {fallback : β a} :
getValueCastD a (insertEntryIfNew k v l) fallback = if h : (k == a) = true containsKey k l = false then cast v else getValueCastD a l fallback
theorem Std.Internal.List.getValueD_insertEntryIfNew {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {fallback v : β} :
getValueD a (insertEntryIfNew k v l) fallback = if (k == a) = true containsKey k l = false then v else getValueD a l fallback
theorem Std.Internal.List.getKey?_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
theorem Std.Internal.List.getKey_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (insertEntryIfNew k v l) = true} :
getKey a (insertEntryIfNew k v l) h = if h' : (k == a) = true containsKey k l = false then k else getKey a l
theorem Std.Internal.List.getKey!_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
theorem Std.Internal.List.getKeyD_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α} {v : β k} :
getKeyD a (insertEntryIfNew k v l) fallback = if (k == a) = true containsKey k l = false then k else getKeyD a l fallback
theorem Std.Internal.List.length_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.length_le_length_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.length_insertEntryIfNew_le {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
@[simp]
theorem Std.Internal.List.keys_eraseKey {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} :
keys (eraseKey k l) = (keys l).erase k
theorem Std.Internal.List.DistinctKeys.eraseKey {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} :
theorem Std.Internal.List.getEntry?_eraseKey_self {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} (h : DistinctKeys l) :
theorem Std.Internal.List.getEntry?_eraseKey_of_beq {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) (hka : (k == a) = true) :
theorem Std.Internal.List.getEntry?_eraseKey_of_false {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hka : (k == a) = false) :
theorem Std.Internal.List.getEntry?_eraseKey {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.keys_filterMap {α : Type u} {β : αType v} {γ : αType w} [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β aOption (γ a)} :
keys (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => p.fst, x) (f p.fst p.snd)) l) = keys (List.filter (fun (p : (a : α) × β a) => (f p.fst p.snd).isSome) l)
@[simp]
theorem Std.Internal.List.keys_map {α : Type u} {β : αType v} {γ : αType w} [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β aγ a} :
keys (List.map (fun (p : (a : α) × β a) => p.fst, f p.fst p.snd) l) = keys l
theorem Std.Internal.List.DistinctKeys.filterMap {α : Type u} {β : αType v} {γ : αType w} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {f : (a : α) → β aOption (γ a)} :
DistinctKeys lDistinctKeys (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => p.fst, x) (f p.fst p.snd)) l)
theorem Std.Internal.List.DistinctKeys.map {α : Type u} {β : αType v} {γ : αType w} [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β aγ a} (h : DistinctKeys l) :
DistinctKeys (List.map (fun (p : (a : α) × β a) => p.fst, f p.fst p.snd) l)
theorem Std.Internal.List.DistinctKeys.filter {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β aBool} (h : DistinctKeys l) :
DistinctKeys (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l)
theorem Std.Internal.List.getValue?_eraseKey_self {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} (h : DistinctKeys l) :
theorem Std.Internal.List.getValue?_eraseKey_of_beq {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) (hka : (k == a) = true) :
theorem Std.Internal.List.getValue?_eraseKey_of_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} (hka : (k == a) = false) :
theorem Std.Internal.List.getValue?_eraseKey {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey?_eraseKey {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey?_eraseKey_self {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey!_eraseKey {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey!_eraseKey_self {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKeyD_eraseKey {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α} (hl : DistinctKeys l) :
getKeyD a (eraseKey k l) fallback = if (k == a) = true then fallback else getKeyD a l fallback
theorem Std.Internal.List.getKeyD_eraseKey_self {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k fallback : α} (hl : DistinctKeys l) :
getKeyD k (eraseKey k l) fallback = fallback
theorem Std.Internal.List.containsKey_eraseKey_self {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} (h : DistinctKeys l) :
theorem Std.Internal.List.containsKey_eraseKey_of_beq {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) (hka : (a == k) = true) :
theorem Std.Internal.List.containsKey_eraseKey_of_false {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hka : (k == a) = false) :
theorem Std.Internal.List.containsKey_eraseKey {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.isEmpty_eq_isEmpty_eraseKey_and_not_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (k : α) :
theorem Std.Internal.List.isEmpty_eq_false_of_isEmpty_eraseKey_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) :
theorem Std.Internal.List.getValueCast?_eraseKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCast?_eraseKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCast!_eraseKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} [Inhabited (β a)] (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCast!_eraseKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCastD_eraseKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {fallback : β a} (hl : DistinctKeys l) :
getValueCastD a (eraseKey k l) fallback = if (k == a) = true then fallback else getValueCastD a l fallback
theorem Std.Internal.List.getValueCastD_eraseKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (hl : DistinctKeys l) :
getValueCastD k (eraseKey k l) fallback = fallback
theorem Std.Internal.List.getValue!_eraseKey {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValue!_eraseKey_self {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueD_eraseKey {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {fallback : β} (hl : DistinctKeys l) :
getValueD a (eraseKey k l) fallback = if (k == a) = true then fallback else getValueD a l fallback
theorem Std.Internal.List.getValueD_eraseKey_self {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} {fallback : β} (hl : DistinctKeys l) :
getValueD k (eraseKey k l) fallback = fallback
theorem Std.Internal.List.containsKey_of_containsKey_eraseKey {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCast_eraseKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {h : containsKey a (eraseKey k l) = true} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValue_eraseKey {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {h : containsKey a (eraseKey k l) = true} (hl : DistinctKeys l) :
getValue a (eraseKey k l) h = getValue a l
theorem Std.Internal.List.getKey_eraseKey {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a : α} {h : containsKey a (eraseKey k l) = true} (hl : DistinctKeys l) :
getKey a (eraseKey k l) h = getKey a l
theorem Std.Internal.List.getEntry?_of_perm {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.containsKey_of_perm {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {k : α} (h : l.Perm l') :
theorem Std.Internal.List.getValueCast?_of_perm {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getValueCast_of_perm {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} {h' : containsKey a l = true} (hl : DistinctKeys l) (h : l.Perm l') :
getValueCast a l h' = getValueCast a l'
theorem Std.Internal.List.getValueCast!_of_perm {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getValueCastD_of_perm {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} {fallback : β a} (hl : DistinctKeys l) (h : l.Perm l') :
getValueCastD a l fallback = getValueCastD a l' fallback
theorem Std.Internal.List.getValue?_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getValue_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α} {h' : containsKey a l = true} (hl : DistinctKeys l) (h : l.Perm l') :
getValue a l h' = getValue a l'
theorem Std.Internal.List.getValue!_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l l' : List ((_ : α) × β)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getValueD_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α} {fallback : β} (hl : DistinctKeys l) (h : l.Perm l') :
getValueD a l fallback = getValueD a l' fallback
theorem Std.Internal.List.getKey?_of_perm {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') :
getKey? a l = getKey? a l'
theorem Std.Internal.List.getKey_of_perm {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} {h' : containsKey a l = true} (hl : DistinctKeys l) (h : l.Perm l') :
getKey a l h' = getKey a l'
theorem Std.Internal.List.getKey!_of_perm {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] [Inhabited α] {l l' : List ((a : α) × β a)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') :
getKey! a l = getKey! a l'
theorem Std.Internal.List.getKeyD_of_perm {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a fallback : α} (hl : DistinctKeys l) (h : l.Perm l') :
getKeyD a l fallback = getKeyD a l' fallback
theorem Std.Internal.List.perm_cons_getEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
(l' : List ((a : α) × β a)), l.Perm (getEntry a l h :: l')
theorem Std.Internal.List.getEntry?_ext {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hl' : DistinctKeys l') (h : ∀ (a : α), getEntry? a l = getEntry? a l') :
l.Perm l'
theorem Std.Internal.List.getValueCast?_ext {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hl' : DistinctKeys l') (h : ∀ (a : α), getValueCast? a l = getValueCast? a l') :
l.Perm l'
theorem Std.Internal.List.getKey?_getValue?_ext {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {l l' : List ((_ : α) × β)} (hl : DistinctKeys l) (hl' : DistinctKeys l') (hk : ∀ (a : α), getKey? a l = getKey? a l') (hv : ∀ (a : α), getValue? a l = getValue? a l') :
l.Perm l'
theorem Std.Internal.List.getKey?_ext {α : Type u} [BEq α] [EquivBEq α] {l l' : List ((_ : α) × Unit)} (hl : DistinctKeys l) (hl' : DistinctKeys l') (h : ∀ (a : α), getKey? a l = getKey? a l') :
l.Perm l'
theorem Std.Internal.List.containsKey_ext {α : Type u} [BEq α] [LawfulBEq α] {l l' : List ((_ : α) × Unit)} (hl : DistinctKeys l) (hl' : DistinctKeys l') (h : ∀ (a : α), containsKey a l = containsKey a l') :
l.Perm l'
theorem Std.Internal.List.replaceEntry_of_perm {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k} (hl : DistinctKeys l) (h : l.Perm l') :
(replaceEntry k v l).Perm (replaceEntry k v l')
theorem Std.Internal.List.insertEntry_of_perm {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k} (hl : DistinctKeys l) (h : l.Perm l') :
(insertEntry k v l).Perm (insertEntry k v l')
theorem Std.Internal.List.insertEntryIfNew_of_perm {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.eraseKey_of_perm {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) (h : l.Perm l') :
(eraseKey k l).Perm (eraseKey k l')
@[simp]
theorem Std.Internal.List.getEntry?_append {α : Type u} {β : αType v} [BEq α] {l l' : List ((a : α) × β a)} {a : α} :
getEntry? a (l ++ l') = (getEntry? a l).or (getEntry? a l')
theorem Std.Internal.List.getEntry?_append_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] {l l' : List ((a : α) × β a)} {a : α} (h : containsKey a l' = false) :
getEntry? a (l ++ l') = getEntry? a l
@[simp]
theorem Std.Internal.List.containsKey_append {α : Type u} {β : αType v} [BEq α] {l l' : List ((a : α) × β a)} {a : α} :
theorem Std.Internal.List.containsKey_flatMap_eq_false {α : Type u} {β : αType v} [BEq α] {γ : Type w} {l : List γ} {f : γList ((a : α) × β a)} {a : α} (h : ∀ (i : Nat) (h : i < l.length), containsKey a (f l[i]) = false) :
theorem Std.Internal.List.containsKey_append_of_not_contains_right {α : Type u} {β : αType v} [BEq α] {l l' : List ((a : α) × β a)} {a : α} (hl' : containsKey a l' = false) :
@[simp]
theorem Std.Internal.List.getValue?_append {α : Type u} {β : Type v} [BEq α] {l l' : List ((_ : α) × β)} {a : α} :
getValue? a (l ++ l') = (getValue? a l).or (getValue? a l')
theorem Std.Internal.List.getValue?_append_of_containsKey_eq_false {α : Type u} {β : Type v} [BEq α] {l l' : List ((_ : α) × β)} {a : α} (h : containsKey a l' = false) :
getValue? a (l ++ l') = getValue? a l
theorem Std.Internal.List.getValue_append_of_containsKey_eq_false {α : Type u} {β : Type v} [BEq α] {l l' : List ((_ : α) × β)} {a : α} {h' : containsKey a (l ++ l') = true} (h : containsKey a l' = false) :
getValue a (l ++ l') h' = getValue a l
theorem Std.Internal.List.getValueCast?_append_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl' : containsKey a l' = false) :
theorem Std.Internal.List.getValueCast_append_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a (l ++ l') = true} (hl' : containsKey a l' = false) :
getValueCast a (l ++ l') h = getValueCast a l
theorem Std.Internal.List.getKey?_append_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl' : containsKey a l' = false) :
getKey? a (l ++ l') = getKey? a l
theorem Std.Internal.List.getKey_append_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a (l ++ l') = true} (hl' : containsKey a l' = false) :
getKey a (l ++ l') h = getKey a l
theorem Std.Internal.List.replaceEntry_append_of_containsKey_left {α : Type u} {β : αType v} [BEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = true) :
replaceEntry k v (l ++ l') = replaceEntry k v l ++ l'
theorem Std.Internal.List.replaceEntry_append_of_containsKey_left_eq_false {α : Type u} {β : αType v} [BEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = false) :
replaceEntry k v (l ++ l') = l ++ replaceEntry k v l'
theorem Std.Internal.List.replaceEntry_append_of_containsKey_right_eq_false {α : Type u} {β : αType v} [BEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l' = false) :
replaceEntry k v (l ++ l') = replaceEntry k v l ++ l'
theorem Std.Internal.List.insertEntry_append_of_not_contains_right {α : Type u} {β : αType v} [BEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k} (h' : containsKey k l' = false) :
insertEntry k v (l ++ l') = insertEntry k v l ++ l'
theorem Std.Internal.List.eraseKey_append_of_containsKey_right_eq_false {α : Type u} {β : αType v} [BEq α] {l l' : List ((a : α) × β a)} {k : α} (h : containsKey k l' = false) :
eraseKey k (l ++ l') = eraseKey k l ++ l'
theorem Std.Internal.List.mem_iff_getValueCast?_eq_some {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} {v : β k} {l : List ((a : α) × β a)} (h : DistinctKeys l) :
k, v l getValueCast? k l = some v
theorem Std.Internal.List.find?_eq_some_iff_getValueCast?_eq_some {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : DistinctKeys l) :
List.find? (fun (x : (a : α) × β a) => x.fst == k) l = some k, v getValueCast? k l = some v
theorem Std.Internal.List.find?_eq_none_iff_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} :
List.find? (fun (x : (a : α) × β a) => x.fst == k) l = none containsKey k l = false
theorem Std.Internal.List.pairwise_fst_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} (h : DistinctKeys l) :
List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l
theorem Std.Internal.List.map_fst_map_toProd_eq_keys {α : Type u} {β : Type v} {l : List ((_ : α) × β)} :
List.map Prod.fst (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l) = keys l
theorem Std.Internal.List.find?_map_eq_none_iff_containsKey_eq_false {α : Type u} [BEq α] [PartialEquivBEq α] {β : Type v} {l : List ((_ : α) × β)} {k : α} :
List.find? (fun (x : α × β) => x.fst == k) (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l) = none containsKey k l = false
theorem Std.Internal.List.mem_map_toProd_iff_mem {α : Type u} {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} :
k, v l (k, v) List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l
theorem Std.Internal.List.mem_iff_getValue?_eq_some {α : Type u} [BEq α] [LawfulBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) :
k, v l getValue? k l = some v
theorem Std.Internal.List.mem_map_toProd_iff_getValue?_eq_some {α : Type u} [BEq α] [LawfulBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) :
(k, v) List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l getValue? k l = some v
theorem Std.Internal.List.find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {k k' : α} {v : β} {l : List ((_ : α) × β)} :
List.find? (fun (a : α × β) => a.fst == k) (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l) = some (k', v) getKey? k l = some k' getValue? k l = some v
theorem Std.Internal.List.mem_iff_getKey?_eq_some_and_getValue?_eq_some {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) :
k, v l getKey? k l = some k getValue? k l = some v
theorem Std.Internal.List.getValue?_eq_some_iff_exists_beq_and_mem_toList {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} (h : DistinctKeys l) :
getValue? k l = some v (k' : α), (k == k') = true (k', v) List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l
theorem Std.Internal.List.mem_map_toProd_iff_getKey?_eq_some_and_getValue?_eq_some {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) :
(k, v) List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l getKey? k l = some k getValue? k l = some v
theorem Std.Internal.List.pairwise_fst_eq_false_map_toProd {α : Type u} [BEq α] {β : Type v} {l : List ((_ : α) × β)} (h : DistinctKeys l) :
List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)
theorem Std.Internal.List.foldlM_eq_foldlM_toProd {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × β)} {f : δαβm' δ} {init : δ} :
List.foldlM (fun (a : δ) (b : (_ : α) × β) => f a b.fst b.snd) init l = List.foldlM (fun (a : δ) (b : α × β) => f a b.fst b.snd) init (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)
theorem Std.Internal.List.foldl_eq_foldl_toProd {α : Type u} {β : Type v} {δ : Type w} {l : List ((_ : α) × β)} {f : δαβδ} {init : δ} :
List.foldl (fun (a : δ) (b : (_ : α) × β) => f a b.fst b.snd) init l = List.foldl (fun (a : δ) (b : α × β) => f a b.fst b.snd) init (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)
theorem Std.Internal.List.foldrM_eq_foldrM_toProd {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × β)} {f : αβδm' δ} {init : δ} :
List.foldrM (fun (a : (_ : α) × β) (b : δ) => f a.fst a.snd b) init l = List.foldrM (fun (a : α × β) (b : δ) => f a.fst a.snd b) init (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)
theorem Std.Internal.List.foldrM_eq_foldrM_toProd' {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × β)} {f : δαβm' δ} {init : δ} :
List.foldrM (fun (a : (_ : α) × β) (b : δ) => f b a.fst a.snd) init l = List.foldrM (fun (a : α × β) (b : δ) => f b a.fst a.snd) init (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)
theorem Std.Internal.List.foldr_eq_foldr_toProd {α : Type u} {β : Type v} {δ : Type w} {l : List ((_ : α) × β)} {f : αβδδ} {init : δ} :
List.foldr (fun (a : (_ : α) × β) (b : δ) => f a.fst a.snd b) init l = List.foldr (fun (a : α × β) (b : δ) => f a.fst a.snd b) init (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)
theorem Std.Internal.List.foldr_eq_foldr_toProd' {α : Type u} {β : Type v} {δ : Type w} {l : List ((_ : α) × β)} {f : δαβδ} {init : δ} :
List.foldr (fun (a : (_ : α) × β) (b : δ) => f b a.fst a.snd) init l = List.foldr (fun (a : α × β) (b : δ) => f b a.fst a.snd) init (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)
theorem Std.Internal.List.forM_eq_forM_toProd {α : Type u} {β : Type v} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × β)} {f : αβm' PUnit} :
(forM l fun (a : (_ : α) × β) => f a.fst a.snd) = forM (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l) fun (a : α × β) => f a.fst a.snd
theorem Std.Internal.List.forIn_eq_forIn_toProd {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × β)} {f : αβδm' (ForInStep δ)} {init : δ} :
(forIn l init fun (a : (_ : α) × β) (d : δ) => f a.fst a.snd d) = forIn (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l) init fun (a : α × β) (d : δ) => f a.fst a.snd d
theorem Std.Internal.List.foldlM_eq_foldlM_keys {α : Type u} {β : αType v} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((a : α) × β a)} {f : δαm' δ} {init : δ} :
List.foldlM (fun (a : δ) (b : (a : α) × β a) => f a b.fst) init l = List.foldlM f init (keys l)
theorem Std.Internal.List.foldl_eq_foldl_keys {α : Type u} {β : αType v} {δ : Type w} {l : List ((a : α) × β a)} {f : δαδ} {init : δ} :
List.foldl (fun (a : δ) (b : (a : α) × β a) => f a b.fst) init l = List.foldl f init (keys l)
theorem Std.Internal.List.foldrM_eq_foldrM_keys {α : Type u} {β : αType v} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((a : α) × β a)} {f : αδm' δ} {init : δ} :
List.foldrM (fun (a : (a : α) × β a) (b : δ) => f a.fst b) init l = List.foldrM f init (keys l)
theorem Std.Internal.List.foldrM_eq_foldrM_keys' {α : Type u} {β : αType v} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((a : α) × β a)} {f : δαm' δ} {init : δ} :
List.foldrM (fun (a : (a : α) × β a) (b : δ) => f b a.fst) init l = List.foldrM (fun (a : α) (b : δ) => f b a) init (keys l)
theorem Std.Internal.List.foldr_eq_foldr_keys {α : Type u} {β : αType v} {δ : Type w} {l : List ((a : α) × β a)} {f : αδδ} {init : δ} :
List.foldr (fun (a : (a : α) × β a) (b : δ) => f a.fst b) init l = List.foldr f init (keys l)
theorem Std.Internal.List.foldr_eq_foldr_keys' {α : Type u} {β : αType v} {δ : Type w} {l : List ((a : α) × β a)} {f : δαδ} {init : δ} :
List.foldr (fun (a : (a : α) × β a) (b : δ) => f b a.fst) init l = List.foldr (fun (a : α) (b : δ) => f b a) init (keys l)
theorem Std.Internal.List.forM_eq_forM_keys {α : Type u} {β : αType v} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((a : α) × β a)} {f : αm' PUnit} :
(l.forM fun (a : (a : α) × β a) => f a.fst) = (keys l).forM f
theorem Std.Internal.List.forIn_eq_forIn_keys {α : Type u} {β : αType v} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {f : αδm' (ForInStep δ)} {init : δ} {l : List ((a : α) × β a)} :
(forIn l init fun (a : (a : α) × β a) (d : δ) => f a.fst d) = forIn (keys l) init f
def Std.Internal.List.insertList {α : Type u} {β : αType v} [BEq α] (l toInsert : List ((a : α) × β a)) :
List ((a : α) × β a)

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.DistinctKeys.insertList {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (h : DistinctKeys l₁) :
theorem Std.Internal.List.insertList_perm_of_perm_first {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l1 l2 toInsert : List ((a : α) × β a)} (h : l1.Perm l2) (distinct : DistinctKeys l1) :
(insertList l1 toInsert).Perm (insertList l2 toInsert)
theorem Std.Internal.List.insertList_cons_perm {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {p : (a : α) × β a} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys (p :: l₂)) :
(insertList l₁ (p :: l₂)).Perm (insertEntry p.fst p.snd (insertList l₁ l₂))
theorem Std.Internal.List.getEntry?_insertList {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (k : α) :
getEntry? k (insertList l toInsert) = (getEntry? k toInsert).or (getEntry? k l)
theorem Std.Internal.List.getEntry?_insertList_of_contains_eq_false {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : containsKey k toInsert = false) :
getEntry? k (insertList l toInsert) = getEntry? k l
theorem Std.Internal.List.getEntry?_insertList_of_contains_eq_true {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (contains : containsKey k toInsert = true) :
getEntry? k (insertList l toInsert) = getEntry? k toInsert
theorem Std.Internal.List.containsKey_insertList {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} :
containsKey k (insertList l toInsert) = (containsKey k l || (List.map Sigma.fst toInsert).contains k)
theorem Std.Internal.List.containsKey_of_containsKey_insertList {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (h₁ : containsKey k (insertList l toInsert) = true) (h₂ : (List.map Sigma.fst toInsert).contains k = false) :
theorem Std.Internal.List.getValueCast?_insertList_of_contains_eq_false {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : (List.map Sigma.fst toInsert).contains k = false) :
theorem Std.Internal.List.getValueCast?_insertList_of_mem {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k, v toInsert) :
getValueCast? k' (insertList l toInsert) = some (cast v)
theorem Std.Internal.List.getValueCast_insertList_of_contains_eq_false {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : (List.map Sigma.fst toInsert).contains k = false) {h : containsKey k (insertList l toInsert) = true} :
getValueCast k (insertList l toInsert) h = getValueCast k l
theorem Std.Internal.List.getValueCast_insertList_of_mem {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (v : β k) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k, v toInsert) {h : containsKey k' (insertList l toInsert) = true} :
getValueCast k' (insertList l toInsert) h = cast v
theorem Std.Internal.List.getValueCast!_insertList_of_contains_eq_false {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (not_contains : (List.map Sigma.fst toInsert).contains k = false) :
theorem Std.Internal.List.getValueCast!_insertList_of_mem {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (v : β k) [Inhabited (β k')] (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k, v toInsert) :
getValueCast! k' (insertList l toInsert) = cast v
theorem Std.Internal.List.getValueCastD_insertList_of_contains_eq_false {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} {fallback : β k} (not_mem : (List.map Sigma.fst toInsert).contains k = false) :
getValueCastD k (insertList l toInsert) fallback = getValueCastD k l fallback
theorem Std.Internal.List.getValueCastD_insertList_of_mem {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k, v toInsert) :
getValueCastD k' (insertList l toInsert) fallback = cast v
theorem Std.Internal.List.getKey?_insertList_of_contains_eq_false {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : (List.map Sigma.fst toInsert).contains k = false) :
getKey? k (insertList l toInsert) = getKey? k l
theorem Std.Internal.List.getKey?_insertList_of_mem {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k List.map Sigma.fst toInsert) :
getKey? k' (insertList l toInsert) = some k
theorem Std.Internal.List.getKey_insertList_of_contains_eq_false {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : (List.map Sigma.fst toInsert).contains k = false) {h : containsKey k (insertList l toInsert) = true} :
getKey k (insertList l toInsert) h = getKey k l
theorem Std.Internal.List.getKey_insertList_of_mem {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k List.map Sigma.fst toInsert) {h : containsKey k' (insertList l toInsert) = true} :
getKey k' (insertList l toInsert) h = k
theorem Std.Internal.List.getKey!_insertList_of_contains_eq_false {α : Type u} {β : αType v} [BEq α] [EquivBEq α] [Inhabited α] {l toInsert : List ((a : α) × β a)} {k : α} (contains_false : (List.map Sigma.fst toInsert).contains k = false) :
getKey! k (insertList l toInsert) = getKey! k l
theorem Std.Internal.List.getKey!_insertList_of_mem {α : Type u} {β : αType v} [BEq α] [EquivBEq α] [Inhabited α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k List.map Sigma.fst toInsert) :
getKey! k' (insertList l toInsert) = k
theorem Std.Internal.List.getKeyD_insertList_of_contains_eq_false {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α} (not_contains : (List.map Sigma.fst toInsert).contains k = false) :
getKeyD k (insertList l toInsert) fallback = getKeyD k l fallback
theorem Std.Internal.List.getKeyD_insertList_of_mem {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' fallback : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k List.map Sigma.fst toInsert) :
getKeyD k' (insertList l toInsert) fallback = k
theorem Std.Internal.List.perm_insertList {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (distinct_both : ∀ (a : α), containsKey a l = true(List.map Sigma.fst toInsert).contains a = false) :
(insertList l toInsert).Perm (l ++ toInsert)
theorem Std.Internal.List.length_insertList {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (distinct_both : ∀ (a : α), containsKey a l = true(List.map Sigma.fst toInsert).contains a = false) :
(insertList l toInsert).length = l.length + toInsert.length
theorem Std.Internal.List.length_le_length_insertList {α : Type u} {β : αType v} [BEq α] {l toInsert : List ((a : α) × β a)} :
l.length (insertList l toInsert).length
theorem Std.Internal.List.length_insertList_le {α : Type u} {β : αType v} [BEq α] {l toInsert : List ((a : α) × β a)} :
(insertList l toInsert).length l.length + toInsert.length
theorem Std.Internal.List.isEmpty_insertList {α : Type u} {β : αType v} [BEq α] {l toInsert : List ((a : α) × β a)} :
(insertList l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)
def Std.Internal.List.Prod.toSigma {α : Type u} {β : Type v} (p : α × β) :
(_ : α) × β

Internal implementation detail of the hash map

Equations
def Std.Internal.List.insertListConst {α : Type u} {β : Type v} [BEq α] (l : List ((_ : α) × β)) (toInsert : List (α × β)) :
List ((_ : α) × β)

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.containsKey_insertListConst {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} :
theorem Std.Internal.List.containsKey_of_containsKey_insertListConst {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (h₁ : containsKey k (insertListConst l toInsert) = true) (h₂ : (List.map Prod.fst toInsert).contains k = false) :
theorem Std.Internal.List.getKey?_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) :
getKey? k (insertListConst l toInsert) = getKey? k l
theorem Std.Internal.List.getKey?_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k List.map Prod.fst toInsert) :
getKey? k' (insertListConst l toInsert) = some k
theorem Std.Internal.List.getKey_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) {h : containsKey k (insertListConst l toInsert) = true} :
getKey k (insertListConst l toInsert) h = getKey k l
theorem Std.Internal.List.getKey_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k List.map Prod.fst toInsert) {h : containsKey k' (insertListConst l toInsert) = true} :
getKey k' (insertListConst l toInsert) h = k
theorem Std.Internal.List.getKey!_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) :
getKey! k (insertListConst l toInsert) = getKey! k l
theorem Std.Internal.List.getKey!_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k List.map Prod.fst toInsert) :
getKey! k' (insertListConst l toInsert) = k
theorem Std.Internal.List.getKeyD_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k fallback : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) :
getKeyD k (insertListConst l toInsert) fallback = getKeyD k l fallback
theorem Std.Internal.List.getKeyD_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' fallback : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k List.map Prod.fst toInsert) :
getKeyD k' (insertListConst l toInsert) fallback = k
theorem Std.Internal.List.length_insertListConst {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (distinct_both : ∀ (a : α), containsKey a l = true(List.map Prod.fst toInsert).contains a = false) :
(insertListConst l toInsert).length = l.length + toInsert.length
theorem Std.Internal.List.length_le_length_insertListConst {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} :
theorem Std.Internal.List.length_insertListConst_le {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} :
(insertListConst l toInsert).length l.length + toInsert.length
theorem Std.Internal.List.isEmpty_insertListConst {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} :
(insertListConst l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)
theorem Std.Internal.List.getValue?_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) :
theorem Std.Internal.List.getValue?_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) toInsert) :
getValue? k' (insertListConst l toInsert) = some v
theorem Std.Internal.List.getValue_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} {not_contains : (List.map Prod.fst toInsert).contains k = false} {h : containsKey k (insertListConst l toInsert) = true} :
getValue k (insertListConst l toInsert) h = getValue k l
theorem Std.Internal.List.getValue_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) toInsert) {h : containsKey k' (insertListConst l toInsert) = true} :
getValue k' (insertListConst l toInsert) h = v
theorem Std.Internal.List.getValue!_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) :
theorem Std.Internal.List.getValue!_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v : β} (distinct_l : DistinctKeys l) (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) toInsert) :
getValue! k' (insertListConst l toInsert) = v
theorem Std.Internal.List.getValueD_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} {fallback : β} (not_contains : (List.map Prod.fst toInsert).contains k = false) :
getValueD k (insertListConst l toInsert) fallback = getValueD k l fallback
theorem Std.Internal.List.getValueD_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback : β} (distinct_l : DistinctKeys l) (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) toInsert) :
getValueD k' (insertListConst l toInsert) fallback = v
def Std.Internal.List.insertListIfNewUnit {α : Type u} [BEq α] (l : List ((_ : α) × Unit)) (toInsert : List α) :
List ((_ : α) × Unit)

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.insertListIfNewUnit_perm_of_perm_first {α : Type u} [BEq α] [EquivBEq α] {l1 l2 : List ((_ : α) × Unit)} {toInsert : List α} (h : l1.Perm l2) (distinct : DistinctKeys l1) :
(insertListIfNewUnit l1 toInsert).Perm (insertListIfNewUnit l2 toInsert)
theorem Std.Internal.List.DistinctKeys.insertListIfNewUnit {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} (distinct : DistinctKeys l) :
theorem Std.Internal.List.getEntry?_insertListIfNewUnit {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} :
getEntry? k (insertListIfNewUnit l toInsert) = (getEntry? k l).or (getEntry? k (List.map (fun (x : α) => x, ()) toInsert))
theorem Std.Internal.List.DistinctKeys.mapUnit {α : Type u} [BEq α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :
DistinctKeys (List.map (fun (x : α) => x, ()) l)
theorem Std.Internal.List.getEntry?_insertListIfNewUnit_of_contains_eq_false {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (not_contains : toInsert.contains k = false) :
theorem Std.Internal.List.containsKey_insertListIfNewUnit {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} :
containsKey k (insertListIfNewUnit l toInsert) = (containsKey k l || toInsert.contains k)
theorem Std.Internal.List.containsKey_of_containsKey_insertListIfNewUnit {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (h₂ : toInsert.contains k = false) :
theorem Std.Internal.List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (h' : containsKey k l = false) (h : toInsert.contains k = false) :
theorem Std.Internal.List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' : α} (k_beq : (k == k') = true) (mem' : containsKey k l = false) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) toInsert) (mem : k toInsert) :
getKey? k' (insertListIfNewUnit l toInsert) = some k
theorem Std.Internal.List.getKey?_insertListIfNewUnit_of_contains {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (h : containsKey k l = true) :
theorem Std.Internal.List.getKey_insertListIfNewUnit_of_contains_eq_false_of_mem {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' : α} (k_beq : (k == k') = true) {h : containsKey k' (insertListIfNewUnit l toInsert) = true} (contains_eq_false : containsKey k l = false) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) toInsert) (mem : k toInsert) :
getKey k' (insertListIfNewUnit l toInsert) h = k
theorem Std.Internal.List.getKey_insertListIfNewUnit_of_contains {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (contains : containsKey k l = true) {h : containsKey k (insertListIfNewUnit l toInsert) = true} :
getKey k (insertListIfNewUnit l toInsert) h = getKey k l contains
theorem Std.Internal.List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false {α : Type u} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (contains_eq_false : containsKey k l = false) (contains_eq_false' : toInsert.contains k = false) :
theorem Std.Internal.List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_mem {α : Type u} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' : α} (k_beq : (k == k') = true) (h : containsKey k l = false) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) toInsert) (mem : k toInsert) :
getKey! k' (insertListIfNewUnit l toInsert) = k
theorem Std.Internal.List.getKey!_insertListIfNewUnit_of_contains {α : Type u} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (h : containsKey k l = true) :
theorem Std.Internal.List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α} (contains_eq_false : containsKey k l = false) (contains_eq_false' : toInsert.contains k = false) :
getKeyD k (insertListIfNewUnit l toInsert) fallback = fallback
theorem Std.Internal.List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_mem {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' fallback : α} (k_beq : (k == k') = true) (h : containsKey k l = false) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) toInsert) (mem : k toInsert) :
getKeyD k' (insertListIfNewUnit l toInsert) fallback = k
theorem Std.Internal.List.getKeyD_insertListIfNewUnit_of_contains {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α} (contains : containsKey k l = true) :
getKeyD k (insertListIfNewUnit l toInsert) fallback = getKeyD k l fallback
theorem Std.Internal.List.length_insertListIfNewUnit {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α) => (a == b) = false) toInsert) (distinct_both : ∀ (a : α), containsKey a l = truetoInsert.contains a = false) :
(insertListIfNewUnit l toInsert).length = l.length + toInsert.length
theorem Std.Internal.List.length_le_length_insertListIfNewUnit {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} :
theorem Std.Internal.List.length_insertListIfNewUnit_le {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} :
(insertListIfNewUnit l toInsert).length l.length + toInsert.length
theorem Std.Internal.List.isEmpty_insertListIfNewUnit {α : Type u} [BEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} :
(insertListIfNewUnit l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)
theorem Std.Internal.List.getValue?_list_unit {α : Type u} [BEq α] {l : List ((_ : α) × Unit)} {k : α} :
theorem Std.Internal.List.getValue?_insertListIfNewUnit {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} :
def Std.Internal.List.alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (k : α) (f : Option (β k)Option (β k)) (l : List ((a : α) × β a)) :
List ((a : α) × β a)

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.length_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} {l : List ((a : α) × β a)} :
(alterKey k f l).length = if h : containsKey k l = true then if (f (some (getValueCast k l h))).isSome = true then l.length else l.length - 1 else if (f none).isSome = true then l.length + 1 else l.length
theorem Std.Internal.List.length_alterKey' {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} {l : List ((a : α) × β a)} :
theorem Std.Internal.List.alterKey_cons_perm {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} {k' : α} {v' : β k'} {l : List ((a : α) × β a)} :
(alterKey k f (k', v' :: l)).Perm (if hk : (k' == k) = true then match f (some (cast v')) with | none => l | some v => k, v :: l else k', v' :: alterKey k f l)
theorem Std.Internal.List.isEmpty_alterKey_eq_isEmpty_eraseKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} {l : List ((a : α) × β a)} :
theorem Std.Internal.List.isEmpty_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} {l : List ((a : α) × β a)} :
theorem Std.Internal.List.alterKey_of_perm {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a)Option (β a)} {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hp : l.Perm l') :
(alterKey a f l).Perm (alterKey a f l')
theorem Std.Internal.List.alterKey_append_of_containsKey_right_eq_false {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a)Option (β a)} {l l' : List ((a : α) × β a)} (hc : containsKey a l' = false) :
alterKey a f (l ++ l') = alterKey a f l ++ l'
@[simp]
theorem Std.Internal.List.alterKey_nil {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a)Option (β a)} :
alterKey a f [] = match f none with | none => [] | some b => [a, b]
theorem Std.Internal.List.containsKey_alterKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a)Option (β a)} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.containsKey_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' : α} {f : Option (β k)Option (β k)} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.DistinctKeys.alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a)Option (β a)} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.mem_alterKey_of_key_ne {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a)Option (β a)} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.fst a) :
p alterKey a f l p l
theorem Std.Internal.List.getValueCast?_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (k k' : α) (f : Option (β k)Option (β k)) (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCast? k' (alterKey k f l) = if h : (k == k') = true then cast (f (getValueCast? k l)) else getValueCast? k' l
theorem Std.Internal.List.getValueCast_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (k k' : α) (f : Option (β k)Option (β k)) (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l) = true) :
getValueCast k' (alterKey k f l) hc = if h : (k == k') = true then cast ((f (getValueCast? k l)).get ) else getValueCast k' l
theorem Std.Internal.List.getValueCast_alterKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (k : α) (f : Option (β k)Option (β k)) (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k (alterKey k f l) = true) :
getValueCast k (alterKey k f l) hc = (f (getValueCast? k l)).get
theorem Std.Internal.List.getValueCast!_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' : α} [Inhabited (β k')] {f : Option (β k)Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCast! k' (alterKey k f l) = if heq : (k == k') = true then (Option.map (cast ) (f (getValueCast? k l))).get! else getValueCast! k' l
theorem Std.Internal.List.getValueCastD_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' : α} {fallback : β k'} {f : Option (β k)Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCastD k' (alterKey k f l) fallback = if heq : (k == k') = true then (Option.map (cast ) (f (getValueCast? k l))).getD fallback else getValueCastD k' l fallback
theorem Std.Internal.List.getKey?_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' : α} {f : Option (β k)Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey!_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k)Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' : α} {f : Option (β k)Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l) = true) :
getKey k' (alterKey k f l) hc = if heq : (k == k') = true then k else getKey k' l
theorem Std.Internal.List.getKeyD_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' fallback : α} {f : Option (β k)Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getKeyD k' (alterKey k f l) fallback = if (k == k') = true then if (f (getValueCast? k l)).isSome = true then k else fallback else getKeyD k' l fallback
def Std.Internal.List.Const.alterKey {α : Type u} {β : Type v} [BEq α] (k : α) (f : Option βOption β) (l : List ((_ : α) × β)) :
List ((_ : α) × β)

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.Const.length_alterKey {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option βOption β} {l : List ((_ : α) × β)} :
(alterKey k f l).length = if h : containsKey k l = true then if (f (some (getValue k l h))).isSome = true then l.length else l.length - 1 else if (f none).isSome = true then l.length + 1 else l.length
theorem Std.Internal.List.Const.length_alterKey' {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option βOption β} {l : List ((_ : α) × β)} :
theorem Std.Internal.List.Const.length_alterKey_eq_add_one {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option βOption β} {l : List ((_ : α) × β)} (h : containsKey k l = false) (h' : (f (getValue? k l)).isSome = true) :
(alterKey k f l).length = l.length + 1
theorem Std.Internal.List.Const.length_alterKey_eq_sub_one {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option βOption β} {l : List ((_ : α) × β)} (h : containsKey k l = true) (h' : (f (getValue? k l)).isNone = true) :
(alterKey k f l).length = l.length - 1
theorem Std.Internal.List.Const.length_alterKey_eq_self {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option βOption β} {l : List ((_ : α) × β)} (h : containsKey k l = true) (h' : (f (getValue? k l)).isSome = true) :
theorem Std.Internal.List.Const.length_alterKey_eq_self' {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option βOption β} {l : List ((_ : α) × β)} (h : containsKey k l = false) (h' : (f (getValue? k l)).isNone = true) :
theorem Std.Internal.List.Const.alterKey_cons_perm {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option βOption β} {k' : α} {v' : β} {l : List ((_ : α) × β)} :
(alterKey k f (k', v' :: l)).Perm (if (k' == k) = true then match f (some v') with | none => l | some v => k, v :: l else k', v' :: alterKey k f l)
theorem Std.Internal.List.Const.isEmpty_alterKey_eq_isEmpty_eraseKey {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option βOption β} {l : List ((_ : α) × β)} :
(alterKey k f l).isEmpty = ((eraseKey k l).isEmpty && (f (getValue? k l)).isNone)
theorem Std.Internal.List.Const.isEmpty_alterKey {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option βOption β} {l : List ((_ : α) × β)} :
(alterKey k f l).isEmpty = ((l.isEmpty || l.length == 1 && containsKey k l) && (f (getValue? k l)).isNone)
theorem Std.Internal.List.Const.alterKey_of_perm {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {a : α} {f : Option βOption β} {l l' : List ((_ : α) × β)} (hl : DistinctKeys l) (hp : l.Perm l') :
(alterKey a f l).Perm (alterKey a f l')
theorem Std.Internal.List.Const.alterKey_append_of_containsKey_right_eq_false {α : Type u} [BEq α] {β : Type v} {a : α} {f : Option βOption β} {l l' : List ((_ : α) × β)} (hc : containsKey a l' = false) :
alterKey a f (l ++ l') = alterKey a f l ++ l'
@[simp]
theorem Std.Internal.List.Const.alterKey_nil {α : Type u} [BEq α] {β : Type v} {a : α} {f : Option βOption β} :
alterKey a f [] = match f none with | none => [] | some b => [a, b]
theorem Std.Internal.List.Const.containsKey_alterKey_self {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {a : α} {f : Option βOption β} {l : List ((_ : α) × β)} (hl : DistinctKeys l) :
containsKey a (alterKey a f l) = (f (getValue? a l)).isSome
theorem Std.Internal.List.Const.mem_alterKey_of_key_not_beq {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {a : α} {f : Option βOption β} {l : List ((_ : α) × β)} (p : (_ : α) × β) (hne : (p.fst == a) = false) :
p alterKey a f l p l
theorem Std.Internal.List.Const.containsKey_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} {f : Option βOption β} {l : List ((_ : α) × β)} (hl : DistinctKeys l) :
containsKey k' (alterKey k f l) = if (k == k') = true then (f (getValue? k l)).isSome else containsKey k' l
theorem Std.Internal.List.Const.getValue?_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] (k k' : α) (f : Option βOption β) (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
getValue? k' (alterKey k f l) = if (k == k') = true then f (getValue? k l) else getValue? k' l
theorem Std.Internal.List.Const.getValue_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] (k k' : α) (f : Option βOption β) (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l) = true) :
getValue k' (alterKey k f l) hc = if h : (k == k') = true then (f (getValue? k l)).get else getValue k' l
theorem Std.Internal.List.Const.getValue_alterKey_self {α : Type u} [BEq α] {β : Type v} [EquivBEq α] (k : α) (f : Option βOption β) (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k (alterKey k f l) = true) :
getValue k (alterKey k f l) hc = (f (getValue? k l)).get
theorem Std.Internal.List.Const.getValue!_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} [Inhabited β] {f : Option βOption β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
getValue! k' (alterKey k f l) = if (k == k') = true then (f (getValue? k l)).get! else getValue! k' l
theorem Std.Internal.List.Const.getValueD_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} {fallback : β} {f : Option βOption β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
getValueD k' (alterKey k f l) fallback = if (k == k') = true then (f (getValue? k l)).getD fallback else getValueD k' l fallback
theorem Std.Internal.List.Const.getKey?_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} {f : Option βOption β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
getKey? k' (alterKey k f l) = if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l
theorem Std.Internal.List.Const.getKey!_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] [Inhabited α] {k k' : α} {f : Option βOption β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
getKey! k' (alterKey k f l) = if (k == k') = true then if (f (getValue? k l)).isSome = true then k else default else getKey! k' l
theorem Std.Internal.List.Const.getKey_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} {f : Option βOption β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l) = true) :
getKey k' (alterKey k f l) hc = if heq : (k == k') = true then k else getKey k' l
theorem Std.Internal.List.Const.getKeyD_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' fallback : α} {f : Option βOption β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
getKeyD k' (alterKey k f l) fallback = if (k == k') = true then if (f (getValue? k l)).isSome = true then k else fallback else getKeyD k' l fallback
theorem Std.Internal.List.constAlterKey_eq_alterKey {α : Type u} [BEq α] [LawfulBEq α] {β : Type v} {k : α} {f : Option βOption β} {l : List ((_ : α) × β)} :
theorem Std.Internal.List.DistinctKeys.constAlterKey {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {a : α} {f : Option βOption β} {l : List ((_ : α) × β)} (hl : DistinctKeys l) :
def Std.Internal.List.modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (k : α) (f : β kβ k) (l : List ((a : α) × β a)) :
List ((a : α) × β a)

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.isEmpty_modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (k : α) (f : β kβ k) (l : List ((a : α) × β a)) :
theorem Std.Internal.List.length_modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (k : α) (f : β kβ k) (l : List ((a : α) × β a)) :
theorem Std.Internal.List.containsKey_modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (k k' : α) (f : β kβ k) (l : List ((a : α) × β a)) :
theorem Std.Internal.List.modifyKey_eq_alterKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (k : α) (f : β kβ k) (l : List ((a : α) × β a)) :
modifyKey k f l = alterKey k (fun (x : Option (β k)) => Option.map f x) l
theorem Std.Internal.List.DistinctKeys.modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {f : β aβ a} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.modifyKey_of_perm {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {k : α} {f : β kβ k} (hl : DistinctKeys l) (h : l.Perm l') :
(modifyKey k f l).Perm (modifyKey k f l')
theorem Std.Internal.List.getValueCast?_modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' : α} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCast? k' (modifyKey k f l) = if h : (k == k') = true then cast (Option.map f (getValueCast? k l)) else getValueCast? k' l
@[simp]
theorem Std.Internal.List.getValueCast?_modifyKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCast_modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' : α} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l) = true) :
getValueCast k' (modifyKey k f l) h = if heq : (k == k') = true then cast (f (getValueCast k l )) else getValueCast k' l
@[simp]
theorem Std.Internal.List.getValueCast_modifyKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) {h : containsKey k (modifyKey k f l) = true} :
getValueCast k (modifyKey k f l) h = f (getValueCast k l )
theorem Std.Internal.List.getValueCast!_modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCast! k' (modifyKey k f l) = if heq : (k == k') = true then (Option.map (cast ) (Option.map f (getValueCast? k l))).get! else getValueCast! k' l
@[simp]
theorem Std.Internal.List.getValueCast!_modifyKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} [Inhabited (β k)] {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCastD_modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCastD k' (modifyKey k f l) fallback = if heq : (k == k') = true then (Option.map (cast ) (Option.map f (getValueCast? k l))).getD fallback else getValueCastD k' l fallback
@[simp]
theorem Std.Internal.List.getValueCastD_modifyKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} {fallback : β k} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCastD k (modifyKey k f l) fallback = (Option.map f (getValueCast? k l)).getD fallback
theorem Std.Internal.List.getKey?_modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' : α} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey?_modifyKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey!_modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey!_modifyKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Inhabited α] {k : α} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey_modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' : α} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l) = true) :
getKey k' (modifyKey k f l) h = if (k == k') = true then k else getKey k' l
@[simp]
theorem Std.Internal.List.getKey_modifyKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k : α} {f : β kβ k} (l : List ((a : α) × β a)) :
DistinctKeys l∀ (h : containsKey k (modifyKey k f l) = true), getKey k (modifyKey k f l) h = k
theorem Std.Internal.List.getKeyD_modifyKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k k' fallback : α} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getKeyD k' (modifyKey k f l) fallback = if (k == k') = true then if containsKey k l = true then k else fallback else getKeyD k' l fallback
theorem Std.Internal.List.getKeyD_modifyKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {k fallback : α} {f : β kβ k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getKeyD k (modifyKey k f l) fallback = if containsKey k l = true then k else fallback
def Std.Internal.List.Const.modifyKey {α : Type u} {β : Type v} [BEq α] (k : α) (f : ββ) (l : List ((_ : α) × β)) :
List ((_ : α) × β)

Internal implementation detail of the hash map

Equations
theorem Std.Internal.List.Const.isEmpty_modifyKey {α : Type u} {β : Type v} [BEq α] (k : α) (f : ββ) (l : List ((_ : α) × β)) :
theorem Std.Internal.List.Const.modifyKey_eq_alterKey {α : Type u} {β : Type v} [BEq α] (k : α) (f : ββ) (l : List ((_ : α) × β)) :
modifyKey k f l = alterKey k (fun (x : Option β) => Option.map f x) l
theorem Std.Internal.List.Const.modifyKey_of_perm {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l l' : List ((_ : α) × β)} {k : α} {f : ββ} (hl : DistinctKeys l) (h : l.Perm l') :
(modifyKey k f l).Perm (modifyKey k f l')
theorem Std.Internal.List.Const.length_modifyKey {α : Type u} {β : Type v} [BEq α] (k : α) (f : ββ) (l : List ((_ : α) × β)) :
theorem Std.Internal.List.Const.containsKey_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] (k k' : α) (f : ββ) (l : List ((_ : α) × β)) :
theorem Std.Internal.List.Const.getValue?_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
@[simp]
theorem Std.Internal.List.Const.getValue?_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getValue_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l) = true) :
getValue k' (modifyKey k f l) h = if heq : (k == k') = true then f (getValue k l ) else getValue k' l
@[simp]
theorem Std.Internal.List.Const.getValue_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) {h : containsKey k (modifyKey k f l) = true} :
getValue k (modifyKey k f l) h = f (getValue k l )
theorem Std.Internal.List.Const.getValue!_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} [hi : Inhabited β] {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
@[simp]
theorem Std.Internal.List.Const.getValue!_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} [Inhabited β] {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getValueD_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {fallback : β} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
getValueD k' (modifyKey k f l) fallback = if (k == k') = true then (Option.map f (getValue? k l)).getD fallback else getValueD k' l fallback
@[simp]
theorem Std.Internal.List.Const.getValueD_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {fallback : β} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
getValueD k (modifyKey k f l) fallback = (Option.map f (getValue? k l)).getD fallback
theorem Std.Internal.List.Const.getKey?_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getKey?_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getKey!_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {k k' : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getKey!_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {k : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getKey_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l) = true) :
getKey k' (modifyKey k f l) h = if (k == k') = true then k else getKey k' l
@[simp]
theorem Std.Internal.List.Const.getKey_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l) = true) :
getKey k (modifyKey k f l) h = k
theorem Std.Internal.List.Const.getKeyD_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' fallback : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
getKeyD k' (modifyKey k f l) fallback = if (k == k') = true then if containsKey k l = true then k else fallback else getKeyD k' l fallback
theorem Std.Internal.List.Const.getKeyD_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k fallback : α} {f : ββ} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
getKeyD k (modifyKey k f l) fallback = if containsKey k l = true then k else fallback
theorem Std.Internal.List.constModifyKey_eq_modifyKey {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] {k : α} {f : ββ} {l : List ((_ : α) × β)} :
theorem Std.Internal.List.DistinctKeys.constModifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {a : α} {f : ββ} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
theorem Std.Internal.List.min_def {α : Type u} {β : αType v} [Ord α] {p q : (a : α) × β a} :
min p q = if (compare p.fst q.fst).isLE = true then p else q
def Std.Internal.List.minEntry? {α : Type u} {β : αType v} [Ord α] (xs : List ((a : α) × β a)) :
Option ((a : α) × β a)

Like List.min?, but using an Ord typeclass instead of a Min typeclass.

Equations
def Std.Internal.List.minKey? {α : Type u} {β : αType v} [Ord α] (xs : List ((a : α) × β a)) :

Returns the smallest key in an associative list.

Equations
theorem Std.Internal.List.DistinctKeys.eq_of_mem_of_beq {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {a b : (a : α) × β a} {l : List ((a : α) × β a)} (hma : a l) (hmb : b l) (he : (a.fst == b.fst) = true) (hd : DistinctKeys l) :
a = b
theorem Std.Internal.List.min_eq_or {α : Type u} {β : αType v} [Ord α] {p q : (a : α) × β a} :
min p q = p min p q = q
theorem Std.Internal.List.min_eq_left {α : Type u} {β : αType v} [Ord α] {p q : (a : α) × β a} (h : (compare p.fst q.fst).isLE = true) :
min p q = p
theorem Std.Internal.List.min_eq_left_of_lt {α : Type u} {β : αType v} [Ord α] {p q : (a : α) × β a} (h : compare p.fst q.fst = Ordering.lt) :
min p q = p
theorem Std.Internal.List.minEntry?_eq_head? {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} (hl : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) :
@[simp]
theorem Std.Internal.List.minEntry?_nil {α : Type u} {β : αType v} [Ord α] :
theorem Std.Internal.List.minEntry?_cons {α : Type u} {β : αType v} [Ord α] [TransOrd α] (e : (a : α) × β a) (l : List ((a : α) × β a)) :
minEntry? (e :: l) = some (match minEntry? l with | none => e | some w => min e w)
theorem Std.Internal.List.isSome_minEntry?_of_isEmpty_eq_false {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} (hl : l.isEmpty = false) :
theorem Std.Internal.List.le_min_iff {α : Type u} {β : αType v} [Ord α] [TransOrd α] {a b c : (a : α) × β a} :
a min b c a b a c
theorem Std.Internal.List.minEntry?_eq_some_iff {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] (a : (a : α) × β a) {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
minEntry? l = some a a l ∀ (b : α), containsKey b l = true(compare a.fst b).isLE = true
theorem Std.Internal.List.minKey?_eq_some_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
minKey? l = some k getKey? k l = some k ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
theorem Std.Internal.List.minKey?_eq_some_iff_mem_and_forall {α : Type u} {β : αType v} [Ord α] [LawfulEqOrd α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
minKey? l = some k containsKey k l = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
theorem Std.Internal.List.minEntry?_of_perm {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.minKey?_of_perm {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.minEntry?_eq_none_iff_isEmpty {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.minKey?_eq_none_iff_isEmpty {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.minKey?_of_isEmpty {α : Type u} {β : αType v} [Ord α] [TransOrd α] {l : List ((a : α) × β a)} (he : l.isEmpty = true) :
theorem Std.Internal.List.isNone_minEntry?_eq_isEmpty {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.isNone_minKey?_eq_isEmpty {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.isSome_minEntry?_eq_not_isEmpty {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.isSome_minKey?_eq_not_isEmpty {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.isSome_minKey?_iff_isEmpty_eq_false {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.min_apply {α : Type u} {β : αType v} [Ord α] {e₁ e₂ : (a : α) × β a} {f : (a : α) × β a(a : α) × β a} (hf : compare e₁.fst e₂.fst = compare (f e₁).fst (f e₂).fst) :
min (f e₁) (f e₂) = f (min e₁ e₂)
theorem Std.Internal.List.minEntry?_map {α : Type u} {β : αType v} [Ord α] (l : List ((a : α) × β a)) (f : (a : α) × β a(a : α) × β a) (hf : ∀ (e₁ e₂ : (a : α) × β a), compare e₁.fst e₂.fst = compare (f e₁).fst (f e₂).fst) :
theorem Std.Internal.List.replaceEntry_eq_map {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
replaceEntry k v l = List.map (fun (e : (a : α) × β a) => if (e.fst == k) = true then k, v else e) l
theorem Std.Internal.List.minEntry?_replaceEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
minEntry? (replaceEntry k v l) = Option.map (fun (e : (a : α) × β a) => if (e.fst == k) = true then k, v else e) (minEntry? l)
theorem Std.Internal.List.isSome_minEntry?_of_contains {α : Type u} {β : αType v} [Ord α] [BEq α] {l : List ((a : α) × β a)} {b : α} (hb : containsKey b l = true) :
theorem Std.Internal.List.minEntry?_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
minEntry? (insertEntry k v l) = some (match minEntry? l with | none => k, v | some w => if (compare k w.fst).isLE = true then k, v else w)
theorem Std.Internal.List.minKey?_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
minKey? (insertEntry k v l) = some ((minKey? l).elim k fun (k' : α) => if (compare k k').isLE = true then k else k')
theorem Std.Internal.List.isSome_minEntry?_insert {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.isSome_minKey?_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.isSome_minEntry?_of_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hc : containsKey k l = true) :
theorem Std.Internal.List.isSome_minKey?_of_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hc : containsKey k l = true) :
theorem Std.Internal.List.getEntry?_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {em : (a : α) × β a} (hem : minEntry? l = some em) :
theorem Std.Internal.List.minKey?_bind_getEntry? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
((minKey? l).bind fun (k : α) => getEntry? k l) = minEntry? l
theorem Std.Internal.List.getKey?_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} (hkm : minKey? l = some km) :
getKey? km l = some km
theorem Std.Internal.List.getKey_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} {hc : containsKey km l = true} (hkm : (minKey? l).get = km) :
getKey km l hc = km
theorem Std.Internal.List.getKey!_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} (hkm : minKey? l = some km) :
getKey! km l = km
theorem Std.Internal.List.getKeyD_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km fallback : α} (hkm : minKey? l = some km) :
getKeyD km l fallback = km
theorem Std.Internal.List.minKey?_bind_getKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
((minKey? l).bind fun (k : α) => getKey? k l) = minKey? l
theorem Std.Internal.List.containsKey_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} (hkm : minKey? l = some km) :
theorem Std.Internal.List.minKey?_eraseKey_eq_iff_beq_minKey?_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
minKey? (eraseKey k l) = minKey? l ∀ {km : α}, minKey? l = some km → (k == km) = false
theorem Std.Internal.List.minKey?_eraseKey_eq_of_beq_minKey?_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hc : ∀ {km : α}, minKey? l = some km → (k == km) = false) :
theorem Std.Internal.List.minKey?_insertEntry_le_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) {km kmi : α} (hkm : minKey? l = some km) (hkmi : (minKey? (insertEntry k v l)).get = kmi) :
(compare kmi km).isLE = true
theorem Std.Internal.List.minKey?_insertEntry_le_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) {kmi : α} (hkmi : (minKey? (insertEntry k v l)).get = kmi) :
(compare kmi k).isLE = true
theorem Std.Internal.List.minKey?_le_of_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k km : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hc : containsKey k l = true) (hkm : (minKey? l).get = km) :
theorem Std.Internal.List.le_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
(∀ (k' : α), minKey? l = some k'(compare k k').isLE = true) ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
theorem Std.Internal.List.isSome_minKey?_of_isSome_minKey?_eraseKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hs : (minKey? (eraseKey k l)).isSome = true) :
theorem Std.Internal.List.containsKey_minKey?_eraseKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {kme : α} (hkme : minKey? (eraseKey k l) = some kme) :
theorem Std.Internal.List.minKey?_le_minKey?_eraseKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k km kme : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hkme : minKey? (eraseKey k l) = some kme) (hkm : (minKey? l).get = km) :
(compare km kme).isLE = true
theorem Std.Internal.List.minKey?_cons {α : Type u} {β : αType v} [Ord α] [TransOrd α] (e : (a : α) × β a) (l : List ((a : α) × β a)) :
minKey? (e :: l) = some (match minKey? l with | none => e.fst | some w => if (compare e.fst w).isLE = true then e.fst else w)
theorem Std.Internal.List.minEntry?_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
minEntry? (insertEntryIfNew k v l) = some (match minEntry? l with | none => k, v | some e => if compare k e.fst = Ordering.lt then k, v else e)
theorem Std.Internal.List.minKey?_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
minKey? (insertEntryIfNew k v l) = some ((minKey? l).elim k fun (k' : α) => if compare k k' = Ordering.lt then k else k')
theorem Std.Internal.List.isSome_minEntry?_insertIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.isSome_minKey?_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.minKey?_insertEntryIfNew_le_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) {km kmi : α} (hkm : minKey? l = some km) (hkmi : (minKey? (insertEntryIfNew k v l)).get = kmi) :
(compare kmi km).isLE = true
theorem Std.Internal.List.minKey?_insertEntryIfNew_le_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k kmi : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) (hkmi : (minKey? (insertEntryIfNew k v l)).get = kmi) :
(compare kmi k).isLE = true
theorem Std.Internal.List.minKey?_eq_head?_keys {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) :
theorem Std.Internal.List.minKey?_modifyKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : β kβ k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.minKey?_alterKey_eq_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : Option (β k)Option (β k)} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
minKey? (alterKey k f l) = some k (f (getValueCast? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
theorem Std.Internal.List.Const.minKey?_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : ββ} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
minKey? (modifyKey k f l) = Option.map (fun (km : α) => if (km == k) = true then k else km) (minKey? l)
theorem Std.Internal.List.Const.minKey?_modifyKey_eq_minKey? {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : ββ} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
theorem Std.Internal.List.Const.isSome_minKey?_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : ββ} {l : List ((_ : α) × β)} :
theorem Std.Internal.List.Const.isSome_minKey?_modifyKey_eq_isSome {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : ββ} {l : List ((_ : α) × β)} :
theorem Std.Internal.List.Const.minKey?_modifyKey_beq {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : ββ} {km kmm : α} {l : List ((_ : α) × β)} (hd : DistinctKeys l) (hkm : minKey? l = some km) (hkmm : (minKey? (modifyKey k f l)).get = kmm) :
(kmm == km) = true
theorem Std.Internal.List.Const.minKey?_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : Option βOption β} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
minKey? (alterKey k f l) = some k (f (getValue? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
def Std.Internal.List.minKey {α : Type u} {β : αType v} [Ord α] (xs : List ((a : α) × β a)) (h : xs.isEmpty = false) :
α

Given a proof that the list is nonempty, returns the smallest key in an associative list.

Equations
theorem Std.Internal.List.minKey_of_perm {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} {hl : l.isEmpty = false} (hd : DistinctKeys l) (hp : l.Perm l') :
minKey l hl = minKey l'
theorem Std.Internal.List.minKey_eq_get_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} :
minKey l he = (minKey? l).get
theorem Std.Internal.List.minKey?_eq_some_minKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} :
minKey? l = some (minKey l he)
theorem Std.Internal.List.minKey_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} {km : α} :
minKey l he = km getKey? km l = some km ∀ (k : α), containsKey k l = true(compare km k).isLE = true
theorem Std.Internal.List.minKey_eq_iff_mem_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} {km : α} :
minKey l he = km containsKey km l = true ∀ (k : α), containsKey k l = true(compare km k).isLE = true
theorem Std.Internal.List.minKey_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
minKey (insertEntry k v l) = (minKey? l).elim k fun (k' : α) => if (compare k k').isLE = true then k else k'
theorem Std.Internal.List.minKey_insertEntry_le_minKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {he : l.isEmpty = false} :
(compare (minKey (insertEntry k v l) ) (minKey l he)).isLE = true
theorem Std.Internal.List.minKey_insertEntry_le_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
(compare (minKey (insertEntry k v l) ) k).isLE = true
theorem Std.Internal.List.containsKey_minKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} :
theorem Std.Internal.List.minKey_le_of_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) :
(compare (minKey l ) k).isLE = true
theorem Std.Internal.List.le_minKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {he : l.isEmpty = false} :
(compare k (minKey l he)).isLE = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
theorem Std.Internal.List.getKey?_minKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} :
getKey? (minKey l he) l = some (minKey l he)
theorem Std.Internal.List.getKey_minKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} :
getKey (minKey l he) l = minKey l he
theorem Std.Internal.List.getKey!_minKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} :
getKey! (minKey l he) l = minKey l he
theorem Std.Internal.List.getKeyD_minKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} {fallback : α} :
getKeyD (minKey l he) l fallback = minKey l he
theorem Std.Internal.List.minKey_eraseKey_eq_iff_beq_minKey_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {he : (eraseKey k l).isEmpty = false} :
minKey (eraseKey k l) he = minKey l (k == minKey l ) = false
theorem Std.Internal.List.minKey_eraseKey_eq_of_beq_minKey_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {he : (eraseKey k l).isEmpty = false} (hc : (k == minKey l ) = false) :
minKey (eraseKey k l) he = minKey l
theorem Std.Internal.List.minKey_le_minKey_erase {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {he : (eraseKey k l).isEmpty = false} :
(compare (minKey l ) (minKey (eraseKey k l) he)).isLE = true
theorem Std.Internal.List.minKey_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
minKey (insertEntryIfNew k v l) = (minKey? l).elim k fun (k' : α) => if compare k k' = Ordering.lt then k else k'
theorem Std.Internal.List.minKey_insertEntryIfNew_le_minKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {he : l.isEmpty = false} :
theorem Std.Internal.List.minKey_insertEntryIfNew_le_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.minKey_eq_head_keys {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) {he : l.isEmpty = false} :
minKey l he = (keys l).head
theorem Std.Internal.List.minKey_modifyKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : β kβ k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : (modifyKey k f l).isEmpty = false} :
minKey (modifyKey k f l) he = minKey l
theorem Std.Internal.List.minKey_alterKey_eq_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k)Option (β k)} {he : (alterKey k f l).isEmpty = false} :
minKey (alterKey k f l) he = k (f (getValueCast? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
theorem Std.Internal.List.Const.minKey_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} {he : (modifyKey k f l).isEmpty = false} :
minKey (modifyKey k f l) he = if (minKey l == k) = true then k else minKey l
theorem Std.Internal.List.Const.minKey_modifyKey_eq_minKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} {he : (modifyKey k f l).isEmpty = false} :
minKey (modifyKey k f l) he = minKey l
theorem Std.Internal.List.Const.minKey_modifyKey_beq {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} {he : (modifyKey k f l).isEmpty = false} :
(minKey (modifyKey k f l) he == minKey l ) = true
theorem Std.Internal.List.Const.minKey_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : Option βOption β} {he : (alterKey k f l).isEmpty = false} :
minKey (alterKey k f l) he = k (f (getValue? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
def Std.Internal.List.minKey! {α : Type u} {β : αType v} [Ord α] [Inhabited α] (xs : List ((a : α) × β a)) :
α

Returns the smallest key in an associative list or panics if the list is empty.

Equations
theorem Std.Internal.List.minKey!_of_perm {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l l' : List ((a : α) × β a)} (hd : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.minKey!_eq_get!_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.minKey_eq_minKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} :
theorem Std.Internal.List.minKey?_eq_some_minKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (he : l.isEmpty = false) :
theorem Std.Internal.List.minKey!_eq_default {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (h : l.isEmpty = true) :
theorem Std.Internal.List.minKey!_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km : α} :
minKey! l = km getKey? km l = some km ∀ (k : α), containsKey k l = true(compare km k).isLE = true
theorem Std.Internal.List.minKey!_eq_iff_mem_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km : α} :
minKey! l = km containsKey km l = true ∀ (k : α), containsKey k l = true(compare km k).isLE = true
theorem Std.Internal.List.minKey!_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
minKey! (insertEntry k v l) = (minKey? l).elim k fun (k' : α) => if (compare k k').isLE = true then k else k'
theorem Std.Internal.List.minKey!_insertEntry_le_minKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} :
theorem Std.Internal.List.minKey!_insertEntry_le_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.containsKey_minKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
theorem Std.Internal.List.minKey!_le_of_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) :
theorem Std.Internal.List.le_minKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} :
(compare k (minKey! l)).isLE = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
theorem Std.Internal.List.getKey?_minKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
theorem Std.Internal.List.getKey_minKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : containsKey (minKey! l) l = true} :
getKey (minKey! l) l he = minKey! l
theorem Std.Internal.List.getKey_minKey!_eq_minKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : containsKey (minKey! l) l = true} :
getKey (minKey! l) l he = minKey l
theorem Std.Internal.List.getKey!_minKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
theorem Std.Internal.List.getKeyD_minKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback : α} :
getKeyD (minKey! l) l fallback = minKey! l
theorem Std.Internal.List.minKey!_eraseKey_eq_iff_beq_minKey_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) :
theorem Std.Internal.List.minKey!_eraseKey_eq_iff_beq_minKey!_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) :
theorem Std.Internal.List.minKey!_eraseKey_eq_of_beq_minKey!_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) (heq : (k == minKey! l) = false) :
theorem Std.Internal.List.minKey!_le_minKey!_erase {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) :
theorem Std.Internal.List.minKey!_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
minKey! (insertEntryIfNew k v l) = (minKey? l).elim k fun (k' : α) => if compare k k' = Ordering.lt then k else k'
theorem Std.Internal.List.minKey!_insertEntryIfNew_le_minKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} :
theorem Std.Internal.List.minKey!_insertEntryIfNew_le_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.minKey!_eq_head!_keys {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) :
theorem Std.Internal.List.minKey!_modifyKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : β kβ k} :
theorem Std.Internal.List.minKey!_alterKey_eq_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k)Option (β k)} (he : (alterKey k f l).isEmpty = false) :
minKey! (alterKey k f l) = k (f (getValueCast? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
theorem Std.Internal.List.Const.minKey!_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} (he : (modifyKey k f l).isEmpty = false) :
theorem Std.Internal.List.Const.minKey!_modifyKey_eq_minKey! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} :
theorem Std.Internal.List.Const.minKey!_modifyKey_beq {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} :
theorem Std.Internal.List.Const.minKey!_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : Option βOption β} (he : (alterKey k f l).isEmpty = false) :
minKey! (alterKey k f l) = k (f (getValue? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
def Std.Internal.List.minKeyD {α : Type u} {β : αType v} [Ord α] (xs : List ((a : α) × β a)) (fallback : α) :
α

Returns the smallest key in an associative list or fallback if the list is empty.

Equations
theorem Std.Internal.List.minKeyD_of_perm {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} {fallback : α} (hd : DistinctKeys l) (hp : l.Perm l') :
minKeyD l fallback = minKeyD l' fallback
theorem Std.Internal.List.minKeyD_eq_getD_minKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} :
minKeyD l fallback = (minKey? l).getD fallback
theorem Std.Internal.List.minKey_eq_minKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} {fallback : α} :
minKey l he = minKeyD l fallback
theorem Std.Internal.List.minKey?_eq_some_minKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} (he : l.isEmpty = false) :
minKey? l = some (minKeyD l fallback)
theorem Std.Internal.List.minKey!_eq_minKeyD_default {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.minKeyD_eq_fallback {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} (h : l.isEmpty = true) :
minKeyD l fallback = fallback
theorem Std.Internal.List.minKeyD_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km fallback : α} :
minKeyD l fallback = km getKey? km l = some km ∀ (k : α), containsKey k l = true(compare km k).isLE = true
theorem Std.Internal.List.minKeyD_eq_iff_mem_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km fallback : α} :
minKeyD l fallback = km containsKey km l = true ∀ (k : α), containsKey k l = true(compare km k).isLE = true
theorem Std.Internal.List.minKeyD_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
minKeyD (insertEntry k v l) fallback = (minKey? l).elim k fun (k' : α) => if (compare k k').isLE = true then k else k'
theorem Std.Internal.List.minKeyD_insertEntry_le_minKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} :
(compare (minKeyD (insertEntry k v l) fallback) (minKeyD l fallback)).isLE = true
theorem Std.Internal.List.minKeyD_insertEntry_le_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
(compare (minKeyD (insertEntry k v l) fallback) k).isLE = true
theorem Std.Internal.List.containsKey_minKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback : α} :
containsKey (minKeyD l fallback) l = true
theorem Std.Internal.List.minKeyD_le_of_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) {fallback : α} :
(compare (minKeyD l fallback) k).isLE = true
theorem Std.Internal.List.le_minKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k fallback : α} :
(compare k (minKeyD l fallback)).isLE = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
theorem Std.Internal.List.getKey?_minKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback : α} :
getKey? (minKeyD l fallback) l = some (minKeyD l fallback)
theorem Std.Internal.List.getKey_minKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {fallback : α} {he : containsKey (minKeyD l fallback) l = true} :
getKey (minKeyD l fallback) l he = minKeyD l fallback
theorem Std.Internal.List.getKey_minKeyD_eq_minKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {fallback : α} {he : containsKey (minKeyD l fallback) l = true} :
getKey (minKeyD l fallback) l he = minKey l
theorem Std.Internal.List.getKey!_minKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback : α} :
getKey! (minKeyD l fallback) l = minKeyD l fallback
theorem Std.Internal.List.getKeyD_minKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback fallback' : α} :
getKeyD (minKeyD l fallback) l fallback' = minKeyD l fallback
theorem Std.Internal.List.minKeyD_eraseKey_eq_iff_beq_minKey_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k fallback : α} (he : (eraseKey k l).isEmpty = false) :
minKeyD (eraseKey k l) fallback = minKeyD l fallback (k == minKeyD l fallback) = false
theorem Std.Internal.List.minKeyD_eraseKey_eq_iff_beq_minKeyD_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k fallback : α} (he : (eraseKey k l).isEmpty = false) :
minKeyD (eraseKey k l) fallback = minKeyD l fallback (k == minKeyD l fallback) = false
theorem Std.Internal.List.minKeyD_eraseKey_eq_of_beq_minKeyD_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k fallback : α} (he : (eraseKey k l).isEmpty = false) (heq : (k == minKeyD l fallback) = false) :
minKeyD (eraseKey k l) fallback = minKeyD l fallback
theorem Std.Internal.List.minKeyD_le_minKeyD_erase {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) {fallback : α} :
(compare (minKeyD l fallback) (minKeyD (eraseKey k l) fallback)).isLE = true
theorem Std.Internal.List.minKeyD_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
minKeyD (insertEntryIfNew k v l) fallback = (minKey? l).elim k fun (k' : α) => if compare k k' = Ordering.lt then k else k'
theorem Std.Internal.List.minKeyD_insertEntryIfNew_le_minKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} :
(compare (minKeyD (insertEntryIfNew k v l) fallback) (minKeyD l fallback)).isLE = true
theorem Std.Internal.List.minKeyD_insertEntryIfNew_le_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
(compare (minKeyD (insertEntryIfNew k v l) fallback) k).isLE = true
theorem Std.Internal.List.minKeyD_eq_headD_keys {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) {fallback : α} :
minKeyD l fallback = (keys l).headD fallback
theorem Std.Internal.List.minKeyD_modifyKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : β kβ k} {fallback : α} :
minKeyD (modifyKey k f l) fallback = minKeyD l fallback
theorem Std.Internal.List.minKeyD_alterKey_eq_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k)Option (β k)} {fallback : α} (he : (alterKey k f l).isEmpty = false) :
minKeyD (alterKey k f l) fallback = k (f (getValueCast? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
theorem Std.Internal.List.Const.minKeyD_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} (he : (modifyKey k f l).isEmpty = false) {fallback : α} :
minKeyD (modifyKey k f l) fallback = if (minKeyD l fallback == k) = true then k else minKeyD l fallback
theorem Std.Internal.List.Const.minKeyD_modifyKey_eq_minKeyD {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} {fallback : α} :
minKeyD (modifyKey k f l) fallback = minKeyD l fallback
theorem Std.Internal.List.Const.minKeyD_modifyKey_beq {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} {fallback : α} :
(minKeyD (modifyKey k f l) fallback == minKeyD l fallback) = true
theorem Std.Internal.List.Const.minKeyD_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : Option βOption β} (he : (alterKey k f l).isEmpty = false) {fallback : α} :
minKeyD (alterKey k f l) fallback = k (f (getValue? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k k').isLE = true
@[reducible, inline]
abbrev Std.Internal.List.maxKey? {α : Type u} {β : αType v} [Ord α] (xs : List ((a : α) × β a)) :

Returns the largest key in an associative list.

Equations
theorem Std.Internal.List.maxKey?_eq_some_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
maxKey? l = some k getKey? k l = some k ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
theorem Std.Internal.List.maxKey?_eq_some_iff_mem_and_forall {α : Type u} {β : αType v} [Ord α] [LawfulEqOrd α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
maxKey? l = some k containsKey k l = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
theorem Std.Internal.List.maxKey?_of_perm {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.maxKey?_eq_none_iff_isEmpty {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.maxKey?_of_isEmpty {α : Type u} {β : αType v} [Ord α] [TransOrd α] {l : List ((a : α) × β a)} (he : l.isEmpty = true) :
theorem Std.Internal.List.isNone_maxKey?_eq_isEmpty {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.isSome_maxKey?_eq_not_isEmpty {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.isSome_maxKey?_iff_isEmpty_eq_false {α : Type u} {β : αType v} [Ord α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.maxKey?_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
maxKey? (insertEntry k v l) = some ((maxKey? l).elim k fun (k' : α) => if (compare k' k).isLE = true then k else k')
theorem Std.Internal.List.isSome_maxKey?_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.isSome_maxKey?_of_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hc : containsKey k l = true) :
theorem Std.Internal.List.getKey?_maxKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} (hkm : maxKey? l = some km) :
getKey? km l = some km
theorem Std.Internal.List.getKey_maxKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} {hc : containsKey km l = true} (hkm : (maxKey? l).get = km) :
getKey km l hc = km
theorem Std.Internal.List.getKey!_maxKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} (hkm : maxKey? l = some km) :
getKey! km l = km
theorem Std.Internal.List.getKeyD_maxKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km fallback : α} (hkm : maxKey? l = some km) :
getKeyD km l fallback = km
theorem Std.Internal.List.maxKey?_bind_getKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
((maxKey? l).bind fun (k : α) => getKey? k l) = maxKey? l
theorem Std.Internal.List.containsKey_maxKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} (hkm : maxKey? l = some km) :
theorem Std.Internal.List.maxKey?_eraseKey_eq_iff_beq_maxKey?_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
maxKey? (eraseKey k l) = maxKey? l ∀ {km : α}, maxKey? l = some km → (k == km) = false
theorem Std.Internal.List.maxKey?_eraseKey_eq_of_beq_maxKey?_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hc : ∀ {km : α}, maxKey? l = some km → (k == km) = false) :
theorem Std.Internal.List.maxKey?_le_maxKey?_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km kmi : α} (hkm : maxKey? l = some km) (hkmi : (maxKey? (insertEntry k v l)).get = kmi) :
(compare km kmi).isLE = true
theorem Std.Internal.List.self_le_maxKey?_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {kmi : α} (hkmi : (maxKey? (insertEntry k v l)).get = kmi) :
(compare k kmi).isLE = true
theorem Std.Internal.List.maxKey?_le_of_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k km : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hc : containsKey k l = true) (hkm : (maxKey? l).get = km) :
theorem Std.Internal.List.maxKey?_le {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
(∀ (k' : α), maxKey? l = some k'(compare k' k).isLE = true) ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
theorem Std.Internal.List.isSome_maxKey?_of_isSome_maxKey?_eraseKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hs : (maxKey? (eraseKey k l)).isSome = true) :
theorem Std.Internal.List.containsKey_maxKey?_eraseKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {kme : α} (hkme : maxKey? (eraseKey k l) = some kme) :
theorem Std.Internal.List.maxKey?_eraseKey_le_maxKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k km kme : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hkme : maxKey? (eraseKey k l) = some kme) (hkm : (maxKey? l).get = km) :
(compare kme km).isLE = true
theorem Std.Internal.List.maxKey?_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
maxKey? (insertEntryIfNew k v l) = some ((maxKey? l).elim k fun (k' : α) => if compare k' k = Ordering.lt then k else k')
theorem Std.Internal.List.isSome_maxKey?_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.maxKey?_le_maxKey?_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km kmi : α} (hkm : maxKey? l = some km) (hkmi : (maxKey? (insertEntryIfNew k v l)).get = kmi) :
(compare km kmi).isLE = true
theorem Std.Internal.List.self_le_maxKey?_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k kmi : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hkmi : (maxKey? (insertEntryIfNew k v l)).get = kmi) :
(compare k kmi).isLE = true
theorem Std.Internal.List.reverse_keys {α : Type u} {β : αType v} {l : List ((a : α) × β a)} :
theorem Std.Internal.List.maxKey?_eq_getLast?_keys {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) :
theorem Std.Internal.List.maxKey?_modifyKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : β kβ k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.maxKey?_alterKey_eq_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : Option (β k)Option (β k)} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
maxKey? (alterKey k f l) = some k (f (getValueCast? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
theorem Std.Internal.List.Const.maxKey?_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : ββ} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
maxKey? (modifyKey k f l) = Option.map (fun (km : α) => if (km == k) = true then k else km) (maxKey? l)
theorem Std.Internal.List.Const.maxKey?_modifyKey_eq_maxKey? {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : ββ} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
theorem Std.Internal.List.Const.isSome_maxKey?_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : ββ} {l : List ((_ : α) × β)} :
theorem Std.Internal.List.Const.isSome_maxKey?_modifyKey_eq_isSome {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : ββ} {l : List ((_ : α) × β)} :
theorem Std.Internal.List.Const.maxKey?_modifyKey_beq {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : ββ} {km kmm : α} {l : List ((_ : α) × β)} (hd : DistinctKeys l) (hkm : maxKey? l = some km) (hkmm : (maxKey? (modifyKey k f l)).get = kmm) :
(kmm == km) = true
theorem Std.Internal.List.Const.maxKey?_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : Option βOption β} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
maxKey? (alterKey k f l) = some k (f (getValue? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
@[reducible, inline]
abbrev Std.Internal.List.maxKey {α : Type u} {β : αType v} [Ord α] (xs : List ((a : α) × β a)) (h : xs.isEmpty = false) :
α

Given a proof that the list is nonempty, returns the largest key in an associative list.

Equations
theorem Std.Internal.List.maxKey_of_perm {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} {hl : l.isEmpty = false} (hd : DistinctKeys l) (hp : l.Perm l') :
maxKey l hl = maxKey l'
theorem Std.Internal.List.maxKey_eq_get_maxKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} :
maxKey l he = (maxKey? l).get
theorem Std.Internal.List.maxKey?_eq_some_maxKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} :
maxKey? l = some (maxKey l he)
theorem Std.Internal.List.maxKey_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} {km : α} :
maxKey l he = km getKey? km l = some km ∀ (k : α), containsKey k l = true(compare k km).isLE = true
theorem Std.Internal.List.maxKey_eq_iff_mem_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} {km : α} :
maxKey l he = km containsKey km l = true ∀ (k : α), containsKey k l = true(compare k km).isLE = true
theorem Std.Internal.List.maxKey_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
maxKey (insertEntry k v l) = (maxKey? l).elim k fun (k' : α) => if (compare k' k).isLE = true then k else k'
theorem Std.Internal.List.maxKey_le_maxKey_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {he : l.isEmpty = false} :
(compare (maxKey l he) (maxKey (insertEntry k v l) )).isLE = true
theorem Std.Internal.List.self_le_maxKey_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
(compare k (maxKey (insertEntry k v l) )).isLE = true
theorem Std.Internal.List.containsKey_maxKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} :
theorem Std.Internal.List.le_maxKey_of_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) :
(compare k (maxKey l )).isLE = true
theorem Std.Internal.List.maxKey_le {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {he : l.isEmpty = false} :
(compare (maxKey l he) k).isLE = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
theorem Std.Internal.List.getKey?_maxKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} :
getKey? (maxKey l he) l = some (maxKey l he)
theorem Std.Internal.List.getKey_maxKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} :
getKey (maxKey l he) l = maxKey l he
theorem Std.Internal.List.getKey!_maxKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} :
getKey! (maxKey l he) l = maxKey l he
theorem Std.Internal.List.getKeyD_maxKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} {fallback : α} :
getKeyD (maxKey l he) l fallback = maxKey l he
theorem Std.Internal.List.maxKey_eraseKey_eq_iff_beq_maxKey_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {he : (eraseKey k l).isEmpty = false} :
maxKey (eraseKey k l) he = maxKey l (k == maxKey l ) = false
theorem Std.Internal.List.maxKey_eraseKey_eq_of_beq_maxKey_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {he : (eraseKey k l).isEmpty = false} (hc : (k == maxKey l ) = false) :
maxKey (eraseKey k l) he = maxKey l
theorem Std.Internal.List.maxKey_eraseKey_le_maxKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {he : (eraseKey k l).isEmpty = false} :
(compare (maxKey (eraseKey k l) he) (maxKey l )).isLE = true
theorem Std.Internal.List.maxKey_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
maxKey (insertEntryIfNew k v l) = (maxKey? l).elim k fun (k' : α) => if compare k' k = Ordering.lt then k else k'
theorem Std.Internal.List.maxKey_le_maxKey_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {he : l.isEmpty = false} :
theorem Std.Internal.List.self_le_maxKey_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.maxKey_eq_getLast_keys {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) {he : l.isEmpty = false} :
maxKey l he = (keys l).getLast
theorem Std.Internal.List.maxKey_modifyKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : β kβ k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : (modifyKey k f l).isEmpty = false} :
maxKey (modifyKey k f l) he = maxKey l
theorem Std.Internal.List.maxKey_alterKey_eq_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k)Option (β k)} {he : (alterKey k f l).isEmpty = false} :
maxKey (alterKey k f l) he = k (f (getValueCast? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
theorem Std.Internal.List.Const.maxKey_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} {he : (modifyKey k f l).isEmpty = false} :
maxKey (modifyKey k f l) he = if (maxKey l == k) = true then k else maxKey l
theorem Std.Internal.List.Const.maxKey_modifyKey_eq_maxKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} {he : (modifyKey k f l).isEmpty = false} :
maxKey (modifyKey k f l) he = maxKey l
theorem Std.Internal.List.Const.maxKey_modifyKey_beq {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} {he : (modifyKey k f l).isEmpty = false} :
(maxKey (modifyKey k f l) he == maxKey l ) = true
theorem Std.Internal.List.Const.maxKey_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : Option βOption β} {he : (alterKey k f l).isEmpty = false} :
maxKey (alterKey k f l) he = k (f (getValue? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
def Std.Internal.List.maxKey! {α : Type u} {β : αType v} [Ord α] [Inhabited α] (xs : List ((a : α) × β a)) :
α

Given a proof that the list is nonempty, returns the smallest key in an associative list.

Equations
theorem Std.Internal.List.maxKey!_of_perm {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l l' : List ((a : α) × β a)} (hd : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.maxKey!_eq_get!_maxKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.maxKey_eq_maxKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} :
theorem Std.Internal.List.maxKey?_eq_some_maxKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (he : l.isEmpty = false) :
theorem Std.Internal.List.maxKey!_eq_default {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (h : l.isEmpty = true) :
theorem Std.Internal.List.maxKey!_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km : α} :
maxKey! l = km getKey? km l = some km ∀ (k : α), containsKey k l = true(compare k km).isLE = true
theorem Std.Internal.List.maxKey!_eq_iff_mem_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km : α} :
maxKey! l = km containsKey km l = true ∀ (k : α), containsKey k l = true(compare k km).isLE = true
theorem Std.Internal.List.maxKey!_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
maxKey! (insertEntry k v l) = (maxKey? l).elim k fun (k' : α) => if (compare k' k).isLE = true then k else k'
theorem Std.Internal.List.maxKey!_le_maxKey!_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} :
theorem Std.Internal.List.self_le_maxKey!_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.containsKey_maxKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
theorem Std.Internal.List.le_maxKey!_of_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) :
theorem Std.Internal.List.maxKey!_le {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} :
(compare (maxKey! l) k).isLE = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
theorem Std.Internal.List.getKey?_maxKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
theorem Std.Internal.List.getKey_maxKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : containsKey (maxKey! l) l = true} :
getKey (maxKey! l) l he = maxKey! l
theorem Std.Internal.List.getKey_maxKey!_eq_maxKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : containsKey (maxKey! l) l = true} :
getKey (maxKey! l) l he = maxKey l
theorem Std.Internal.List.getKey!_maxKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
theorem Std.Internal.List.getKeyD_maxKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback : α} :
getKeyD (maxKey! l) l fallback = maxKey! l
theorem Std.Internal.List.maxKey!_eraseKey_eq_iff_beq_maxKey_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) :
theorem Std.Internal.List.maxKey!_eraseKey_eq_iff_beq_maxKey!_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) :
theorem Std.Internal.List.maxKey!_eraseKey_eq_of_beq_maxKey!_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) (heq : (k == maxKey! l) = false) :
theorem Std.Internal.List.maxKey!_erase_le_maxKey! {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) :
theorem Std.Internal.List.maxKey!_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
maxKey! (insertEntryIfNew k v l) = (maxKey? l).elim k fun (k' : α) => if compare k' k = Ordering.lt then k else k'
theorem Std.Internal.List.maxKey!_le_maxKey!_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} :
theorem Std.Internal.List.self_le_maxKey!_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.maxKey!_eq_getLast!_keys {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) :
theorem Std.Internal.List.maxKey!_modifyKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : β kβ k} :
theorem Std.Internal.List.maxKey!_alterKey_eq_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k)Option (β k)} (he : (alterKey k f l).isEmpty = false) :
maxKey! (alterKey k f l) = k (f (getValueCast? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
theorem Std.Internal.List.Const.maxKey!_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} (he : (modifyKey k f l).isEmpty = false) :
theorem Std.Internal.List.Const.maxKey!_modifyKey_eq_maxKey! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} :
theorem Std.Internal.List.Const.maxKey!_modifyKey_beq {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} :
theorem Std.Internal.List.Const.maxKey!_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : Option βOption β} (he : (alterKey k f l).isEmpty = false) :
maxKey! (alterKey k f l) = k (f (getValue? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
@[reducible, inline]
abbrev Std.Internal.List.maxKeyD {α : Type u} {β : αType v} [Ord α] (xs : List ((a : α) × β a)) (fallback : α) :
α

Returns the smallest key in an associative list or fallback if the list is empty.

Equations
theorem Std.Internal.List.maxKeyD_of_perm {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} {fallback : α} (hd : DistinctKeys l) (hp : l.Perm l') :
maxKeyD l fallback = maxKeyD l' fallback
theorem Std.Internal.List.maxKeyD_eq_getD_maxKey? {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} :
maxKeyD l fallback = (maxKey? l).getD fallback
theorem Std.Internal.List.maxKey_eq_maxKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {he : l.isEmpty = false} {fallback : α} :
maxKey l he = maxKeyD l fallback
theorem Std.Internal.List.maxKey?_eq_some_maxKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} (he : l.isEmpty = false) :
maxKey? l = some (maxKeyD l fallback)
theorem Std.Internal.List.maxKey!_eq_maxKeyD_default {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} :
theorem Std.Internal.List.maxKeyD_eq_fallback {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} (h : l.isEmpty = true) :
maxKeyD l fallback = fallback
theorem Std.Internal.List.maxKeyD_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km fallback : α} :
maxKeyD l fallback = km getKey? km l = some km ∀ (k : α), containsKey k l = true(compare k km).isLE = true
theorem Std.Internal.List.maxKeyD_eq_iff_mem_and_forall {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km fallback : α} :
maxKeyD l fallback = km containsKey km l = true ∀ (k : α), containsKey k l = true(compare k km).isLE = true
theorem Std.Internal.List.maxKeyD_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
maxKeyD (insertEntry k v l) fallback = (maxKey? l).elim k fun (k' : α) => if (compare k' k).isLE = true then k else k'
theorem Std.Internal.List.maxKeyD_le_maxKeyD_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} :
(compare (maxKeyD l fallback) (maxKeyD (insertEntry k v l) fallback)).isLE = true
theorem Std.Internal.List.self_le_maxKeyD_insertEntry {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
(compare k (maxKeyD (insertEntry k v l) fallback)).isLE = true
theorem Std.Internal.List.containsKey_maxKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback : α} :
containsKey (maxKeyD l fallback) l = true
theorem Std.Internal.List.le_maxKeyD_of_containsKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) {fallback : α} :
(compare k (maxKeyD l fallback)).isLE = true
theorem Std.Internal.List.maxKeyD_le {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k fallback : α} :
(compare (maxKeyD l fallback) k).isLE = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
theorem Std.Internal.List.getKey?_maxKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback : α} :
getKey? (maxKeyD l fallback) l = some (maxKeyD l fallback)
theorem Std.Internal.List.getKey_maxKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {fallback : α} {he : containsKey (maxKeyD l fallback) l = true} :
getKey (maxKeyD l fallback) l he = maxKeyD l fallback
theorem Std.Internal.List.getKey_maxKeyD_eq_maxKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {fallback : α} {he : containsKey (maxKeyD l fallback) l = true} :
getKey (maxKeyD l fallback) l he = maxKey l
theorem Std.Internal.List.getKey!_maxKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback : α} :
getKey! (maxKeyD l fallback) l = maxKeyD l fallback
theorem Std.Internal.List.getKeyD_maxKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback fallback' : α} :
getKeyD (maxKeyD l fallback) l fallback' = maxKeyD l fallback
theorem Std.Internal.List.maxKeyD_eraseKey_eq_iff_beq_maxKey_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k fallback : α} (he : (eraseKey k l).isEmpty = false) :
maxKeyD (eraseKey k l) fallback = maxKeyD l fallback (k == maxKeyD l fallback) = false
theorem Std.Internal.List.maxKeyD_eraseKey_eq_iff_beq_maxKeyD_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k fallback : α} (he : (eraseKey k l).isEmpty = false) :
maxKeyD (eraseKey k l) fallback = maxKeyD l fallback (k == maxKeyD l fallback) = false
theorem Std.Internal.List.maxKeyD_eraseKey_eq_of_beq_maxKeyD_eq_false {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k fallback : α} (he : (eraseKey k l).isEmpty = false) (heq : (k == maxKeyD l fallback) = false) :
maxKeyD (eraseKey k l) fallback = maxKeyD l fallback
theorem Std.Internal.List.maxKeyD_eraseKey_le_maxKeyD {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) {fallback : α} :
(compare (maxKeyD (eraseKey k l) fallback) (maxKeyD l fallback)).isLE = true
theorem Std.Internal.List.maxKeyD_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
maxKeyD (insertEntryIfNew k v l) fallback = (maxKey? l).elim k fun (k' : α) => if compare k' k = Ordering.lt then k else k'
theorem Std.Internal.List.maxKeyD_le_maxKeyD_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} :
(compare (maxKeyD l fallback) (maxKeyD (insertEntryIfNew k v l) fallback)).isLE = true
theorem Std.Internal.List.self_le_maxKeyD_insertEntryIfNew {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
(compare k (maxKeyD (insertEntryIfNew k v l) fallback)).isLE = true
theorem Std.Internal.List.maxKeyD_eq_getLastD_keys {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) {fallback : α} :
maxKeyD l fallback = (keys l).getLastD fallback
theorem Std.Internal.List.maxKeyD_modifyKey {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : β kβ k} {fallback : α} :
maxKeyD (modifyKey k f l) fallback = maxKeyD l fallback
theorem Std.Internal.List.maxKeyD_alterKey_eq_self {α : Type u} {β : αType v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k)Option (β k)} {fallback : α} (he : (alterKey k f l).isEmpty = false) :
maxKeyD (alterKey k f l) fallback = k (f (getValueCast? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true
theorem Std.Internal.List.Const.maxKeyD_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} (he : (modifyKey k f l).isEmpty = false) {fallback : α} :
maxKeyD (modifyKey k f l) fallback = if (maxKeyD l fallback == k) = true then k else maxKeyD l fallback
theorem Std.Internal.List.Const.maxKeyD_modifyKey_eq_maxKeyD {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} {fallback : α} :
maxKeyD (modifyKey k f l) fallback = maxKeyD l fallback
theorem Std.Internal.List.Const.maxKeyD_modifyKey_beq {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : ββ} {fallback : α} :
(maxKeyD (modifyKey k f l) fallback == maxKeyD l fallback) = true
theorem Std.Internal.List.Const.maxKeyD_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : Option βOption β} (he : (alterKey k f l).isEmpty = false) {fallback : α} :
maxKeyD (alterKey k f l) fallback = k (f (getValue? k l)).isSome = true ∀ (k' : α), containsKey k' l = true(compare k' k).isLE = true