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 : α} : Std.DHashMap.Internal.List.getEntry? a [] = none

theorem Std.DHashMap.Internal.List.getEntry?_cons {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} : Std.DHashMap.Internal.List.getEntry? a (⟨k, v⟩ :: l) = bif k == a then some ⟨k, v⟩ else Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.getEntry? a (⟨k, v⟩ :: l) = Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.getEntry? a l = Std.DHashMap.Internal.List.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 : α), (Std.DHashMap.Internal.List.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 : α), (Std.DHashMap.Internal.List.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 : α} : Std.DHashMap.Internal.List.getValue? a [] = none

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

@[simp]

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

theorem Std.DHashMap.Internal.List.getValue?_eq_getEntry? {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} : Std.DHashMap.Internal.List.getValue? a l = Option.map (fun (x : (_ : α) × β) => x.snd) (Std.DHashMap.Internal.List.getEntry? a l)

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

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

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) : Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.getValueCast? a (⟨k, v⟩ :: l) = Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.getValueCast? k (⟨k, v⟩ :: l) = some v

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

theorem Std.DHashMap.Internal.List.getValueCast?_eq_getEntry? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} : Std.DHashMap.Internal.List.getValueCast? a l = Std.DHashMap.Internal.List.Option.dmap (Std.DHashMap.Internal.List.getEntry? a l) fun (p : (a : α) × β a) (h : Std.DHashMap.Internal.List.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 : α} : (Std.DHashMap.Internal.List.getValueCast? a l).isSome = (Std.DHashMap.Internal.List.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 : α), (Std.DHashMap.Internal.List.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 : α} : Std.DHashMap.Internal.List.containsKey a [] = false

@[simp]

theorem Std.DHashMap.Internal.List.containsKey_cons {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} : Std.DHashMap.Internal.List.containsKey a (⟨k, v⟩ :: l) = (k == a || Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.containsKey a (⟨k, v⟩ :: l) = false ↔ (k == a) = false ∧ Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.containsKey a (⟨k, v⟩ :: l) = true ↔ (k == a) = true ∨ Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey a l = true) : Std.DHashMap.Internal.List.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₁ : Std.DHashMap.Internal.List.containsKey a (⟨k, v⟩ :: l) = true) (h₂ : (k == a) = false) : Std.DHashMap.Internal.List.containsKey a l = true

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

@[simp]

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

@[simp]

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

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

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

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

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

def Std.DHashMap.Internal.List.getEntry {α : Type u} {β : α → Type v} [BEq α] (a : α) (l : List ((a : α) × β a)) (h : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey a l = true) : Std.DHashMap.Internal.List.getEntry? a l = some (Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.getEntry? a l = some ⟨k, v⟩) {h' : Std.DHashMap.Internal.List.containsKey a l = true} : Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.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₁ : Std.DHashMap.Internal.List.containsKey a (⟨k, v⟩ :: l) = true} (h₂ : (k == a) = false) : Std.DHashMap.Internal.List.getEntry a (⟨k, v⟩ :: l) h₁ = Std.DHashMap.Internal.List.getEntry a l ⋯

def Std.DHashMap.Internal.List.getValue {α : Type u} {β : Type v} [BEq α] (a : α) (l : List ((_ : α) × β)) (h : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey a l = true) : Std.DHashMap.Internal.List.getValue? a l = some (Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.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 : β} : Std.DHashMap.Internal.List.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₁ : Std.DHashMap.Internal.List.containsKey a (⟨k, v⟩ :: l) = true} (h₂ : (k == a) = false) : Std.DHashMap.Internal.List.getValue a (⟨k, v⟩ :: l) h₁ = Std.DHashMap.Internal.List.getValue a l ⋯

