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.DHashMap.Internal.List.assoc_induction {α : Type u} {β : α → Type v} {motive : List ((a : α) × β a) → Prop} (nil : motive []) (cons : ∀ (k : α) (v : β k) (tail : List ((a : α) × β a)), motive tail → motive (⟨k, v⟩ :: tail)) (t : List ((a : α) × β a)) : motive t

def Std.DHashMap.Internal.List.getEntry? {α : Type u} {β : α → Type v} [BEq α] (a : α) : List ((a : α) × β a) → Option ((a : α) × β a)

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.getEntry? a [] = none
• Std.DHashMap.Internal.List.getEntry? a (⟨k, v⟩ :: l) = bif k == a then some ⟨k, v⟩ else Std.DHashMap.Internal.List.getEntry? a l

@[simp]

theorem Std.DHashMap.Internal.List.getEntry?_nil {α : Type u} {β : α → Type v} [BEq α] {a : α} : getEntry? a [] = none

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.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.DHashMap.Internal.List.getEntry?_congr {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α} (h : (a == b) = true) : getEntry? a l = getEntry? b l

theorem Std.DHashMap.Internal.List.isEmpty_eq_false_iff_exists_isSome_getEntry? {α : Type u} {β : α → Type v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} : l.isEmpty = false ↔ ∃ (a : α), (getEntry? a l).isSome = true

theorem Std.DHashMap.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.DHashMap.Internal.List.getValue? {α : Type u} {β : Type v} [BEq α] (a : α) : List ((_ : α) × β) → Option β

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.getValue? a [] = none
• Std.DHashMap.Internal.List.getValue? a (⟨k, v⟩ :: l) = bif k == a then some v else Std.DHashMap.Internal.List.getValue? a l

@[simp]

theorem Std.DHashMap.Internal.List.getValue?_nil {α : Type u} {β : Type v} [BEq α] {a : α} : getValue? a [] = none

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getValue?_cons_self {α : Type u} {β : Type v} [BEq α] [ReflBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} : getValue? k (⟨k, v⟩ :: l) = some v

theorem Std.DHashMap.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.DHashMap.Internal.List.getValue?_congr {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α} (h : (a == b) = true) : getValue? a l = getValue? b l

theorem Std.DHashMap.Internal.List.isEmpty_eq_false_iff_exists_isSome_getValue? {α : Type u} {β : Type v} [BEq α] [ReflBEq α] {l : List ((_ : α) × β)} : l.isEmpty = false ↔ ∃ (a : α), (getValue? a l).isSome = true

def Std.DHashMap.Internal.List.getValueCast? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) : List ((a : α) × β a) → Option (β a)

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.getValueCast? a [] = none
• Std.DHashMap.Internal.List.getValueCast? a (⟨k, v⟩ :: l) = if h : (k == a) = true then some (cast ⋯ v) else Std.DHashMap.Internal.List.getValueCast? a l

@[simp]

theorem Std.DHashMap.Internal.List.getValueCast?_nil {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} : getValueCast? a [] = none

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getValue?_eq_getValueCast? {α : Type u} [BEq α] [LawfulBEq α] {β : Type v} {l : List ((_ : α) × β)} {a : α} : getValue? a l = getValueCast? a l

theorem Std.DHashMap.Internal.List.getValueCast?_eq_getEntry? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} : getValueCast? a l = Std.DHashMap.Internal.List.Option.dmap✝ (getEntry? a l) fun (p : (a : α) × β a) (h : getEntry? a l = some p) => cast ⋯ p.snd

theorem Std.DHashMap.Internal.List.isSome_getValueCast?_eq_isSome_getEntry? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} : (getValueCast? a l).isSome = (getEntry? a l).isSome

theorem Std.DHashMap.Internal.List.isEmpty_eq_false_iff_exists_isSome_getValueCast? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} : l.isEmpty = false ↔ ∃ (a : α), (getValueCast? a l).isSome = true

def Std.DHashMap.Internal.List.containsKey {α : Type u} {β : α → Type v} [BEq α] (a : α) : List ((a : α) × β a) → Bool

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.containsKey a [] = false
• Std.DHashMap.Internal.List.containsKey a (⟨k, v⟩ :: l) = (k == a || Std.DHashMap.Internal.List.containsKey a l)

