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

File contents: Verification of associative lists

theorem Std.Internal.List.assoc_induction {α : Type u} {β : α → Type v} {motive : List ((a : α) × β a) → Prop} (nil : motive []) (cons : ∀ (k : α) (v : β k) (tail : List ((a : α) × β a)), motive tail → motive (⟨k, v⟩ :: tail)) (t : List ((a : α) × β a)) : motive t

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

Internal implementation detail of the hash map

Equations

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

@[simp]

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

theorem Std.Internal.List.getEntry?_cons {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : getEntry? a (⟨k, v⟩ :: l) = bif k == a then some ⟨k, v⟩ else getEntry? a l

theorem Std.Internal.List.getEntry?_eq_find {α : Type u} {β : α → Type v} [BEq α] {k : α} {l : List ((a : α) × β a)} : getEntry? k l = List.find? (fun (x : (a : α) × β a) => x.fst == k) l

theorem Std.Internal.List.getEntry?_cons_of_true {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) : getEntry? a (⟨k, v⟩ :: l) = some ⟨k, v⟩

theorem Std.Internal.List.getEntry?_cons_of_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = false) : getEntry? a (⟨k, v⟩ :: l) = getEntry? a l

@[simp]

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

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

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

theorem Std.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.Internal.List.isEmpty_iff_forall_isSome_getEntry? {α : Type u} {β : α → Type v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} : l.isEmpty = true ↔ ∀ (a : α), (getEntry? a l).isSome = false

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

Internal implementation detail of the hash map

Equations

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

@[simp]

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

theorem Std.Internal.List.getValue?_cons {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} : getValue? a (⟨k, v⟩ :: l) = bif k == a then some v else getValue? a l

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

theorem Std.Internal.List.getValue?_cons_of_false {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = false) : getValue? a (⟨k, v⟩ :: l) = getValue? a l

@[simp]

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

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

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

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

Internal implementation detail of the hash map

Equations

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

@[simp]

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

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

theorem Std.Internal.List.getValueCast?_cons_of_true {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) : getValueCast? a (⟨k, v⟩ :: l) = some (cast ⋯ v)

theorem Std.Internal.List.getValueCast?_cons_of_false {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = false) : getValueCast? a (⟨k, v⟩ :: l) = getValueCast? a l

@[simp]

theorem Std.Internal.List.getValueCast?_cons_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : getValueCast? k (⟨k, v⟩ :: l) = some v

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

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

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

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

Internal implementation detail of the hash map

Equations

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

@[simp]

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

@[simp]