theorem Std.DHashMap.Internal.List.getValue_cons {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {v : β} {h : Std.DHashMap.Internal.List.containsKey a (⟨k, v⟩ :: l) = true} : Std.DHashMap.Internal.List.getValue a (⟨k, v⟩ :: l) h = if h' : (k == a) = true then v else Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey a l = true} : Std.DHashMap.Internal.List.getValue a l h = Std.DHashMap.Internal.List.getValue b l ⋯

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

theorem Std.DHashMap.Internal.List.Option.get_congr {α : Type u} {o : Option α} {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 : Std.DHashMap.Internal.List.containsKey a (⟨k, v⟩ :: l) = true) : Std.DHashMap.Internal.List.getValueCast a (⟨k, v⟩ :: l) h = if h' : (k == a) = true then cast ⋯ v else Std.DHashMap.Internal.List.getValueCast a l ⋯

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

theorem Std.DHashMap.Internal.List.getValueCast!_eq_getValueCast? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] : Std.DHashMap.Internal.List.getValueCast! a l = (Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey a l = false) : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey a l = true) : Std.DHashMap.Internal.List.getValueCast a l h = Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey a l = true) : Std.DHashMap.Internal.List.getValueCast? a l = some (Std.DHashMap.Internal.List.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)] : Std.DHashMap.Internal.List.getValueCast! a l = Std.DHashMap.Internal.List.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 : β} : Std.DHashMap.Internal.List.getValueD a [] fallback = fallback

theorem Std.DHashMap.Internal.List.getValueD_eq_getValue? {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} : Std.DHashMap.Internal.List.getValueD a l fallback = (Std.DHashMap.Internal.List.getValue? a l).getD fallback

theorem Std.DHashMap.Internal.List.getValueD_eq_fallback {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} (h : Std.DHashMap.Internal.List.containsKey a l = false) : Std.DHashMap.Internal.List.getValueD a l fallback = fallback

theorem Std.DHashMap.Internal.List.getValue_eq_getValueD {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} (h : Std.DHashMap.Internal.List.containsKey a l = true) : Std.DHashMap.Internal.List.getValue a l h = Std.DHashMap.Internal.List.getValueD a l fallback

theorem Std.DHashMap.Internal.List.getValue?_eq_some_getValueD {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} (h : Std.DHashMap.Internal.List.containsKey a l = true) : Std.DHashMap.Internal.List.getValue? a l = some (Std.DHashMap.Internal.List.getValueD a l fallback)

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

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

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

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

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

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