@[simp]

theorem Std.DHashMap.Internal.List.containsKey_nil {α : Type u} {β : α → Type v} [BEq α] {a : α} : containsKey a [] = false

@[simp]

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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) : containsKey a l = true

theorem Std.DHashMap.Internal.List.containsKey_eq_isSome_getEntry? {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {a : α} : containsKey a l = (getEntry? a l).isSome

theorem Std.DHashMap.Internal.List.isEmpty_eq_false_of_containsKey {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) : l.isEmpty = false

theorem Std.DHashMap.Internal.List.isEmpty_eq_false_iff_exists_containsKey {α : Type u} {β : α → Type v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} : l.isEmpty = false ↔ ∃ (a : α), containsKey a l = true

theorem Std.DHashMap.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.DHashMap.Internal.List.getEntry?_eq_none {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {a : α} : getEntry? a l = none ↔ containsKey a l = false

@[simp]

theorem Std.DHashMap.Internal.List.getValue?_eq_none {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} : getValue? a l = none ↔ containsKey a l = false

theorem Std.DHashMap.Internal.List.containsKey_eq_isSome_getValue? {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} : containsKey a l = (getValue? a l).isSome

theorem Std.DHashMap.Internal.List.containsKey_eq_isSome_getValueCast? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} : containsKey a l = (getValueCast? a l).isSome

theorem Std.DHashMap.Internal.List.getValueCast?_eq_none {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = false) : getValueCast? a l = none

theorem Std.DHashMap.Internal.List.containsKey_congr {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α} (h : (a == b) = true) : containsKey a l = containsKey b l

theorem Std.DHashMap.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) : containsKey b l = true

def Std.DHashMap.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

• Std.DHashMap.Internal.List.getEntry a l h = (Std.DHashMap.Internal.List.getEntry? a l).get ⋯

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getValue {α : Type u} {β : Type v} [BEq α] (a : α) (l : List ((_ : α) × β)) (h : containsKey a l = true) : β

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.getValue a l h = (Std.DHashMap.Internal.List.getValue? a l).get ⋯

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getValue_cons_self {α : Type u} {β : Type v} [BEq α] [ReflBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} : getValue k (⟨k, v⟩ :: l) ⋯ = v

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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

• Std.DHashMap.Internal.List.getValueCast a l h = (Std.DHashMap.Internal.List.getValueCast? a l).get ⋯

theorem Std.DHashMap.Internal.List.getValueCast?_eq_some_getValueCast {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) : getValueCast? a l = some (getValueCast a l h)

theorem Std.DHashMap.Internal.List.Option.get_congr {α : Type u} {o o' : Option α} {ho : o.isSome = true} (h : o = o') : o.get ho = o'.get ⋯

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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

• Std.DHashMap.Internal.List.getValueCastD a l fallback = (Std.DHashMap.Internal.List.getValueCast? a l).getD fallback

@[simp]

theorem Std.DHashMap.Internal.List.getValueCastD_nil {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {fallback : β a} : getValueCastD a [] fallback = fallback

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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

• Std.DHashMap.Internal.List.getValueCast! a l = (Std.DHashMap.Internal.List.getValueCast? a l).get!

@[simp]

theorem Std.DHashMap.Internal.List.getValueCast!_nil {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} [Inhabited (β a)] : getValueCast! a [] = default

theorem Std.DHashMap.Internal.List.getValueCast!_eq_getValueCast? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] : getValueCast! a l = (getValueCast? a l).get!