theorem Std.Internal.List.containsKey_cons {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : containsKey a (⟨k, v⟩ :: l) = (k == a || containsKey a l)

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

theorem Std.Internal.List.containsKey_cons_eq_true {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : containsKey a (⟨k, v⟩ :: l) = true ↔ (k == a) = true ∨ containsKey a l = true

theorem Std.Internal.List.containsKey_cons_of_beq {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) : containsKey a (⟨k, v⟩ :: l) = true

@[simp]

theorem Std.Internal.List.containsKey_cons_self {α : Type u} {β : α → Type v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : containsKey k (⟨k, v⟩ :: l) = true

theorem Std.Internal.List.containsKey_cons_of_containsKey {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : containsKey a l = true) : containsKey a (⟨k, v⟩ :: l) = true

theorem Std.Internal.List.containsKey_of_containsKey_cons {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (⟨k, v⟩ :: l) = true) (h₂ : (k == a) = false) : containsKey a l = true

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

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

theorem Std.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.Internal.List.isEmpty_iff_forall_containsKey {α : Type u} {β : α → Type v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} : l.isEmpty = true ↔ ∀ (a : α), containsKey a l = false

@[simp]

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

@[simp]

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

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

theorem Std.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.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.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.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.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.Internal.List.getEntry a l h = (Std.Internal.List.getEntry? a l).get ⋯

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

theorem Std.Internal.List.getEntry_eq_of_getEntry?_eq_some {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : getEntry? a l = some ⟨k, v⟩) {h' : containsKey a l = true} : getEntry a l h' = ⟨k, v⟩

theorem Std.Internal.List.getEntry_cons_of_beq {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) : getEntry a (⟨k, v⟩ :: l) ⋯ = ⟨k, v⟩

@[simp]

theorem Std.Internal.List.getEntry_cons_self {α : Type u} {β : α → Type v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : getEntry k (⟨k, v⟩ :: l) ⋯ = ⟨k, v⟩

theorem Std.Internal.List.getEntry_cons_of_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h₁ : containsKey a (⟨k, v⟩ :: l) = true} (h₂ : (k == a) = false) : getEntry a (⟨k, v⟩ :: l) h₁ = getEntry a l ⋯

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

Internal implementation detail of the hash map

Equations

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

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

theorem Std.Internal.List.getValue_cons_of_beq {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = true) : getValue a (⟨k, v⟩ :: l) ⋯ = v

@[simp]

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

theorem Std.Internal.List.getValue_cons_of_false {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} {h₁ : containsKey a (⟨k, v⟩ :: l) = true} (h₂ : (k == a) = false) : getValue a (⟨k, v⟩ :: l) h₁ = getValue a l ⋯

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

theorem Std.Internal.List.getValue_congr {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α} (hab : (a == b) = true) {h : containsKey a l = true} : getValue a l h = getValue b l ⋯

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

Internal implementation detail of the hash map

Equations

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

theorem Std.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.Internal.List.Option.get_congr {α : Type u} {o o' : Option α} {ho : o.isSome = true} (h : o = o') : o.get ho = o'.get ⋯

theorem Std.Internal.List.getValueCast_cons {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : containsKey a (⟨k, v⟩ :: l) = true) : getValueCast a (⟨k, v⟩ :: l) h = if h' : (k == a) = true then cast ⋯ v else getValueCast a l ⋯

theorem Std.Internal.List.getValue_eq_getValueCast {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] {l : List ((_ : α) × β)} {a : α} {h : containsKey a l = true} : getValue a l h = getValueCast a l h

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

Internal implementation detail of the hash map

Equations

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

@[simp]

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

theorem Std.Internal.List.getValueCastD_eq_getValueCast? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {fallback : β a} : getValueCastD a l fallback = (getValueCast? a l).getD fallback

theorem Std.Internal.List.getValueCastD_eq_fallback {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {fallback : β a} (h : containsKey a l = false) : getValueCastD a l fallback = fallback

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

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

def Std.Internal.List.getValueCast! {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) [Inhabited (β a)] (l : List ((a : α) × β a)) : β a

Internal implementation detail of the hash map

Equations

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

@[simp]

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

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

Internal implementation detail of the hash map

Equations

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

@[simp]

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

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

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

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

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

theorem Std.Internal.List.getValueD_eq_getValueCastD {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} : getValueD a l fallback = getValueCastD a l fallback

theorem Std.Internal.List.getValueD_congr {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α} {fallback : β} (hab : (a == b) = true) : getValueD a l fallback = getValueD b l fallback

def Std.Internal.List.getValue! {α : Type u} {β : Type v} [BEq α] [Inhabited β] (a : α) (l : List ((_ : α) × β)) : β

Internal implementation detail of the hash map

Equations

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

@[simp]

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

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

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

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

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

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

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

Internal implementation detail of the hash map

Equations

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

@[simp]

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

@[simp]

theorem Std.Internal.List.getKey?_cons {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : getKey? a (⟨k, v⟩ :: l) = bif k == a then some k else getKey? a l

theorem Std.Internal.List.getKey?_cons_of_true {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) : getKey? a (⟨k, v⟩ :: l) = some k

theorem Std.Internal.List.getKey?_cons_of_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = false) : getKey? a (⟨k, v⟩ :: l) = getKey? a l

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

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

theorem Std.Internal.List.getEntry?_eq_some_iff_getKey?_eq_some_getValue?_eq_some {α : Type u} [BEq α] {β : Type v} {l : List ((_ : α) × β)} {k k' : α} {v : β} : getEntry? k l = some ⟨k', v⟩ ↔ getKey? k l = some k' ∧ getValue? k l = some v

def Std.Internal.List.getKey {α : Type u} {β : α → Type v} [BEq α] (a : α) (l : List ((a : α) × β a)) (h : containsKey a l = true) : α

Internal implementation detail of the hash map

Equations

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

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

theorem Std.Internal.List.getKey_cons {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (⟨k, v⟩ :: l) = true} : getKey a (⟨k, v⟩ :: l) h = if h' : (k == a) = true then k else getKey a l ⋯

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

Internal implementation detail of the hash map

Equations

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

@[simp]

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

theorem Std.Internal.List.getKeyD_eq_getKey? {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {a fallback : α} : getKeyD a l fallback = (getKey? a l).getD fallback

theorem Std.Internal.List.getKeyD_eq_fallback {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α} (h : containsKey a l = false) : getKeyD a l fallback = fallback

theorem Std.Internal.List.getKey_eq_getKeyD {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α} (h : containsKey a l = true) : getKey a l h = getKeyD a l fallback

theorem Std.Internal.List.getKey?_eq_some_getKeyD {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α} (h : containsKey a l = true) : getKey? a l = some (getKeyD a l fallback)

def Std.Internal.List.getKey! {α : Type u} {β : α → Type v} [BEq α] [Inhabited α] (a : α) (l : List ((a : α) × β a)) : α

Internal implementation detail of the hash map

Equations

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

@[simp]

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

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

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

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

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

theorem Std.Internal.List.getKey!_eq_getKeyD_default {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} : getKey! a l = getKeyD a l default

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

Internal implementation detail of the hash map

Equations

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

@[simp]

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

theorem Std.Internal.List.replaceEntry_cons {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} : replaceEntry k v (⟨k', v'⟩ :: l) = bif k' == k then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: replaceEntry k v l

theorem Std.Internal.List.replaceEntry_cons_of_true {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} (h : (k' == k) = true) : replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k, v⟩ :: l

theorem Std.Internal.List.replaceEntry_cons_of_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} (h : (k' == k) = false) : replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: replaceEntry k v l

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

@[simp]

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

theorem Std.Internal.List.mem_replaceEntry_of_beq_eq_false {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : (p.fst == a) = false) : p ∈ replaceEntry a b l ↔ p ∈ l

theorem Std.Internal.List.mem_replaceEntry_of_key_ne {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.fst ≠ a) : p ∈ replaceEntry a b l ↔ p ∈ l

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

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

theorem Std.Internal.List.getEntry?_replaceEntry_of_true {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} (hl : containsKey k l = true) (h : (k == a) = true) : getEntry? a (replaceEntry k v l) = some ⟨k, v⟩

theorem Std.Internal.List.getEntry?_replaceEntry {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} : getEntry? a (replaceEntry k v l) = if containsKey k l = true ∧ (k == a) = true then some ⟨k, v⟩ else getEntry? a l

@[simp]

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

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

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

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

@[simp]

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

Internal implementation detail of the hash map

Equations

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

@[simp]

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

theorem Std.Internal.List.eraseKey_cons {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'} : eraseKey k (⟨k', v'⟩ :: l) = bif k' == k then l else ⟨k', v'⟩ :: eraseKey k l

theorem Std.Internal.List.eraseKey_cons_of_beq {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'} (h : (k' == k) = true) : eraseKey k (⟨k', v'⟩ :: l) = l

@[simp]

theorem Std.Internal.List.eraseKey_cons_self {α : Type u} {β : α → Type v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : eraseKey k (⟨k, v⟩ :: l) = l

theorem Std.Internal.List.eraseKey_cons_of_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'} (h : (k' == k) = false) : eraseKey k (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: eraseKey k l

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

theorem Std.Internal.List.mem_eraseKey_of_key_beq_eq_false {α : Type u} {β : α → Type v} [BEq α] {a : α} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : (p.fst == a) = false) : p ∈ eraseKey a l ↔ p ∈ l

theorem Std.Internal.List.mem_eraseKey_of_key_ne {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.fst ≠ a) : p ∈ eraseKey a l ↔ p ∈ l

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

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

theorem Std.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.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.Internal.List.keys_nil {α : Type u} {β : α → Type v} : keys [] = []

@[simp]

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

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

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

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

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

theorem Std.Internal.List.containsKey_of_mem {α : Type u} {β : α → Type v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a} (hp : p ∈ l) : containsKey p.fst l = true

@[simp]

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

theorem Std.Internal.List.DistinctKeys.def {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} : DistinctKeys l ↔ List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l

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

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

theorem Std.Internal.List.containsKey_eq_false_iff_forall_mem_keys {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} : containsKey a l = false ↔ ∀ (a' : α), a' ∈ keys l → (a == a') = false

theorem Std.Internal.List.containsKey_eq_false_iff {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} : containsKey a l = false ↔ ∀ (b : (a : α) × β a), b ∈ l → (a == b.fst) = false

@[simp]

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

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

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

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

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

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

theorem Std.Internal.List.getEntry?_of_mem {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} (hl : DistinctKeys l) {k k' : α} (hk : (k == k') = true) {v : β k} (hkv : ⟨k, v⟩ ∈ l) : getEntry? k' l = some ⟨k, v⟩

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

Internal implementation detail of the hash map

Equations

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

@[simp]

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

theorem Std.Internal.List.insertEntry_cons_of_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} (h : (k' == k) = false) : (insertEntry k v (⟨k', v'⟩ :: l)).Perm (⟨k', v'⟩ :: insertEntry k v l)

theorem Std.Internal.List.insertEntry_cons_of_beq {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} (h : (k' == k) = true) : insertEntry k v (⟨k', v'⟩ :: l) = ⟨k, v⟩ :: l

@[simp]

theorem Std.Internal.List.insertEntry_cons_self {α : Type u} {β : α → Type v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : insertEntry k v (⟨k, v⟩ :: l) = ⟨k, v⟩ :: l

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

theorem Std.Internal.List.insertEntry_of_containsKey_eq_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = false) : insertEntry k v l = ⟨k, v⟩ :: l

theorem Std.Internal.List.mem_insertEntry_of_key_beq_eq_false {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : (p.fst == a) = false) : p ∈ insertEntry a b l ↔ p ∈ l

theorem Std.Internal.List.mem_insertEntry_of_key_ne {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.fst ≠ a) : p ∈ insertEntry a b l ↔ p ∈ l

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

@[simp]

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

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

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

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

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

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

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

theorem Std.Internal.List.getValueCastD_insertEntry_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback v : β k} : getValueCastD k (insertEntry k v l) fallback = v

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

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

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

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

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

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

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

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

theorem Std.Internal.List.getKeyD_insertEntry {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α} {v : β k} : getKeyD a (insertEntry k v l) fallback = if (k == a) = true then k else getKeyD a l fallback

theorem Std.Internal.List.getKeyD_insertEntry_self {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k fallback : α} {v : β k} : getKeyD k (insertEntry k v l) fallback = k

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

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

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

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

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

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

theorem Std.Internal.List.getKey_insertEntry {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (insertEntry k v l) = true} : getKey a (insertEntry k v l) h = if h' : (k == a) = true then k else getKey a l ⋯

theorem Std.Internal.List.getKey_insertEntry_self {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : getKey k (insertEntry k v l) ⋯ = k

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

Internal implementation detail of the hash map

Equations

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

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

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

@[simp]

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

theorem Std.Internal.List.getEntry?_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : getEntry? a (insertEntryIfNew k v l) = if (k == a && !containsKey k l) = true then some ⟨k, v⟩ else getEntry? a l

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

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

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

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

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

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

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

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

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

theorem Std.Internal.List.getKey_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (insertEntryIfNew k v l) = true} : getKey a (insertEntryIfNew k v l) h = if h' : (k == a) = true ∧ containsKey k l = false then k else getKey a l ⋯

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Std.Internal.List.getValueCastD_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (hl : DistinctKeys l) : getValueCastD k (eraseKey k l) fallback = fallback

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

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

theorem Std.Internal.List.getValueD_eraseKey_self {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} {fallback : β} (hl : DistinctKeys l) : getValueD k (eraseKey k l) fallback = fallback

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

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

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

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

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

theorem Std.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.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.Internal.List.getValueCast_of_perm {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} {h' : containsKey a l = true} (hl : DistinctKeys l) (h : l.Perm l') : getValueCast a l h' = getValueCast a l' ⋯

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

theorem Std.Internal.List.mem_iff_getValueCast?_eq_some {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {v : β k} {l : List ((a : α) × β a)} (h : DistinctKeys l) : ⟨k, v⟩ ∈ l ↔ getValueCast? k l = some v

theorem Std.Internal.List.find?_eq_some_iff_getValueCast?_eq_some {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : DistinctKeys l) : List.find? (fun (x : (a : α) × β a) => x.fst == k) l = some ⟨k, v⟩ ↔ getValueCast? k l = some v

theorem Std.Internal.List.find?_eq_none_iff_containsKey_eq_false {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} : List.find? (fun (x : (a : α) × β a) => x.fst == k) l = none ↔ containsKey k l = false

theorem Std.Internal.List.pairwise_fst_eq_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} (h : DistinctKeys l) : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l

theorem Std.Internal.List.map_fst_map_toProd_eq_keys {α : Type u} {β : Type v} {l : List ((_ : α) × β)} : List.map Prod.fst (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l) = keys l

theorem Std.Internal.List.find?_map_eq_none_iff_containsKey_eq_false {α : Type u} [BEq α] [PartialEquivBEq α] {β : Type v} {l : List ((_ : α) × β)} {k : α} : List.find? (fun (x : α × β) => x.fst == k) (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l) = none ↔ containsKey k l = false

theorem Std.Internal.List.mem_map_toProd_iff_mem {α : Type u} {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} : ⟨k, v⟩ ∈ l ↔ (k, v) ∈ List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l

theorem Std.Internal.List.mem_iff_getValue?_eq_some {α : Type u} [BEq α] [LawfulBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) : ⟨k, v⟩ ∈ l ↔ getValue? k l = some v

theorem Std.Internal.List.mem_map_toProd_iff_getValue?_eq_some {α : Type u} [BEq α] [LawfulBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) : (k, v) ∈ List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l ↔ getValue? k l = some v

theorem Std.Internal.List.find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {k k' : α} {v : β} {l : List ((_ : α) × β)} : List.find? (fun (a : α × β) => a.fst == k) (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l) = some (k', v) ↔ getKey? k l = some k' ∧ getValue? k l = some v

theorem Std.Internal.List.mem_iff_getKey?_eq_some_and_getValue?_eq_some {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) : ⟨k, v⟩ ∈ l ↔ getKey? k l = some k ∧ getValue? k l = some v

theorem Std.Internal.List.getValue?_eq_some_iff_exists_beq_and_mem_toList {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} (h : DistinctKeys l) : getValue? k l = some v ↔ ∃ (k' : α), (k == k') = true ∧ (k', v) ∈ List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l

theorem Std.Internal.List.mem_map_toProd_iff_getKey?_eq_some_and_getValue?_eq_some {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) : (k, v) ∈ List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l ↔ getKey? k l = some k ∧ getValue? k l = some v

theorem Std.Internal.List.pairwise_fst_eq_false_map_toProd {α : Type u} [BEq α] {β : Type v} {l : List ((_ : α) × β)} (h : DistinctKeys l) : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)

theorem Std.Internal.List.foldlM_eq_foldlM_toProd {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × β)} {f : δ → α → β → m' δ} {init : δ} : List.foldlM (fun (a : δ) (b : (_ : α) × β) => f a b.fst b.snd) init l = List.foldlM (fun (a : δ) (b : α × β) => f a b.fst b.snd) init (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)

theorem Std.Internal.List.foldl_eq_foldl_toProd {α : Type u} {β : Type v} {δ : Type w} {l : List ((_ : α) × β)} {f : δ → α → β → δ} {init : δ} : List.foldl (fun (a : δ) (b : (_ : α) × β) => f a b.fst b.snd) init l = List.foldl (fun (a : δ) (b : α × β) => f a b.fst b.snd) init (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)

theorem Std.Internal.List.foldrM_eq_foldrM_toProd {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × β)} {f : δ → α → β → m' δ} {init : δ} : List.foldrM (fun (a : (_ : α) × β) (b : δ) => f b a.fst a.snd) init l = List.foldrM (fun (a : α × β) (b : δ) => f b a.fst a.snd) init (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)

theorem Std.Internal.List.foldr_eq_foldr_toProd {α : Type u} {β : Type v} {δ : Type w} {l : List ((_ : α) × β)} {f : δ → α → β → δ} {init : δ} : List.foldr (fun (a : (_ : α) × β) (b : δ) => f b a.fst a.snd) init l = List.foldr (fun (a : α × β) (b : δ) => f b a.fst a.snd) init (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l)

theorem Std.Internal.List.forM_eq_forM_toProd {α : Type u} {β : Type v} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × β)} {f : α → β → m' PUnit} : (forM l fun (a : (_ : α) × β) => f a.fst a.snd) = forM (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l) fun (a : α × β) => f a.fst a.snd

theorem Std.Internal.List.forIn_eq_forIn_toProd {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × β)} {f : α → β → δ → m' (ForInStep δ)} {init : δ} : (forIn l init fun (a : (_ : α) × β) (d : δ) => f a.fst a.snd d) = forIn (List.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l) init fun (a : α × β) (d : δ) => f a.fst a.snd d

theorem Std.Internal.List.foldlM_eq_foldlM_keys {α : Type u} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × Unit)} {f : δ → α → m' δ} {init : δ} : List.foldlM (fun (a : δ) (b : (_ : α) × Unit) => f a b.fst) init l = List.foldlM f init (keys l)

theorem Std.Internal.List.foldl_eq_foldl_keys {α : Type u} {δ : Type w} {l : List ((_ : α) × Unit)} {f : δ → α → δ} {init : δ} : List.foldl (fun (a : δ) (b : (_ : α) × Unit) => f a b.fst) init l = List.foldl f init (keys l)

theorem Std.Internal.List.foldrM_eq_foldrM_keys {α : Type u} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × Unit)} {f : δ → α → m' δ} {init : δ} : List.foldrM (fun (a : (_ : α) × Unit) (b : δ) => f b a.fst) init l = List.foldrM (fun (a : α) (b : δ) => f b a) init (keys l)

theorem Std.Internal.List.foldr_eq_foldr_keys {α : Type u} {δ : Type w} {l : List ((_ : α) × Unit)} {f : δ → α → δ} {init : δ} : List.foldr (fun (a : (_ : α) × Unit) (b : δ) => f b a.fst) init l = List.foldr (fun (a : α) (b : δ) => f b a) init (keys l)

theorem Std.Internal.List.forM_eq_forM_keys {α : Type u} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × Unit)} {f : α → m' PUnit} : (l.forM fun (a : (_ : α) × Unit) => f a.fst) = (keys l).forM f

theorem Std.Internal.List.forIn_eq_forIn_keys {α : Type u} {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ} {l : List ((_ : α) × Unit)} : (forIn l init fun (a : (_ : α) × Unit) (d : δ) => f a.fst d) = forIn (keys l) init f

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

Internal implementation detail of the hash map

Equations

• Std.Internal.List.insertList l [] = l
• Std.Internal.List.insertList l (⟨k, v⟩ :: l_1) = Std.Internal.List.insertList (Std.Internal.List.insertEntry k v l) l_1

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

theorem Std.Internal.List.insertList_perm_of_perm_first {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l1 l2 toInsert : List ((a : α) × β a)} (h : l1.Perm l2) (distinct : DistinctKeys l1) : (insertList l1 toInsert).Perm (insertList l2 toInsert)

theorem Std.Internal.List.insertList_cons_perm {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {p : (a : α) × β a} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys (p :: l₂)) : (insertList l₁ (p :: l₂)).Perm (insertEntry p.fst p.snd (insertList l₁ l₂))

theorem Std.Internal.List.getEntry?_insertList {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (k : α) : getEntry? k (insertList l toInsert) = (getEntry? k toInsert).or (getEntry? k l)

theorem Std.Internal.List.getEntry?_insertList_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : containsKey k toInsert = false) : getEntry? k (insertList l toInsert) = getEntry? k l

theorem Std.Internal.List.getEntry?_insertList_of_contains_eq_true {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (contains : containsKey k toInsert = true) : getEntry? k (insertList l toInsert) = getEntry? k toInsert

theorem Std.Internal.List.containsKey_insertList {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} : containsKey k (insertList l toInsert) = (containsKey k l || (List.map Sigma.fst toInsert).contains k)

theorem Std.Internal.List.containsKey_of_containsKey_insertList {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (h₁ : containsKey k (insertList l toInsert) = true) (h₂ : (List.map Sigma.fst toInsert).contains k = false) : containsKey k l = true

theorem Std.Internal.List.getValueCast?_insertList_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : (List.map Sigma.fst toInsert).contains k = false) : getValueCast? k (insertList l toInsert) = getValueCast? k l

theorem Std.Internal.List.getValueCast?_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert) : getValueCast? k' (insertList l toInsert) = some (cast ⋯ v)

theorem Std.Internal.List.getValueCast_insertList_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : (List.map Sigma.fst toInsert).contains k = false) {h : containsKey k (insertList l toInsert) = true} : getValueCast k (insertList l toInsert) h = getValueCast k l ⋯

theorem Std.Internal.List.getValueCast_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (v : β k) (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert) {h : containsKey k' (insertList l toInsert) = true} : getValueCast k' (insertList l toInsert) h = cast ⋯ v

theorem Std.Internal.List.getValueCast!_insertList_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (not_contains : (List.map Sigma.fst toInsert).contains k = false) : getValueCast! k (insertList l toInsert) = getValueCast! k l

theorem Std.Internal.List.getValueCast!_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (v : β k) [Inhabited (β k')] (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert) : getValueCast! k' (insertList l toInsert) = cast ⋯ v

theorem Std.Internal.List.getValueCastD_insertList_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} {fallback : β k} (not_mem : (List.map Sigma.fst toInsert).contains k = false) : getValueCastD k (insertList l toInsert) fallback = getValueCastD k l fallback

theorem Std.Internal.List.getValueCastD_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert) : getValueCastD k' (insertList l toInsert) fallback = cast ⋯ v

theorem Std.Internal.List.getKey?_insertList_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : (List.map Sigma.fst toInsert).contains k = false) : getKey? k (insertList l toInsert) = getKey? k l

theorem Std.Internal.List.getKey?_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Sigma.fst toInsert) : getKey? k' (insertList l toInsert) = some k

theorem Std.Internal.List.getKey_insertList_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : (List.map Sigma.fst toInsert).contains k = false) {h : containsKey k (insertList l toInsert) = true} : getKey k (insertList l toInsert) h = getKey k l ⋯

theorem Std.Internal.List.getKey_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Sigma.fst toInsert) {h : containsKey k' (insertList l toInsert) = true} : getKey k' (insertList l toInsert) h = k

theorem Std.Internal.List.getKey!_insertList_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] [Inhabited α] {l toInsert : List ((a : α) × β a)} {k : α} (contains_false : (List.map Sigma.fst toInsert).contains k = false) : getKey! k (insertList l toInsert) = getKey! k l

theorem Std.Internal.List.getKey!_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] [Inhabited α] {l toInsert : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Sigma.fst toInsert) : getKey! k' (insertList l toInsert) = k

theorem Std.Internal.List.getKeyD_insertList_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α} (not_contains : (List.map Sigma.fst toInsert).contains k = false) : getKeyD k (insertList l toInsert) fallback = getKeyD k l fallback

theorem Std.Internal.List.getKeyD_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Sigma.fst toInsert) : getKeyD k' (insertList l toInsert) fallback = k

theorem Std.Internal.List.perm_insertList {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (distinct_both : ∀ (a : α), containsKey a l = true → (List.map Sigma.fst toInsert).contains a = false) : (insertList l toInsert).Perm (l ++ toInsert)

theorem Std.Internal.List.length_insertList {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (distinct_both : ∀ (a : α), containsKey a l = true → (List.map Sigma.fst toInsert).contains a = false) : (insertList l toInsert).length = l.length + toInsert.length

theorem Std.Internal.List.length_le_length_insertList {α : Type u} {β : α → Type v} [BEq α] {l toInsert : List ((a : α) × β a)} : l.length ≤ (insertList l toInsert).length

theorem Std.Internal.List.length_insertList_le {α : Type u} {β : α → Type v} [BEq α] {l toInsert : List ((a : α) × β a)} : (insertList l toInsert).length ≤ l.length + toInsert.length

theorem Std.Internal.List.isEmpty_insertList {α : Type u} {β : α → Type v} [BEq α] {l toInsert : List ((a : α) × β a)} : (insertList l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)

def Std.Internal.List.Prod.toSigma {α : Type u} {β : Type v} (p : α × β) : (_ : α) × β

Internal implementation detail of the hash map

Equations

• Std.Internal.List.Prod.toSigma p = ⟨p.fst, p.snd⟩

@[simp]

theorem Std.Internal.List.Prod.fst_comp_toSigma {α : Type u} {β : Type v} : Sigma.fst ∘ toSigma = Prod.fst

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

Internal implementation detail of the hash map

Equations

• Std.Internal.List.insertListConst l toInsert = Std.Internal.List.insertList l (List.map Std.Internal.List.Prod.toSigma toInsert)

theorem Std.Internal.List.containsKey_insertListConst {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} : containsKey k (insertListConst l toInsert) = (containsKey k l || (List.map Prod.fst toInsert).contains k)

theorem Std.Internal.List.containsKey_of_containsKey_insertListConst {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (h₁ : containsKey k (insertListConst l toInsert) = true) (h₂ : (List.map Prod.fst toInsert).contains k = false) : containsKey k l = true

theorem Std.Internal.List.getKey?_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) : getKey? k (insertListConst l toInsert) = getKey? k l

theorem Std.Internal.List.getKey?_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Prod.fst toInsert) : getKey? k' (insertListConst l toInsert) = some k

theorem Std.Internal.List.getKey_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) {h : containsKey k (insertListConst l toInsert) = true} : getKey k (insertListConst l toInsert) h = getKey k l ⋯

theorem Std.Internal.List.getKey_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Prod.fst toInsert) {h : containsKey k' (insertListConst l toInsert) = true} : getKey k' (insertListConst l toInsert) h = k

theorem Std.Internal.List.getKey!_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) : getKey! k (insertListConst l toInsert) = getKey! k l