theorem Std.DHashMap.Internal.List.getValue!_eq_getValueD_default {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} : Std.DHashMap.Internal.List.getValue! a l = Std.DHashMap.Internal.List.getValueD 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} : Std.DHashMap.Internal.List.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'} : Std.DHashMap.Internal.List.replaceEntry k v (⟨k', v'⟩ :: l) = bif k' == k then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey k l = false) : Std.DHashMap.Internal.List.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} : (Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey k l = false) : Std.DHashMap.Internal.List.getEntry? a (Std.DHashMap.Internal.List.replaceEntry k v l) = Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.getEntry? a (Std.DHashMap.Internal.List.replaceEntry k v l) = Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey k l = true) (h : (k == a) = true) : Std.DHashMap.Internal.List.getEntry? a (Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.getEntry? a (Std.DHashMap.Internal.List.replaceEntry k v l) = if Std.DHashMap.Internal.List.containsKey k l = true ∧ (k == a) = true then some ⟨k, v⟩ else Std.DHashMap.Internal.List.getEntry? a l

@[simp]

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

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

@[simp]

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

theorem Std.DHashMap.Internal.List.eraseKey_cons {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {k' : α} {v' : β k'} : Std.DHashMap.Internal.List.eraseKey k (⟨k', v'⟩ :: l) = bif k' == k then l else ⟨k', v'⟩ :: Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.eraseKey k (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: Std.DHashMap.Internal.List.eraseKey k l

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

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

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

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

@[simp]

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

@[simp]

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

theorem Std.DHashMap.Internal.List.keys_eq_map {α : Type u} {β : α → Type v} (l : List ((a : α) × β a)) : Std.DHashMap.Internal.List.keys l = List.map (fun (x : (a : α) × β a) => x.fst) l

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

@[simp]

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

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

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

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

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

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

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

theorem Std.DHashMap.Internal.List.DistinctKeys.containsKey_eq_false {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : Std.DHashMap.Internal.List.DistinctKeys (⟨k, v⟩ :: l) → Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey k l = false) : Std.DHashMap.Internal.List.DistinctKeys l → Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.DistinctKeys l) : p ∈ l ↔ Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.DistinctKeys (Std.DHashMap.Internal.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} : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey k l = true) : Std.DHashMap.Internal.List.insertEntry k v l = Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey k l = false) : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.DistinctKeys (Std.DHashMap.Internal.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} : (Std.DHashMap.Internal.List.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} : (Std.DHashMap.Internal.List.insertEntry k v l).length = if Std.DHashMap.Internal.List.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 ≤ (Std.DHashMap.Internal.List.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} : (Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.getValue? a (Std.DHashMap.Internal.List.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 : β} : Std.DHashMap.Internal.List.getValue? k (Std.DHashMap.Internal.List.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) : Std.DHashMap.Internal.List.getValue? a (Std.DHashMap.Internal.List.insertEntry k v l) = Std.DHashMap.Internal.List.getValue? a l

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

theorem Std.DHashMap.Internal.List.getValue?_insertEntry_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} : Std.DHashMap.Internal.List.getValue? k (Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.getEntry? a (Std.DHashMap.Internal.List.insertEntry k v l) = if (k == a) = true then some ⟨k, v⟩ else Std.DHashMap.Internal.List.getEntry? a l

theorem Std.DHashMap.Internal.List.getValueCast?_insertEntry {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} : Std.DHashMap.Internal.List.getValueCast? a (Std.DHashMap.Internal.List.insertEntry k v l) = if h : (k == a) = true then some (cast ⋯ v) else Std.DHashMap.Internal.List.getValueCast? a l

theorem Std.DHashMap.Internal.List.getValueCast?_insertEntry_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : Std.DHashMap.Internal.List.getValueCast? k (Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.getValueCast! a (Std.DHashMap.Internal.List.insertEntry k v l) = if h : (k == a) = true then cast ⋯ v else Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.getValueCast! k (Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.getValueCastD a (Std.DHashMap.Internal.List.insertEntry k v l) fallback = if h : (k == a) = true then cast ⋯ v else Std.DHashMap.Internal.List.getValueCastD a l fallback

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

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

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

theorem Std.DHashMap.Internal.List.getValueD_insertEntry_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {fallback : β} {v : β} : Std.DHashMap.Internal.List.getValueD k (Std.DHashMap.Internal.List.insertEntry k v l) fallback = v

@[simp]

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

@[simp]

theorem Std.DHashMap.Internal.List.containsKey_insertEntry_self {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : Std.DHashMap.Internal.List.containsKey k (Std.DHashMap.Internal.List.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₁ : Std.DHashMap.Internal.List.containsKey a (Std.DHashMap.Internal.List.insertEntry k v l) = true) (h₂ : (k == a) = false) : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey a (Std.DHashMap.Internal.List.insertEntry k v l) = true} : Std.DHashMap.Internal.List.getValueCast a (Std.DHashMap.Internal.List.insertEntry k v l) h = if h' : (k == a) = true then cast ⋯ v else Std.DHashMap.Internal.List.getValueCast a l ⋯

theorem Std.DHashMap.Internal.List.getValueCast_insertEntry_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : Std.DHashMap.Internal.List.getValueCast k (Std.DHashMap.Internal.List.insertEntry k v l) ⋯ = v

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

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

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 : Std.DHashMap.Internal.List.containsKey k l = true) : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey k l = false) : Std.DHashMap.Internal.List.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} : (Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.getEntry? a (Std.DHashMap.Internal.List.insertEntryIfNew k v l) = if (k == a && !Std.DHashMap.Internal.List.containsKey k l) = true then some ⟨k, v⟩ else Std.DHashMap.Internal.List.getEntry? a l

theorem Std.DHashMap.Internal.List.getValueCast?_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} : Std.DHashMap.Internal.List.getValueCast? a (Std.DHashMap.Internal.List.insertEntryIfNew k v l) = if h : (k == a) = true ∧ Std.DHashMap.Internal.List.containsKey k l = false then some (cast ⋯ v) else Std.DHashMap.Internal.List.getValueCast? a l

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

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

theorem Std.DHashMap.Internal.List.containsKey_insertEntryIfNew_self {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : Std.DHashMap.Internal.List.containsKey k (Std.DHashMap.Internal.List.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₁ : Std.DHashMap.Internal.List.containsKey a (Std.DHashMap.Internal.List.insertEntryIfNew k v l) = true) (h₂ : (k == a) = false) : Std.DHashMap.Internal.List.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₁ : Std.DHashMap.Internal.List.containsKey a (Std.DHashMap.Internal.List.insertEntryIfNew k v l) = true) (h₂ : ¬((k == a) = true ∧ Std.DHashMap.Internal.List.containsKey k l = false)) : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.containsKey a (Std.DHashMap.Internal.List.insertEntryIfNew k v l) = true} : Std.DHashMap.Internal.List.getValueCast a (Std.DHashMap.Internal.List.insertEntryIfNew k v l) h = if h' : (k == a) = true ∧ Std.DHashMap.Internal.List.containsKey k l = false then cast ⋯ v else Std.DHashMap.Internal.List.getValueCast a l ⋯

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

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