theorem Std.DHashMap.Internal.List.getValueCast!_eq_default {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (h : containsKey a l = false) : getValueCast! a l = default

theorem Std.DHashMap.Internal.List.getValueCast_eq_getValueCast! {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (h : containsKey a l = true) : getValueCast a l h = getValueCast! a l

theorem Std.DHashMap.Internal.List.getValueCast?_eq_some_getValueCast! {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (h : containsKey a l = true) : getValueCast? a l = some (getValueCast! a l)

theorem Std.DHashMap.Internal.List.getValueCast!_eq_getValueCastD_default {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] : getValueCast! a l = getValueCastD a l default

def Std.DHashMap.Internal.List.getValueD {α : Type u} {β : Type v} [BEq α] (a : α) (l : List ((_ : α) × β)) (fallback : β) : β

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.getValueD a l fallback = (Std.DHashMap.Internal.List.getValue? a l).getD fallback

@[simp]

theorem Std.DHashMap.Internal.List.getValueD_nil {α : Type u} {β : Type v} [BEq α] {a : α} {fallback : β} : getValueD a [] fallback = fallback

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getValue! {α : Type u} {β : Type v} [BEq α] [Inhabited β] (a : α) (l : List ((_ : α) × β)) : β

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.getValue! a l = (Std.DHashMap.Internal.List.getValue? a l).get!

@[simp]

theorem Std.DHashMap.Internal.List.getValue!_nil {α : Type u} {β : Type v} [BEq α] [Inhabited β] {a : α} : getValue! a [] = default

theorem Std.DHashMap.Internal.List.getValue!_eq_getValue? {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} : getValue! a l = (getValue? a l).get!

theorem Std.DHashMap.Internal.List.getValue!_eq_default {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} (h : containsKey a l = false) : getValue! a l = default

theorem Std.DHashMap.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.DHashMap.Internal.List.getValue?_eq_some_getValue! {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} (h : containsKey a l = true) : getValue? a l = some (getValue! a l)

theorem Std.DHashMap.Internal.List.getValue!_eq_getValueCast! {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} : getValue! a l = getValueCast! a l

theorem Std.DHashMap.Internal.List.getValue!_congr {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {a b : α} (hab : (a == b) = true) : getValue! a l = getValue! b l

theorem Std.DHashMap.Internal.List.getValue!_eq_getValueD_default {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} : getValue! a l = getValueD a l default

def Std.DHashMap.Internal.List.getKey? {α : Type u} {β : α → Type v} [BEq α] (a : α) : List ((a : α) × β a) → Option α

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.getKey? a [] = none
• Std.DHashMap.Internal.List.getKey? a (⟨k, v⟩ :: l) = bif k == a then some k else Std.DHashMap.Internal.List.getKey? a l

@[simp]

theorem Std.DHashMap.Internal.List.getKey?_nil {α : Type u} {β : α → Type v} [BEq α] {a : α} : getKey? a [] = none

@[simp]

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.containsKey_eq_isSome_getKey? {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {a : α} : containsKey a l = (getKey? a l).isSome

def Std.DHashMap.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

• Std.DHashMap.Internal.List.getKey a l h = (Std.DHashMap.Internal.List.getKey? a l).get ⋯

theorem Std.DHashMap.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.DHashMap.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 ⋯

def Std.DHashMap.Internal.List.getKeyD {α : Type u} {β : α → Type v} [BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α) : α

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.getKeyD a l fallback = (Std.DHashMap.Internal.List.getKey? a l).getD fallback

@[simp]

theorem Std.DHashMap.Internal.List.getKeyD_nil {α : Type u} {β : α → Type v} [BEq α] {a fallback : α} : getKeyD a [] fallback = fallback

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getKey! {α : Type u} {β : α → Type v} [BEq α] [Inhabited α] (a : α) (l : List ((a : α) × β a)) : α

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.getKey! a l = (Std.DHashMap.Internal.List.getKey? a l).get!

@[simp]

theorem Std.DHashMap.Internal.List.getKey!_nil {α : Type u} {β : α → Type v} [BEq α] [Inhabited α] {a : α} : getKey! a [] = default

theorem Std.DHashMap.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.DHashMap.Internal.List.getKey!_eq_default {α : Type u} {β : α → Type v} [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = false) : getKey! a l = default

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getKey!_eq_getKeyD_default {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} : getKey! a l = getKeyD a l default

def Std.DHashMap.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

• Std.DHashMap.Internal.List.replaceEntry k v [] = []
• Std.DHashMap.Internal.List.replaceEntry k v (⟨k_1, v_1⟩ :: l) = bif k_1 == k then ⟨k, v⟩ :: l else ⟨k_1, v_1⟩ :: Std.DHashMap.Internal.List.replaceEntry k v l

@[simp]

theorem Std.DHashMap.Internal.List.replaceEntry_nil {α : Type u} {β : α → Type v} [BEq α] {k : α} {v : β k} : replaceEntry k v [] = []

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.isEmpty_replaceEntry {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : (replaceEntry k v l).isEmpty = l.isEmpty

theorem Std.DHashMap.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) : getEntry? a (replaceEntry k v l) = getEntry? a l

theorem Std.DHashMap.Internal.List.getEntry?_replaceEntry_of_false {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} (h : (k == a) = false) : getEntry? a (replaceEntry k v l) = getEntry? a l

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.length_replaceEntry {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : (replaceEntry k v l).length = l.length

theorem Std.DHashMap.Internal.List.getValue?_replaceEntry_of_containsKey_eq_false {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (hl : containsKey k l = false) : getValue? a (replaceEntry k v l) = getValue? a l

theorem Std.DHashMap.Internal.List.getValue?_replaceEntry_of_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = false) : getValue? a (replaceEntry k v l) = getValue? a l

theorem Std.DHashMap.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) : getValue? a (replaceEntry k v l) = some v

theorem Std.DHashMap.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.DHashMap.Internal.List.getKey?_replaceEntry {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} : getKey? a (replaceEntry k v l) = if containsKey k l = true ∧ (k == a) = true then some k else getKey? a l

@[simp]

theorem Std.DHashMap.Internal.List.containsKey_replaceEntry {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} : containsKey a (replaceEntry k v l) = containsKey a l

def Std.DHashMap.Internal.List.eraseKey {α : Type u} {β : α → Type v} [BEq α] (k : α) : List ((a : α) × β a) → List ((a : α) × β a)

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.eraseKey k [] = []
• Std.DHashMap.Internal.List.eraseKey k (⟨k_1, v⟩ :: l) = bif k_1 == k then l else ⟨k_1, v⟩ :: Std.DHashMap.Internal.List.eraseKey k l

@[simp]

theorem Std.DHashMap.Internal.List.eraseKey_nil {α : Type u} {β : α → Type v} [BEq α] {k : α} : eraseKey k [] = []

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.sublist_eraseKey {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} : (eraseKey k l).Sublist l

theorem Std.DHashMap.Internal.List.length_eraseKey {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} : (eraseKey k l).length = if containsKey k l = true then l.length - 1 else l.length

theorem Std.DHashMap.Internal.List.length_eraseKey_le {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} : (eraseKey k l).length ≤ l.length

theorem Std.DHashMap.Internal.List.length_le_length_eraseKey {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} : l.length ≤ (eraseKey k l).length + 1

theorem Std.DHashMap.Internal.List.isEmpty_eraseKey {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} : (eraseKey k l).isEmpty = (l.isEmpty || l.length == 1 && containsKey k l)

@[simp]

theorem Std.DHashMap.Internal.List.keys_nil {α : Type u} {β : α → Type v} : keys [] = []

@[simp]

theorem Std.DHashMap.Internal.List.keys_cons {α : Type u} {β : α → Type v} {l : List ((a : α) × β a)} {k : α} {v : β k} : keys (⟨k, v⟩ :: l) = k :: keys l

theorem Std.DHashMap.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.DHashMap.Internal.List.length_keys_eq_length {α : Type u} {β : α → Type v} (l : List ((a : α) × β a)) : (keys l).length = l.length

theorem Std.DHashMap.Internal.List.isEmpty_keys_eq_isEmpty {α : Type u} {β : α → Type v} (l : List ((a : α) × β a)) : (keys l).isEmpty = l.isEmpty

theorem Std.DHashMap.Internal.List.containsKey_eq_keys_contains {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} : containsKey a l = (keys l).contains a

theorem Std.DHashMap.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.DHashMap.Internal.List.containsKey_of_mem {α : Type u} {β : α → Type v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a} (hp : p ∈ l) : containsKey p.fst l = true

@[simp]

theorem Std.DHashMap.Internal.List.DistinctKeys.nil {α : Type u} {β : α → Type v} [BEq α] : DistinctKeys []

theorem Std.DHashMap.Internal.List.DistinctKeys.perm_keys {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} (h : (keys l').Perm (keys l)) : DistinctKeys l → DistinctKeys l'

theorem Std.DHashMap.Internal.List.DistinctKeys.perm {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} (h : l'.Perm l) : DistinctKeys l → DistinctKeys l'

theorem Std.DHashMap.Internal.List.DistinctKeys.congr {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} (h : l.Perm l') : DistinctKeys l ↔ DistinctKeys l'

theorem Std.DHashMap.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)) : DistinctKeys l → DistinctKeys l'

theorem Std.DHashMap.Internal.List.distinctKeys_of_sublist {α : Type u} {β : α → Type v} [BEq α] {l l' : List ((a : α) × β a)} (h : l'.Sublist l) : DistinctKeys l → DistinctKeys l'

theorem Std.DHashMap.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') : DistinctKeys l → DistinctKeys l'

theorem Std.DHashMap.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.DHashMap.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

@[simp]

theorem Std.DHashMap.Internal.List.distinctKeys_cons_iff {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : DistinctKeys (⟨k, v⟩ :: l) ↔ DistinctKeys l ∧ containsKey k l = false

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.DistinctKeys.cons {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = false) : DistinctKeys l → DistinctKeys (⟨k, v⟩ :: l)

theorem Std.DHashMap.Internal.List.mem_iff_getEntry?_eq_some {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a} (h : DistinctKeys l) : p ∈ l ↔ getEntry? p.fst l = some p

theorem Std.DHashMap.Internal.List.DistinctKeys.replaceEntry {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : DistinctKeys l) : DistinctKeys (List.replaceEntry k v l)

def Std.DHashMap.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

• Std.DHashMap.Internal.List.insertEntry k v l = bif Std.DHashMap.Internal.List.containsKey k l then Std.DHashMap.Internal.List.replaceEntry k v l else ⟨k, v⟩ :: l

@[simp]

theorem Std.DHashMap.Internal.List.insertEntry_nil {α : Type u} {β : α → Type v} [BEq α] {k : α} {v : β k} : insertEntry k v [] = [⟨k, v⟩]

theorem Std.DHashMap.Internal.List.insertEntry_of_containsKey {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = true) : insertEntry k v l = replaceEntry k v l

theorem Std.DHashMap.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.DHashMap.Internal.List.DistinctKeys.insertEntry {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : DistinctKeys l) : DistinctKeys (List.insertEntry k v l)

@[simp]

theorem Std.DHashMap.Internal.List.isEmpty_insertEntry {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : (insertEntry k v l).isEmpty = false

theorem Std.DHashMap.Internal.List.length_insertEntry {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : (insertEntry k v l).length = if containsKey k l = true then l.length else l.length + 1

theorem Std.DHashMap.Internal.List.length_le_length_insertEntry {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : l.length ≤ (insertEntry k v l).length

theorem Std.DHashMap.Internal.List.length_insertEntry_le {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : (insertEntry k v l).length ≤ l.length + 1

theorem Std.DHashMap.Internal.List.getValue?_insertEntry_of_beq {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = true) : getValue? a (insertEntry k v l) = some v

theorem Std.DHashMap.Internal.List.getValue?_insertEntry_of_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} : getValue? k (insertEntry k v l) = some v

theorem Std.DHashMap.Internal.List.getValue?_insertEntry_of_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = false) : getValue? a (insertEntry k v l) = getValue? a l

theorem Std.DHashMap.Internal.List.getValue?_insertEntry {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} : getValue? a (insertEntry k v l) = if (k == a) = true then some v else getValue? a l

theorem Std.DHashMap.Internal.List.getValue?_insertEntry_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} : getValue? k (insertEntry k v l) = some v

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getValueCast?_insertEntry_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : getValueCast? k (insertEntry k v l) = some v

theorem Std.DHashMap.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.DHashMap.Internal.List.getValueCast!_insertEntry_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] {v : β k} : getValueCast! k (insertEntry k v l) = v

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getValue!_insertEntry {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k a : α} {v : β} : getValue! a (insertEntry k v l) = if (k == a) = true then v else getValue! a l

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getKey?_insertEntry_self {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : getKey? k (insertEntry k v l) = some k

theorem Std.DHashMap.Internal.List.getKey?_eq_none {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = false) : getKey? a l = none

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.containsKey_insertEntry {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : containsKey a (insertEntry k v l) = (k == a || containsKey a l)

theorem Std.DHashMap.Internal.List.containsKey_insertEntry_of_beq {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) : containsKey a (insertEntry k v l) = true

theorem Std.DHashMap.Internal.List.containsKey_insertEntry_self {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : containsKey k (insertEntry k v l) = true

theorem Std.DHashMap.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) : containsKey a l = true

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getValue_insertEntry_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} : getValue k (insertEntry k v l) ⋯ = v

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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

• Std.DHashMap.Internal.List.insertEntryIfNew k v l = bif Std.DHashMap.Internal.List.containsKey k l then l else ⟨k, v⟩ :: l

theorem Std.DHashMap.Internal.List.insertEntryIfNew_of_containsKey {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = true) : insertEntryIfNew k v l = l

theorem Std.DHashMap.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

@[simp]

theorem Std.DHashMap.Internal.List.isEmpty_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : (insertEntryIfNew k v l).isEmpty = false

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getValue?_insertEntryIfNew {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} : getValue? a (insertEntryIfNew k v l) = if (k == a) = true ∧ containsKey k l = false then some v else getValue? a l

theorem Std.DHashMap.Internal.List.containsKey_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : containsKey a (insertEntryIfNew k v l) = (k == a || containsKey a l)

theorem Std.DHashMap.Internal.List.containsKey_insertEntryIfNew_self {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : containsKey k (insertEntryIfNew k v l) = true

theorem Std.DHashMap.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) : containsKey a l = true

theorem Std.DHashMap.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)) : containsKey a l = true

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

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getValue!_insertEntryIfNew {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k a : α} {v : β} : getValue! a (insertEntryIfNew k v l) = if (k == a) = true ∧ containsKey k l = false then v else getValue! a l

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getKey?_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : getKey? a (insertEntryIfNew k v l) = if (k == a) = true ∧ containsKey k l = false then some k else getKey? a l

theorem Std.DHashMap.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.DHashMap.Internal.List.getKey!_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : getKey! a (insertEntryIfNew k v l) = if (k == a) = true ∧ containsKey k l = false then k else getKey! a l

theorem Std.DHashMap.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.DHashMap.Internal.List.length_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : (insertEntryIfNew k v l).length = if containsKey k l = true then l.length else l.length + 1

theorem Std.DHashMap.Internal.List.length_le_length_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : l.length ≤ (insertEntryIfNew k v l).length

theorem Std.DHashMap.Internal.List.length_insertEntryIfNew_le {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : (insertEntryIfNew k v l).length ≤ l.length + 1

@[simp]

theorem Std.DHashMap.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.DHashMap.Internal.List.DistinctKeys.eraseKey {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} : DistinctKeys l → DistinctKeys (List.eraseKey k l)

theorem Std.DHashMap.Internal.List.getEntry?_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} (h : DistinctKeys l) : getEntry? k (eraseKey k l) = none

theorem Std.DHashMap.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) : getEntry? a (eraseKey k l) = none

theorem Std.DHashMap.Internal.List.getEntry?_eraseKey_of_false {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hka : (k == a) = false) : getEntry? a (eraseKey k l) = getEntry? a l

theorem Std.DHashMap.Internal.List.getEntry?_eraseKey {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) : getEntry? a (eraseKey k l) = if (k == a) = true then none else getEntry? a l

theorem Std.DHashMap.Internal.List.keys_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β a → Option (γ 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.DHashMap.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.DHashMap.Internal.List.DistinctKeys.filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {f : (a : α) → β a → Option (γ a)} : DistinctKeys l → DistinctKeys (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l)

theorem Std.DHashMap.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.DHashMap.Internal.List.DistinctKeys.filter {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β a → Bool} (h : DistinctKeys l) : DistinctKeys (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l)

theorem Std.DHashMap.Internal.List.getValue?_eraseKey_self {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} (h : DistinctKeys l) : getValue? k (eraseKey k l) = none

theorem Std.DHashMap.Internal.List.getValue?_eraseKey_of_beq {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) (hka : (k == a) = true) : getValue? a (eraseKey k l) = none

theorem Std.DHashMap.Internal.List.getValue?_eraseKey_of_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} (hka : (k == a) = false) : getValue? a (eraseKey k l) = getValue? a l

theorem Std.DHashMap.Internal.List.getValue?_eraseKey {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) : getValue? a (eraseKey k l) = if (k == a) = true then none else getValue? a l

theorem Std.DHashMap.Internal.List.getKey?_eraseKey {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) : getKey? a (eraseKey k l) = if (k == a) = true then none else getKey? a l

theorem Std.DHashMap.Internal.List.getKey?_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) : getKey? k (eraseKey k l) = none

theorem Std.DHashMap.Internal.List.getKey!_eraseKey {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) : getKey! a (eraseKey k l) = if (k == a) = true then default else getKey! a l

theorem Std.DHashMap.Internal.List.getKey!_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) : getKey! k (eraseKey k l) = default

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.containsKey_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} (h : DistinctKeys l) : containsKey k (eraseKey k l) = false

theorem Std.DHashMap.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) : containsKey a (eraseKey k l) = false

theorem Std.DHashMap.Internal.List.containsKey_eraseKey_of_false {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hka : (k == a) = false) : containsKey a (eraseKey k l) = containsKey a l

theorem Std.DHashMap.Internal.List.containsKey_eraseKey {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) : containsKey a (eraseKey k l) = (!k == a && containsKey a l)

theorem Std.DHashMap.Internal.List.getValueCast?_eraseKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) : getValueCast? a (eraseKey k l) = if (k == a) = true then none else getValueCast? a l

theorem Std.DHashMap.Internal.List.getValueCast?_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) : getValueCast? k (eraseKey k l) = none