theorem Std.Internal.List.getKey!_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Prod.fst toInsert) : getKey! k' (insertListConst l toInsert) = k

theorem Std.Internal.List.getKeyD_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k fallback : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) : getKeyD k (insertListConst l toInsert) fallback = getKeyD k l fallback

theorem Std.Internal.List.getKeyD_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Prod.fst toInsert) : getKeyD k' (insertListConst l toInsert) fallback = k

theorem Std.Internal.List.length_insertListConst {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (distinct_both : ∀ (a : α), containsKey a l = true → (List.map Prod.fst toInsert).contains a = false) : (insertListConst l toInsert).length = l.length + toInsert.length

theorem Std.Internal.List.length_le_length_insertListConst {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} : l.length ≤ (insertListConst l toInsert).length

theorem Std.Internal.List.length_insertListConst_le {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} : (insertListConst l toInsert).length ≤ l.length + toInsert.length

theorem Std.Internal.List.isEmpty_insertListConst {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} : (insertListConst l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)

theorem Std.Internal.List.getValue?_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) : getValue? k (insertListConst l toInsert) = getValue? k l

theorem Std.Internal.List.getValue?_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) ∈ toInsert) : getValue? k' (insertListConst l toInsert) = some v

theorem Std.Internal.List.getValue_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} {not_contains : (List.map Prod.fst toInsert).contains k = false} {h : containsKey k (insertListConst l toInsert) = true} : getValue k (insertListConst l toInsert) h = getValue k l ⋯