theorem Std.DHashMap.Internal.List.getValueD_insertEntryIfNew {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {fallback : β} {v : β} : Std.DHashMap.Internal.List.getValueD a (Std.DHashMap.Internal.List.insertEntryIfNew k v l) fallback = if (k == a) = true ∧ Std.DHashMap.Internal.List.containsKey k l = false then v else Std.DHashMap.Internal.List.getValueD a l fallback

theorem Std.DHashMap.Internal.List.length_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : (Std.DHashMap.Internal.List.insertEntryIfNew k v l).length = if Std.DHashMap.Internal.List.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 ≤ (Std.DHashMap.Internal.List.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} : (Std.DHashMap.Internal.List.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 : α} : Std.DHashMap.Internal.List.keys (Std.DHashMap.Internal.List.eraseKey k l) = (Std.DHashMap.Internal.List.keys l).erase k

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

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

theorem Std.DHashMap.Internal.List.getEntry?_eraseKey {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} (hl : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.getEntry? a (Std.DHashMap.Internal.List.eraseKey k l) = if (k == a) = true then none else Std.DHashMap.Internal.List.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)} : Std.DHashMap.Internal.List.keys (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = Std.DHashMap.Internal.List.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} : Std.DHashMap.Internal.List.keys (List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) l) = Std.DHashMap.Internal.List.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)} : Std.DHashMap.Internal.List.DistinctKeys l → Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.getValue? k (Std.DHashMap.Internal.List.eraseKey k l) = none

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

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

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

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

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