theorem Std.DHashMap.Internal.List.getValueCast!_eraseKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} [Inhabited (β a)] (hl : DistinctKeys l) : getValueCast! a (eraseKey k l) = if (k == a) = true then default else getValueCast! a l

theorem Std.DHashMap.Internal.List.getValueCast!_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (hl : DistinctKeys l) : getValueCast! k (eraseKey k l) = default

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getValue!_eraseKey {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) : getValue! a (eraseKey k l) = if (k == a) = true then default else getValue! a l

theorem Std.DHashMap.Internal.List.getValue!_eraseKey_self {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) : getValue! k (eraseKey k l) = default

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.containsKey_of_containsKey_eraseKey {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) : containsKey a (eraseKey k l) = true → containsKey a l = true

theorem Std.DHashMap.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) : getValueCast a (eraseKey k l) h = getValueCast a l ⋯

theorem Std.DHashMap.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.DHashMap.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.DHashMap.Internal.List.getEntry?_of_perm {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') : getEntry? a l = getEntry? a l'

theorem Std.DHashMap.Internal.List.containsKey_of_perm {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {k : α} (h : l.Perm l') : containsKey k l = containsKey k l'

theorem Std.DHashMap.Internal.List.getValueCast?_of_perm {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') : getValueCast? a l = getValueCast? a l'

theorem Std.DHashMap.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.DHashMap.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') : getValueCast! a l = getValueCast! a l'

theorem Std.DHashMap.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.DHashMap.Internal.List.getValue?_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') : getValue? a l = getValue? a l'

theorem Std.DHashMap.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.DHashMap.Internal.List.getValue!_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l l' : List ((_ : α) × β)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') : getValue! a l = getValue! a l'

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.Internal.List.containsKey_append {α : Type u} {β : α → Type v} [BEq α] {l l' : List ((a : α) × β a)} {a : α} : containsKey a (l ++ l') = (containsKey a l || containsKey a l')

theorem Std.DHashMap.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) : containsKey a (l.flatMap f) = false

theorem Std.DHashMap.Internal.List.containsKey_append_of_not_contains_right {α : Type u} {β : α → Type v} [BEq α] {l l' : List ((a : α) × β a)} {a : α} (hl' : containsKey a l' = false) : containsKey a (l ++ l') = containsKey a l

@[simp]

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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) : getValueCast? a (l ++ l') = getValueCast? a l

theorem Std.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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.DHashMap.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'