theorem Std.Internal.List.getValue_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) ∈ toInsert) {h : containsKey k' (insertListConst l toInsert) = true} : getValue k' (insertListConst l toInsert) h = v

theorem Std.Internal.List.getValue!_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false) : getValue! k (insertListConst l toInsert) = getValue! k l

theorem Std.Internal.List.getValue!_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v : β} (k_beq : (k == k') = true) (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) ∈ toInsert) : getValue! k' (insertListConst l toInsert) = v

theorem Std.Internal.List.getValueD_insertListConst_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} {fallback : β} (not_contains : (List.map Prod.fst toInsert).contains k = false) : getValueD k (insertListConst l toInsert) fallback = getValueD k l fallback

theorem Std.Internal.List.getValueD_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback : β} (k_beq : (k == k') = true) (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) ∈ toInsert) : getValueD k' (insertListConst l toInsert) fallback = v

def Std.Internal.List.insertListIfNewUnit {α : Type u} [BEq α] (l : List ((_ : α) × Unit)) (toInsert : List α) : List ((_ : α) × Unit)

Internal implementation detail of the hash map

Equations

• Std.Internal.List.insertListIfNewUnit l [] = l
• Std.Internal.List.insertListIfNewUnit l (hd :: tl) = Std.Internal.List.insertListIfNewUnit (Std.Internal.List.insertEntryIfNew hd () l) tl

theorem Std.Internal.List.insertListIfNewUnit_perm_of_perm_first {α : Type u} [BEq α] [EquivBEq α] {l1 l2 : List ((_ : α) × Unit)} {toInsert : List α} (h : l1.Perm l2) (distinct : DistinctKeys l1) : (insertListIfNewUnit l1 toInsert).Perm (insertListIfNewUnit l2 toInsert)

theorem Std.Internal.List.DistinctKeys.insertListIfNewUnit {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} (distinct : DistinctKeys l) : DistinctKeys (List.insertListIfNewUnit l toInsert)

theorem Std.Internal.List.getEntry?_insertListIfNewUnit {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} : getEntry? k (insertListIfNewUnit l toInsert) = (getEntry? k l).or (getEntry? k (List.map (fun (x : α) => ⟨x, ()⟩) toInsert))

theorem Std.Internal.List.DistinctKeys.mapUnit {α : Type u} [BEq α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) : DistinctKeys (List.map (fun (x : α) => ⟨x, ()⟩) l)

theorem Std.Internal.List.getEntry?_insertListIfNewUnit_of_contains_eq_false {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (not_contains : toInsert.contains k = false) : getEntry? k (insertListIfNewUnit l toInsert) = getEntry? k l

theorem Std.Internal.List.containsKey_insertListIfNewUnit {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} : containsKey k (insertListIfNewUnit l toInsert) = (containsKey k l || toInsert.contains k)

theorem Std.Internal.List.containsKey_of_containsKey_insertListIfNewUnit {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (h₂ : toInsert.contains k = false) : containsKey k (insertListIfNewUnit l toInsert) = true → containsKey k l = true

theorem Std.Internal.List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (h' : containsKey k l = false) (h : toInsert.contains k = false) : getKey? k (insertListIfNewUnit l toInsert) = none

theorem Std.Internal.List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' : α} (k_beq : (k == k') = true) (mem' : containsKey k l = false) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) toInsert) (mem : k ∈ toInsert) : getKey? k' (insertListIfNewUnit l toInsert) = some k

theorem Std.Internal.List.getKey?_insertListIfNewUnit_of_contains {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (h : containsKey k l = true) : getKey? k (insertListIfNewUnit l toInsert) = getKey? k l

theorem Std.Internal.List.getKey_insertListIfNewUnit_of_contains_eq_false_of_mem {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' : α} (k_beq : (k == k') = true) {h : containsKey k' (insertListIfNewUnit l toInsert) = true} (contains_eq_false : containsKey k l = false) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) toInsert) (mem : k ∈ toInsert) : getKey k' (insertListIfNewUnit l toInsert) h = k

theorem Std.Internal.List.getKey_insertListIfNewUnit_of_contains {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (contains : containsKey k l = true) {h : containsKey k (insertListIfNewUnit l toInsert) = true} : getKey k (insertListIfNewUnit l toInsert) h = getKey k l contains

theorem Std.Internal.List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false {α : Type u} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (contains_eq_false : containsKey k l = false) (contains_eq_false' : toInsert.contains k = false) : getKey! k (insertListIfNewUnit l toInsert) = default

theorem Std.Internal.List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_mem {α : Type u} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' : α} (k_beq : (k == k') = true) (h : containsKey k l = false) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) toInsert) (mem : k ∈ toInsert) : getKey! k' (insertListIfNewUnit l toInsert) = k

theorem Std.Internal.List.getKey!_insertListIfNewUnit_of_contains {α : Type u} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (h : containsKey k l = true) : getKey! k (insertListIfNewUnit l toInsert) = getKey! k l

theorem Std.Internal.List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α} (contains_eq_false : containsKey k l = false) (contains_eq_false' : toInsert.contains k = false) : getKeyD k (insertListIfNewUnit l toInsert) fallback = fallback

theorem Std.Internal.List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_mem {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' fallback : α} (k_beq : (k == k') = true) (h : containsKey k l = false) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) toInsert) (mem : k ∈ toInsert) : getKeyD k' (insertListIfNewUnit l toInsert) fallback = k