theorem Std.DHashMap.Internal.List.getValueCast?_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (hl : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.getValueCast? k (Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.getValueCast! a (Std.DHashMap.Internal.List.eraseKey k l) = if (k == a) = true then default else Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.getValueCast! k (Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.getValueCastD a (Std.DHashMap.Internal.List.eraseKey k l) fallback = if (k == a) = true then fallback else Std.DHashMap.Internal.List.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 : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.getValueCastD k (Std.DHashMap.Internal.List.eraseKey k l) fallback = fallback

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

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

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

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

theorem Std.DHashMap.Internal.List.getValueCast_eraseKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {h : Std.DHashMap.Internal.List.containsKey a (Std.DHashMap.Internal.List.eraseKey k l) = true} (hl : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.getValueCast a (Std.DHashMap.Internal.List.eraseKey k l) h = Std.DHashMap.Internal.List.getValueCast a l ⋯

theorem Std.DHashMap.Internal.List.getValue_eraseKey {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {h : Std.DHashMap.Internal.List.containsKey a (Std.DHashMap.Internal.List.eraseKey k l) = true} (hl : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.getValue a (Std.DHashMap.Internal.List.eraseKey k l) h = Std.DHashMap.Internal.List.getValue a l ⋯

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

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

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

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

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

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

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

theorem Std.DHashMap.Internal.List.getValue_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {l' : List ((_ : α) × β)} {a : α} {h' : Std.DHashMap.Internal.List.containsKey a l = true} (hl : Std.DHashMap.Internal.List.DistinctKeys l) (h : Std.DHashMap.Internal.List.Perm l l') : Std.DHashMap.Internal.List.getValue a l h' = Std.DHashMap.Internal.List.getValue a l' ⋯

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

theorem Std.DHashMap.Internal.List.getValueD_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {l' : List ((_ : α) × β)} {a : α} {fallback : β} (hl : Std.DHashMap.Internal.List.DistinctKeys l) (h : Std.DHashMap.Internal.List.Perm l l') : Std.DHashMap.Internal.List.getValueD a l fallback = Std.DHashMap.Internal.List.getValueD a l' fallback

theorem Std.DHashMap.Internal.List.perm_cons_getEntry {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {a : α} (h : Std.DHashMap.Internal.List.containsKey a l = true) : ∃ (l' : List ((a : α) × β a)), Std.DHashMap.Internal.List.Perm l (Std.DHashMap.Internal.List.getEntry a l h :: l')

theorem Std.DHashMap.Internal.List.getEntry?_ext {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} (hl : Std.DHashMap.Internal.List.DistinctKeys l) (hl' : Std.DHashMap.Internal.List.DistinctKeys l') (h : ∀ (a : α), Std.DHashMap.Internal.List.getEntry? a l = Std.DHashMap.Internal.List.getEntry? a l') : Std.DHashMap.Internal.List.Perm l l'

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

theorem Std.DHashMap.Internal.List.insertEntry_of_perm {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} {k : α} {v : β k} (hl : Std.DHashMap.Internal.List.DistinctKeys l) (h : Std.DHashMap.Internal.List.Perm l l') : Std.DHashMap.Internal.List.Perm (Std.DHashMap.Internal.List.insertEntry k v l) (Std.DHashMap.Internal.List.insertEntry k v l')

theorem Std.DHashMap.Internal.List.eraseKey_of_perm {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} {k : α} (hl : Std.DHashMap.Internal.List.DistinctKeys l) (h : Std.DHashMap.Internal.List.Perm l l') : Std.DHashMap.Internal.List.Perm (Std.DHashMap.Internal.List.eraseKey k l) (Std.DHashMap.Internal.List.eraseKey k l')

@[simp]

theorem Std.DHashMap.Internal.List.getEntry?_append {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} {a : α} : Std.DHashMap.Internal.List.getEntry? a (l ++ l') = (Std.DHashMap.Internal.List.getEntry? a l).or (Std.DHashMap.Internal.List.getEntry? a l')

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

@[simp]

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

theorem Std.DHashMap.Internal.List.containsKey_bind_eq_false {α : Type u} {β : α → Type v} [BEq α] {γ : Type w} {l : List γ} {f : γ → List ((a : α) × β a)} {a : α} (h : ∀ (i : Nat) (h : i < l.length), Std.DHashMap.Internal.List.containsKey a (f l[i]) = false) : Std.DHashMap.Internal.List.containsKey a (l.bind f) = false

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

@[simp]

theorem Std.DHashMap.Internal.List.getValue?_append {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {l' : List ((_ : α) × β)} {a : α} : Std.DHashMap.Internal.List.getValue? a (l ++ l') = (Std.DHashMap.Internal.List.getValue? a l).or (Std.DHashMap.Internal.List.getValue? a l')

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

theorem Std.DHashMap.Internal.List.getValue_append_of_containsKey_eq_false {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {l' : List ((_ : α) × β)} {a : α} {h' : Std.DHashMap.Internal.List.containsKey a (l ++ l') = true} (h : Std.DHashMap.Internal.List.containsKey a l' = false) : Std.DHashMap.Internal.List.getValue a (l ++ l') h' = Std.DHashMap.Internal.List.getValue a l ⋯

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

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

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

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

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

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

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