theorem Std.Internal.List.getKeyD_insertListIfNewUnit_of_contains {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α} (contains : containsKey k l = true) : getKeyD k (insertListIfNewUnit l toInsert) fallback = getKeyD k l fallback

theorem Std.Internal.List.length_insertListIfNewUnit {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} (distinct_l : DistinctKeys l) (distinct_toInsert : List.Pairwise (fun (a b : α) => (a == b) = false) toInsert) (distinct_both : ∀ (a : α), containsKey a l = true → toInsert.contains a = false) : (insertListIfNewUnit l toInsert).length = l.length + toInsert.length

theorem Std.Internal.List.length_le_length_insertListIfNewUnit {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} : l.length ≤ (insertListIfNewUnit l toInsert).length

theorem Std.Internal.List.length_insertListIfNewUnit_le {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} : (insertListIfNewUnit l toInsert).length ≤ l.length + toInsert.length

theorem Std.Internal.List.isEmpty_insertListIfNewUnit {α : Type u} [BEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} : (insertListIfNewUnit l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)

theorem Std.Internal.List.getValue?_list_unit {α : Type u} [BEq α] {l : List ((_ : α) × Unit)} {k : α} : getValue? k l = if containsKey k l = true then some () else none

theorem Std.Internal.List.getValue?_insertListIfNewUnit {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} : getValue? k (insertListIfNewUnit l toInsert) = if containsKey k l = true ∨ toInsert.contains k = true then some () else none

def Std.Internal.List.alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (k : α) (f : Option (β k) → Option (β k)) (l : List ((a : α) × β a)) : List ((a : α) × β a)

Internal implementation detail of the hash map

Equations

• Std.Internal.List.alterKey k f l = match f (Std.Internal.List.getValueCast? k l) with | none => Std.Internal.List.eraseKey k l | some v => Std.Internal.List.insertEntry k v l

theorem Std.Internal.List.length_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} : (alterKey k f l).length = if h : containsKey k l = true then if (f (some (getValueCast k l h))).isSome = true then l.length else l.length - 1 else if (f none).isSome = true then l.length + 1 else l.length

theorem Std.Internal.List.length_alterKey' {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} : (alterKey k f l).length = if (containsKey k l && (f (getValueCast? k l)).isNone) = true then l.length - 1 else if (!containsKey k l && (f (getValueCast? k l)).isSome) = true then l.length + 1 else l.length

theorem Std.Internal.List.alterKey_cons_perm {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} {k' : α} {v' : β k'} {l : List ((a : α) × β a)} : (alterKey k f (⟨k', v'⟩ :: l)).Perm (if hk : (k' == k) = true then match f (some (cast ⋯ v')) with | none => l | some v => ⟨k, v⟩ :: l else ⟨k', v'⟩ :: alterKey k f l)

theorem Std.Internal.List.isEmpty_alterKey_eq_isEmpty_eraseKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} : (alterKey k f l).isEmpty = ((eraseKey k l).isEmpty && (f (getValueCast? k l)).isNone)

theorem Std.Internal.List.isEmpty_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} : (alterKey k f l).isEmpty = ((l.isEmpty || l.length == 1 && containsKey k l) && (f (getValueCast? k l)).isNone)

theorem Std.Internal.List.alterKey_of_perm {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hp : l.Perm l') : (alterKey a f l).Perm (alterKey a f l')

theorem Std.Internal.List.alterKey_append_of_containsKey_right_eq_false {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} {l l' : List ((a : α) × β a)} (hc : containsKey a l' = false) : alterKey a f (l ++ l') = alterKey a f l ++ l'

@[simp]

theorem Std.Internal.List.alterKey_nil {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} : alterKey a f [] = match f none with | none => [] | some b => [⟨a, b⟩]

theorem Std.Internal.List.containsKey_alterKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} {l : List ((a : α) × β a)} (hl : DistinctKeys l) : containsKey a (alterKey a f l) = (f (getValueCast? a l)).isSome

theorem Std.Internal.List.containsKey_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} (hl : DistinctKeys l) : containsKey k' (alterKey k f l) = if (k == k') = true then (f (getValueCast? k l)).isSome else containsKey k' l

theorem Std.Internal.List.DistinctKeys.alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} {l : List ((a : α) × β a)} (hl : DistinctKeys l) : DistinctKeys (List.alterKey a f l)

theorem Std.Internal.List.mem_alterKey_of_key_ne {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.fst ≠ a) : p ∈ alterKey a f l ↔ p ∈ l

theorem Std.Internal.List.getValueCast?_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (k k' : α) (f : Option (β k) → Option (β k)) (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCast? k' (alterKey k f l) = if h : (k == k') = true then cast ⋯ (f (getValueCast? k l)) else getValueCast? k' l

theorem Std.Internal.List.getValueCast_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (k k' : α) (f : Option (β k) → Option (β k)) (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l) = true) : getValueCast k' (alterKey k f l) hc = if h : (k == k') = true then cast ⋯ ((f (getValueCast? k l)).get ⋯) else getValueCast k' l ⋯

theorem Std.Internal.List.getValueCast_alterKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (k : α) (f : Option (β k) → Option (β k)) (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k (alterKey k f l) = true) : getValueCast k (alterKey k f l) hc = (f (getValueCast? k l)).get ⋯

theorem Std.Internal.List.getValueCast!_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} [Inhabited (β k')] {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCast! k' (alterKey k f l) = if heq : (k == k') = true then (Option.map (cast ⋯) (f (getValueCast? k l))).get! else getValueCast! k' l

theorem Std.Internal.List.getValueCastD_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCastD k' (alterKey k f l) fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (f (getValueCast? k l))).getD fallback else getValueCastD k' l fallback

theorem Std.Internal.List.getKey?_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getKey? k' (alterKey k f l) = if (k == k') = true then if (f (getValueCast? k l)).isSome = true then some k else none else getKey? k' l

theorem Std.Internal.List.getKey!_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getKey! k' (alterKey k f l) = if (k == k') = true then if (f (getValueCast? k l)).isSome = true then k else default else getKey! k' l

theorem Std.Internal.List.getKey_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l) = true) : getKey k' (alterKey k f l) hc = if heq : (k == k') = true then k else getKey k' l ⋯

theorem Std.Internal.List.getKeyD_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' fallback : α} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getKeyD k' (alterKey k f l) fallback = if (k == k') = true then if (f (getValueCast? k l)).isSome = true then k else fallback else getKeyD k' l fallback

def Std.Internal.List.Const.alterKey {α : Type u} {β : Type v} [BEq α] (k : α) (f : Option β → Option β) (l : List ((_ : α) × β)) : List ((_ : α) × β)

Internal implementation detail of the hash map

Equations

• Std.Internal.List.Const.alterKey k f l = match f (Std.Internal.List.getValue? k l) with | none => Std.Internal.List.eraseKey k l | some v => Std.Internal.List.insertEntry k v l

theorem Std.Internal.List.Const.length_alterKey {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} : (alterKey k f l).length = if h : containsKey k l = true then if (f (some (getValue k l h))).isSome = true then l.length else l.length - 1 else if (f none).isSome = true then l.length + 1 else l.length

theorem Std.Internal.List.Const.length_alterKey' {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} : (alterKey k f l).length = if (containsKey k l && (f (getValue? k l)).isNone) = true then l.length - 1 else if (!containsKey k l && (f (getValue? k l)).isSome) = true then l.length + 1 else l.length

theorem Std.Internal.List.Const.length_alterKey_eq_add_one {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (h : containsKey k l = false) (h' : (f (getValue? k l)).isSome = true) : (alterKey k f l).length = l.length + 1

theorem Std.Internal.List.Const.length_alterKey_eq_sub_one {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (h : containsKey k l = true) (h' : (f (getValue? k l)).isNone = true) : (alterKey k f l).length = l.length - 1

theorem Std.Internal.List.Const.length_alterKey_eq_self {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (h : containsKey k l = true) (h' : (f (getValue? k l)).isSome = true) : (alterKey k f l).length = l.length

theorem Std.Internal.List.Const.length_alterKey_eq_self' {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (h : containsKey k l = false) (h' : (f (getValue? k l)).isNone = true) : (alterKey k f l).length = l.length

theorem Std.Internal.List.Const.alterKey_cons_perm {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option β → Option β} {k' : α} {v' : β} {l : List ((_ : α) × β)} : (alterKey k f (⟨k', v'⟩ :: l)).Perm (if (k' == k) = true then match f (some v') with | none => l | some v => ⟨k, v⟩ :: l else ⟨k', v'⟩ :: alterKey k f l)

theorem Std.Internal.List.Const.isEmpty_alterKey_eq_isEmpty_eraseKey {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} : (alterKey k f l).isEmpty = ((eraseKey k l).isEmpty && (f (getValue? k l)).isNone)

theorem Std.Internal.List.Const.isEmpty_alterKey {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} : (alterKey k f l).isEmpty = ((l.isEmpty || l.length == 1 && containsKey k l) && (f (getValue? k l)).isNone)

theorem Std.Internal.List.Const.alterKey_of_perm {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {a : α} {f : Option β → Option β} {l l' : List ((_ : α) × β)} (hl : DistinctKeys l) (hp : l.Perm l') : (alterKey a f l).Perm (alterKey a f l')

theorem Std.Internal.List.Const.alterKey_append_of_containsKey_right_eq_false {α : Type u} [BEq α] {β : Type v} {a : α} {f : Option β → Option β} {l l' : List ((_ : α) × β)} (hc : containsKey a l' = false) : alterKey a f (l ++ l') = alterKey a f l ++ l'

@[simp]

theorem Std.Internal.List.Const.alterKey_nil {α : Type u} [BEq α] {β : Type v} {a : α} {f : Option β → Option β} : alterKey a f [] = match f none with | none => [] | some b => [⟨a, b⟩]

theorem Std.Internal.List.Const.containsKey_alterKey_self {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {a : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (hl : DistinctKeys l) : containsKey a (alterKey a f l) = (f (getValue? a l)).isSome

theorem Std.Internal.List.Const.mem_alterKey_of_key_not_beq {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {a : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (p : (_ : α) × β) (hne : (p.fst == a) = false) : p ∈ alterKey a f l ↔ p ∈ l

theorem Std.Internal.List.Const.containsKey_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (hl : DistinctKeys l) : containsKey k' (alterKey k f l) = if (k == k') = true then (f (getValue? k l)).isSome else containsKey k' l

theorem Std.Internal.List.Const.getValue?_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] (k k' : α) (f : Option β → Option β) (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValue? k' (alterKey k f l) = if (k == k') = true then f (getValue? k l) else getValue? k' l

theorem Std.Internal.List.Const.getValue_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] (k k' : α) (f : Option β → Option β) (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l) = true) : getValue k' (alterKey k f l) hc = if h : (k == k') = true then (f (getValue? k l)).get ⋯ else getValue k' l ⋯

theorem Std.Internal.List.Const.getValue_alterKey_self {α : Type u} [BEq α] {β : Type v} [EquivBEq α] (k : α) (f : Option β → Option β) (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k (alterKey k f l) = true) : getValue k (alterKey k f l) hc = (f (getValue? k l)).get ⋯

theorem Std.Internal.List.Const.getValue!_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} [Inhabited β] {f : Option β → Option β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValue! k' (alterKey k f l) = if (k == k') = true then (f (getValue? k l)).get! else getValue! k' l

theorem Std.Internal.List.Const.getValueD_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} {fallback : β} {f : Option β → Option β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValueD k' (alterKey k f l) fallback = if (k == k') = true then (f (getValue? k l)).getD fallback else getValueD k' l fallback

theorem Std.Internal.List.Const.getKey?_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} {f : Option β → Option β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getKey? k' (alterKey k f l) = if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l

theorem Std.Internal.List.Const.getKey!_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] [Inhabited α] {k k' : α} {f : Option β → Option β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getKey! k' (alterKey k f l) = if (k == k') = true then if (f (getValue? k l)).isSome = true then k else default else getKey! k' l

theorem Std.Internal.List.Const.getKey_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] [Inhabited α] {k k' : α} {f : Option β → Option β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l) = true) : getKey k' (alterKey k f l) hc = if heq : (k == k') = true then k else getKey k' l ⋯

theorem Std.Internal.List.Const.getKeyD_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' fallback : α} {f : Option β → Option β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getKeyD k' (alterKey k f l) fallback = if (k == k') = true then if (f (getValue? k l)).isSome = true then k else fallback else getKeyD k' l fallback

theorem Std.Internal.List.constAlterKey_eq_alterKey {α : Type u} [BEq α] [LawfulBEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} : Const.alterKey k f l = alterKey k f l

theorem Std.Internal.List.DistinctKeys.constAlterKey {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {a : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (hl : DistinctKeys l) : DistinctKeys (Const.alterKey a f l)

def Std.Internal.List.modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) (l : List ((a : α) × β a)) : List ((a : α) × β a)

Internal implementation detail of the hash map

Equations

• Std.Internal.List.modifyKey k f l = match Std.Internal.List.getValueCast? k l with | none => l | some v => Std.Internal.List.replaceEntry k (f v) l

theorem Std.Internal.List.isEmpty_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) (l : List ((a : α) × β a)) : (modifyKey k f l).isEmpty = l.isEmpty

theorem Std.Internal.List.length_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) (l : List ((a : α) × β a)) : (modifyKey k f l).length = l.length

theorem Std.Internal.List.containsKey_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (k k' : α) (f : β k → β k) (l : List ((a : α) × β a)) : containsKey k' (modifyKey k f l) = containsKey k' l

theorem Std.Internal.List.modifyKey_eq_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) (l : List ((a : α) × β a)) : modifyKey k f l = alterKey k (fun (x : Option (β k)) => Option.map f x) l

theorem Std.Internal.List.getValueCast?_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCast? k' (modifyKey k f l) = if h : (k == k') = true then cast ⋯ (Option.map f (getValueCast? k l)) else getValueCast? k' l

@[simp]

theorem Std.Internal.List.getValueCast?_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCast? k (modifyKey k f l) = Option.map f (getValueCast? k l)

theorem Std.Internal.List.getValueCast_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l) = true) : getValueCast k' (modifyKey k f l) h = if heq : (k == k') = true then cast ⋯ (f (getValueCast k l ⋯)) else getValueCast k' l ⋯

@[simp]

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

theorem Std.Internal.List.getValueCast!_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCast! k' (modifyKey k f l) = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (getValueCast? k l))).get! else getValueCast! k' l

@[simp]

theorem Std.Internal.List.getValueCast!_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} [Inhabited (β k)] {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCast! k (modifyKey k f l) = (Option.map f (getValueCast? k l)).get!

theorem Std.Internal.List.getValueCastD_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCastD k' (modifyKey k f l) fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (getValueCast? k l))).getD fallback else getValueCastD k' l fallback

@[simp]

theorem Std.Internal.List.getValueCastD_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCastD k (modifyKey k f l) fallback = (Option.map f (getValueCast? k l)).getD fallback

theorem Std.Internal.List.getKey?_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getKey? k' (modifyKey k f l) = if (k == k') = true then if containsKey k l = true then some k else none else getKey? k' l

theorem Std.Internal.List.getKey?_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getKey? k (modifyKey k f l) = if containsKey k l = true then some k else none

theorem Std.Internal.List.getKey!_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getKey! k' (modifyKey k f l) = if (k == k') = true then if containsKey k l = true then k else default else getKey! k' l

theorem Std.Internal.List.getKey!_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getKey! k (modifyKey k f l) = if containsKey k l = true then k else default

theorem Std.Internal.List.getKey_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l) = true) : getKey k' (modifyKey k f l) h = if (k == k') = true then k else getKey k' l ⋯

@[simp]

theorem Std.Internal.List.getKey_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l) = true) : getKey k (modifyKey k f l) h = k

theorem Std.Internal.List.getKeyD_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' fallback : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getKeyD k' (modifyKey k f l) fallback = if (k == k') = true then if containsKey k l = true then k else fallback else getKeyD k' l fallback

theorem Std.Internal.List.getKeyD_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Inhabited α] {k fallback : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getKeyD k (modifyKey k f l) fallback = if containsKey k l = true then k else fallback

def Std.Internal.List.Const.modifyKey {α : Type u} {β : Type v} [BEq α] (k : α) (f : β → β) (l : List ((_ : α) × β)) : List ((_ : α) × β)

Internal implementation detail of the hash map

Equations

• Std.Internal.List.Const.modifyKey k f l = match Std.Internal.List.getValue? k l with | none => l | some v => Std.Internal.List.replaceEntry k (f v) l

theorem Std.Internal.List.Const.isEmpty_modifyKey {α : Type u} {β : Type v} [BEq α] (k : α) (f : β → β) (l : List ((_ : α) × β)) : (modifyKey k f l).isEmpty = l.isEmpty

theorem Std.Internal.List.Const.modifyKey_eq_alterKey {α : Type u} {β : Type v} [BEq α] (k : α) (f : β → β) (l : List ((_ : α) × β)) : modifyKey k f l = alterKey k (fun (x : Option β) => Option.map f x) l

theorem Std.Internal.List.Const.length_modifyKey {α : Type u} {β : Type v} [BEq α] (k : α) (f : β → β) (l : List ((_ : α) × β)) : (modifyKey k f l).length = l.length

theorem Std.Internal.List.Const.containsKey_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] (k k' : α) (f : β → β) (l : List ((_ : α) × β)) : containsKey k' (modifyKey k f l) = containsKey k' l

theorem Std.Internal.List.Const.getValue?_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValue? k' (modifyKey k f l) = if (k == k') = true then Option.map f (getValue? k l) else getValue? k' l

@[simp]

theorem Std.Internal.List.Const.getValue?_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValue? k (modifyKey k f l) = Option.map f (getValue? k l)

theorem Std.Internal.List.Const.getValue_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l) = true) : getValue k' (modifyKey k f l) h = if heq : (k == k') = true then f (getValue k l ⋯) else getValue k' l ⋯

@[simp]

theorem Std.Internal.List.Const.getValue_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) {h : containsKey k (modifyKey k f l) = true} : getValue k (modifyKey k f l) h = f (getValue k l ⋯)

theorem Std.Internal.List.Const.getValue!_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} [hi : Inhabited β] {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValue! k' (modifyKey k f l) = if (k == k') = true then (Option.map f (getValue? k l)).get! else getValue! k' l

@[simp]

theorem Std.Internal.List.Const.getValue!_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} [Inhabited β] {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValue! k (modifyKey k f l) = (Option.map f (getValue? k l)).get!

theorem Std.Internal.List.Const.getValueD_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {fallback : β} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValueD k' (modifyKey k f l) fallback = if (k == k') = true then (Option.map f (getValue? k l)).getD fallback else getValueD k' l fallback

@[simp]

theorem Std.Internal.List.Const.getValueD_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {fallback : β} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValueD k (modifyKey k f l) fallback = (Option.map f (getValue? k l)).getD fallback

theorem Std.Internal.List.Const.getKey?_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getKey? k' (modifyKey k f l) = if (k == k') = true then if containsKey k l = true then some k else none else getKey? k' l

theorem Std.Internal.List.Const.getKey?_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getKey? k (modifyKey k f l) = if containsKey k l = true then some k else none

theorem Std.Internal.List.Const.getKey!_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getKey! k' (modifyKey k f l) = if (k == k') = true then if containsKey k l = true then k else default else getKey! k' l

theorem Std.Internal.List.Const.getKey!_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {k : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getKey! k (modifyKey k f l) = if containsKey k l = true then k else default

theorem Std.Internal.List.Const.getKey_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l) = true) : getKey k' (modifyKey k f l) h = if (k == k') = true then k else getKey k' l ⋯

@[simp]

theorem Std.Internal.List.Const.getKey_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {k : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l) = true) : getKey k (modifyKey k f l) h = k

theorem Std.Internal.List.Const.getKeyD_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' fallback : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getKeyD k' (modifyKey k f l) fallback = if (k == k') = true then if containsKey k l = true then k else fallback else getKeyD k' l fallback

theorem Std.Internal.List.Const.getKeyD_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {k fallback : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getKeyD k (modifyKey k f l) fallback = if containsKey k l = true then k else fallback

theorem Std.Internal.List.constModifyKey_eq_modifyKey {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] {k : α} {f : β → β} {l : List ((_ : α) × β)} : Const.modifyKey k f l = modifyKey k f l