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
@[simp]
@[simp]
theorem Std.Internal.List.containsKey_cons {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
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) :
theorem Std.Internal.List.containsKey_eq_isSome_getEntry? {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {a : α} :
theorem Std.Internal.List.containsKey_eq_contains_map_fst {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} :
theorem Std.Internal.List.containsKey_eq_keys_contains {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :
@[simp]
theorem Std.Internal.List.DistinctKeys.def {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} :
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') :
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'
@[simp]
theorem Std.Internal.List.distinctKeys_cons_iff {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.DistinctKeys.tail {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
DistinctKeys (⟨k, v⟩ :: l) → DistinctKeys l
theorem Std.Internal.List.DistinctKeys.containsKey_eq_false {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
DistinctKeys (⟨k, v⟩ :: l) → containsKey k l = false
theorem Std.Internal.List.DistinctKeys.cons {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = false) :
DistinctKeys l → DistinctKeys (⟨k, v⟩ :: l)
theorem Std.Internal.List.containsKey_eq_isSome_getValue? {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} :
theorem Std.Internal.List.containsKey_of_getValueCast?_eq_some {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {b : β a} (h : getValueCast? a l = some b) :
theorem Std.Internal.List.getValueCast?_eq_none {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = false) :
theorem Std.Internal.List.containsKey_congr {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α} (h : (a == b) = true) :
theorem Std.Internal.List.containsKey_of_beq {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α} (hla : containsKey a l = true) (hab : (a == b) = true) :
def Std.Internal.List.getEntry {α : Type u} {β : α → Type v} [BEq α] (a : α) (l : List ((a : α) × β a)) (h : containsKey a l = true) :
(a : α) × β a
Internal implementation detail of the hash map
Instances For
theorem Std.Internal.List.getEntry_congr {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α} (h : (a == b) = true) {h₁ : containsKey a l = true} {h₂ : containsKey b l = true} :
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
Instances For
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
Instances For
theorem Std.Internal.List.getValueCast?_eq_some_getValueCast {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
theorem Std.Internal.List.getValueCast_mem {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = true) :
theorem Std.Internal.List.getValueCast_of_mem {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {x : (a : α) × β a} (h : x ∈ l) (distinct : DistinctKeys l) :
theorem Std.Internal.List.getValue_eq_getValueCast {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] {l : List ((_ : α) × β)} {a : α} {h : containsKey a l = true} :
@[simp]
theorem Std.Internal.List.getValueCastD_nil {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {fallback : β a} :
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) :
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) :
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) :
theorem Std.Internal.List.getValueCast!_eq_default {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (h : containsKey a l = false) :
theorem Std.Internal.List.getValueCast_eq_getValueCast! {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (h : containsKey a l = true) :
theorem Std.Internal.List.getValueCast?_eq_some_getValueCast! {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (h : containsKey a l = true) :
theorem Std.Internal.List.containsKey_eq_isSome_getKey? {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {a : α} :
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
Instances For
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) :
@[simp]
theorem Std.Internal.List.isEmpty_replaceEntry {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.getEntry?_replaceEntry_of_containsKey_eq_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} (hl : containsKey k l = false) :
theorem Std.Internal.List.getEntry?_replaceEntry_of_false {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} (h : (k == a) = false) :
theorem Std.Internal.List.getEntry?_replaceEntry_of_true {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} (hl : containsKey k l = true) (h : (k == a) = true) :
@[simp]
theorem Std.Internal.List.containsKey_replaceEntry {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} :
theorem Std.Internal.List.getEntry_replaceEntry_of_true {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} (hl : containsKey a (replaceEntry k v l) = true) (h : (k == a) = true) :
theorem Std.Internal.List.mem_replaceEntry_of_true {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (hl : containsKey k l = true) :
@[simp]
theorem Std.Internal.List.length_replaceEntry {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.getValue?_replaceEntry_of_containsKey_eq_false {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (hl : containsKey k l = false) :
theorem Std.Internal.List.getValue?_replaceEntry_of_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = false) :
theorem Std.Internal.List.getValue?_replaceEntry_of_true {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (hl : containsKey k l = true) (h : (k == a) = true) :
theorem Std.Internal.List.getValueCast?_replaceEntry {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} :
getValueCast? a (replaceEntry k v l) = if h : containsKey k l = true ∧ (k == a) = true then some (cast ⋯ v) else getValueCast? a l
theorem Std.Internal.List.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.insertEntry_of_containsKey {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = true) :
theorem Std.Internal.List.insertEntry_of_containsKey_eq_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = false) :
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} :
theorem Std.Internal.List.length_le_length_insertEntry {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
theorem Std.Internal.List.getValue?_insertEntry_of_beq {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = true) :
theorem Std.Internal.List.getValue?_insertEntry_of_false {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = false) :
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.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.getKey?_eq_none {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l = false) :
theorem Std.Internal.List.containsKey_insertEntry {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
theorem Std.Internal.List.containsKey_insertEntry_of_beq {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true) :
theorem Std.Internal.List.containsKey_of_containsKey_insertEntry {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntry k v l) = true) (h₂ : (k == a) = false) :
theorem Std.Internal.List.getValueCast_insertEntry {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (insertEntry k v l) = true} :
getValueCast a (insertEntry k v l) h = if h' : (k == a) = true then cast ⋯ v else getValueCast a l ⋯
theorem Std.Internal.List.getEntry_insertEntry {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (insertEntry k v l) = true} :
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} :
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} :
theorem Std.Internal.List.insertEntryIfNew_of_containsKey {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = true) :
theorem Std.Internal.List.insertEntryIfNew_of_containsKey_eq_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l = false) :
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} :
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.containsKey_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
theorem Std.Internal.List.containsKey_of_containsKey_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntryIfNew k v l) = true) (h₂ : (k == a) = false) :
theorem Std.Internal.List.containsKey_of_containsKey_insertEntryIfNew' {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntryIfNew k v l) = true) (h₂ : ¬((k == a) = true ∧ containsKey k l = false)) :
This is a restatement of containsKey_insertEntryIfNew that is written to exactly match the proof
obligation in the statement of getValueCast_insertEntryIfNew.
theorem Std.Internal.List.getValueCast_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (insertEntryIfNew k v l) = true} :
getValueCast a (insertEntryIfNew k v l) h = if h' : (k == a) = true ∧ containsKey k l = false then cast ⋯ v else getValueCast a l ⋯
theorem Std.Internal.List.getValue_insertEntryIfNew {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} {h : containsKey a (insertEntryIfNew k v l) = true} :
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.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.getKey_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h : containsKey a (insertEntryIfNew k v l) = true} :
theorem Std.Internal.List.length_le_length_insertEntryIfNew {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β 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) :
theorem Std.Internal.List.getEntry?_eraseKey_of_beq {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) (hka : (k == a) = true) :
theorem Std.Internal.List.keys_filterMap' {α : Type u} {β : α → Type v} {γ : α → Type w} {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)
theorem Std.Internal.List.keys_filter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {f : (a : α) → β a → Bool} (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.keys_filter {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {l : List ((_ : α) × β)} {f : α → β → Bool} (hl : DistinctKeys 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) :
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) :
theorem Std.Internal.List.getValue?_eraseKey_of_beq {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) (hka : (k == a) = true) :
theorem Std.Internal.List.getKey?_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey!_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKeyD_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k fallback : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.containsKey_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} (h : DistinctKeys l) :
theorem Std.Internal.List.containsKey_eraseKey_of_beq {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) (hka : (a == k) = true) :
theorem Std.Internal.List.containsKey_eraseKey_of_false {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hka : (k == a) = false) :
theorem Std.Internal.List.containsKey_eraseKey {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.isEmpty_eq_isEmpty_eraseKey_and_not_containsKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (k : α) :
theorem Std.Internal.List.getValueCast?_eraseKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCast?_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCast!_eraseKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} [Inhabited (β a)] (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCast!_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCastD_eraseKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {fallback : β a} (hl : DistinctKeys l) :
getValueCastD a (eraseKey k l) fallback = if (k == a) = true then fallback else getValueCastD a l fallback
theorem Std.Internal.List.getValueCastD_eraseKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValue!_eraseKey_self {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueD_eraseKey_self {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} {fallback : β} (hl : DistinctKeys l) :
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) :
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) :
theorem Std.Internal.List.getEntry?_of_perm {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getEntryD_of_perm {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} {fallback : (a : α) × β a} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getEntry!_of_perm {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} [Inhabited ((a : α) × β a)] (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.containsKey_of_perm {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {k : α} (h : l.Perm l') :
theorem Std.Internal.List.getValueCast?_of_perm {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getValueCast_of_perm {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} {h' : containsKey a l = true} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getEntry_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') :
theorem Std.Internal.List.getValueCast!_of_perm {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getValueCastD_of_perm {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} {fallback : β a} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getValue?_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getValue_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α} {h' : containsKey a l = true} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getValue!_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l l' : List ((_ : α) × β)} {a : α} (hl : DistinctKeys l) (h : l.Perm l') :
theorem Std.Internal.List.getValueD_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α} {fallback : β} (hl : DistinctKeys l) (h : l.Perm l') :
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') :
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') :
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') :
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') :
theorem Std.Internal.List.getEntry?_ext {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hl' : DistinctKeys l') (h : ∀ (a : α), getEntry? a l = getEntry? a l') :
l.Perm l'
theorem Std.Internal.List.getValueCast?_ext {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hl' : DistinctKeys l') (h : ∀ (a : α), getValueCast? a l = getValueCast? a l') :
l.Perm l'
theorem Std.Internal.List.getKey_getValue?_ext {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {l l' : List ((_ : α) × β)} (hl : DistinctKeys l) (hl' : DistinctKeys l') (hk : ∀ (a : α) (h : containsKey a l = true) (h' : containsKey a l' = true), getKey a l h = getKey a l' h') (hv : ∀ (a : α), getValue? a l = getValue? a l') :
l.Perm l'
theorem Std.Internal.List.getKey?_ext {α : Type u} [BEq α] [EquivBEq α] {l l' : List ((_ : α) × Unit)} (hl : DistinctKeys l) (hl' : DistinctKeys l') (h : ∀ (a : α), getKey? a l = getKey? a l') :
l.Perm l'
theorem Std.Internal.List.containsKey_ext {α : Type u} [BEq α] [LawfulBEq α] {l l' : List ((_ : α) × Unit)} (hl : DistinctKeys l) (hl' : DistinctKeys l') (h : ∀ (a : α), containsKey a l = containsKey a l') :
l.Perm l'
theorem Std.Internal.List.replaceEntry_of_perm {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k} (hl : DistinctKeys l) (h : l.Perm l') :
(replaceEntry k v l).Perm (replaceEntry k v l')
theorem Std.Internal.List.insertEntry_of_perm {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k} (hl : DistinctKeys l) (h : l.Perm l') :
(insertEntry k v l).Perm (insertEntry k v l')
theorem Std.Internal.List.insertEntryIfNew_of_perm {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k} (hl : DistinctKeys l) (h : l.Perm l') :
(insertEntryIfNew k v l).Perm (insertEntryIfNew k v l')
@[simp]
theorem Std.Internal.List.containsKey_append {α : Type u} {β : α → Type v} [BEq α] {l l' : List ((a : α) × β a)} {a : α} :
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) :
theorem Std.Internal.List.getValueCast?_append_of_containsKey_eq_false {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl' : containsKey a l' = false) :
theorem Std.Internal.List.getValueCast_append_of_containsKey_eq_false {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a (l ++ l') = true} (hl' : containsKey a l' = false) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
theorem Std.Internal.List.find?_eq_none_iff_containsKey_eq_false {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} :
theorem Std.Internal.List.pairwise_fst_eq_false {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} (h : DistinctKeys l) :
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) :
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) :
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 : δ} :
theorem Std.Internal.List.foldl_eq_foldl_toProd {α : Type u} {β : Type v} {δ : Type w} {l : List ((_ : α) × β)} {f : δ → α → β → δ} {init : δ} :
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 : δ} :
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 : δ} :
theorem Std.Internal.List.foldr_eq_foldr_toProd {α : Type u} {β : Type v} {δ : Type w} {l : List ((_ : α) × β)} {f : α → β → δ → δ} {init : δ} :
theorem Std.Internal.List.foldr_eq_foldr_toProd' {α : Type u} {β : Type v} {δ : Type w} {l : List ((_ : α) × β)} {f : δ → α → β → δ} {init : δ} :
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} :
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 : δ} :
theorem Std.Internal.List.foldlM_eq_foldlM_keys {α : Type u} {β : α → Type v} {δ : Type w} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] {l : List ((a : α) × β a)} {f : δ → α → m' δ} {init : δ} :
theorem Std.Internal.List.foldl_eq_foldl_keys {α : Type u} {β : α → Type v} {δ : Type w} {l : List ((a : α) × β a)} {f : δ → α → δ} {init : δ} :
theorem Std.Internal.List.foldrM_eq_foldrM_keys {α : Type u} {β : α → Type v} {δ : Type w} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] {l : List ((a : α) × β a)} {f : α → δ → m' δ} {init : δ} :
theorem Std.Internal.List.foldrM_eq_foldrM_keys' {α : Type u} {β : α → Type v} {δ : Type w} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] {l : List ((a : α) × β a)} {f : δ → α → m' δ} {init : δ} :
List.foldrM (fun (a : (a : α) × β a) (b : δ) => f b a.fst) init l = List.foldrM (fun (a : α) (b : δ) => f b a) init (keys l)
theorem Std.Internal.List.foldr_eq_foldr_keys {α : Type u} {β : α → Type v} {δ : Type w} {l : List ((a : α) × β a)} {f : α → δ → δ} {init : δ} :
theorem Std.Internal.List.foldr_eq_foldr_keys' {α : Type u} {β : α → Type v} {δ : Type w} {l : List ((a : α) × β a)} {f : δ → α → δ} {init : δ} :
List.foldr (fun (a : (a : α) × β a) (b : δ) => f b a.fst) init l = List.foldr (fun (a : α) (b : δ) => f b a) init (keys l)
theorem Std.Internal.List.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 : α) :
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) :
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) :
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_insertList_disj_of_containsKey {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} :
theorem Std.Internal.List.containsKey_of_containsKey_insertList {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (h₁ : containsKey k (insertList l toInsert) = true) (h₂ : (List.map Sigma.fst toInsert).contains k = false) :
theorem Std.Internal.List.getValueCast?_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert) :
theorem Std.Internal.List.getValueCast_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (v : β k) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert) {h : containsKey k' (insertList l toInsert) = true} :
theorem Std.Internal.List.getValueCast!_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (v : β k) [Inhabited (β k')] (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert) :
theorem Std.Internal.List.getValueCastD_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert) :
theorem Std.Internal.List.getKey?_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Sigma.fst toInsert) :
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} :
theorem Std.Internal.List.getKey_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Sigma.fst toInsert) {h : containsKey k' (insertList l toInsert) = true} :
theorem Std.Internal.List.getKey!_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] [Inhabited α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Sigma.fst toInsert) :
theorem Std.Internal.List.getKeyD_insertList_of_mem {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) {k k' fallback : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Sigma.fst toInsert) :
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) :
theorem Std.Internal.List.length_le_length_insertList {α : Type u} {β : α → Type v} [BEq α] {l toInsert : List ((a : α) × β a)} :
theorem Std.Internal.List.DistinctKeys.insertListIfNew {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (h : DistinctKeys l₁) :
DistinctKeys (List.insertListIfNew l₁ l₂)
theorem Std.Internal.List.insertListIfNew_perm_of_perm_first {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l1 l2 toInsert : List ((a : α) × β a)} (h : l1.Perm l2) (distinct : DistinctKeys l1) :
(insertListIfNew l1 toInsert).Perm (insertListIfNew l2 toInsert)
theorem Std.Internal.List.containsKey_insertListIfNew {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} :
containsKey k (insertListIfNew l toInsert) = (containsKey k l || (List.map Sigma.fst toInsert).contains k)
theorem Std.Internal.List.contains_insertList_iff {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} :
containsKey k (insertList l toInsert) = true ↔ containsKey k l = true ∨ containsKey k toInsert = true
theorem Std.Internal.List.contains_of_contains_insertList_of_contains_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (h₁ : containsKey k (insertList l toInsert) = true) (h₂ : containsKey k toInsert = false) :
theorem Std.Internal.List.contains_of_contains_insertList_of_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (h₁ : containsKey k (insertList l toInsert) = true) (h₂ : containsKey k l = false) :
theorem Std.Internal.List.contains_insertList_of_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (contains : containsKey k l = true) :
theorem Std.Internal.List.contains_insertList_of_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (contains : containsKey k toInsert = true) :
theorem Std.Internal.List.DistinctKeys_impl_Pairwise_distinct {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} (distinct_l : DistinctKeys l) :
theorem Std.Internal.List.insertList_perm_of_perm_second {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l1 l2 l : List ((a : α) × β a)} (h : l1.Perm l2) (distinct_l : DistinctKeys l) (distinct : DistinctKeys l1) :
(insertList l l1).Perm (insertList l l2)
theorem Std.Internal.List.insertList_congr {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l1 l2 l3 l4 : List ((a : α) × β a)} (h₁ : l1.Perm l3) (h₂ : l2.Perm l4) (hd₁ : DistinctKeys l1) (hd₂ : DistinctKeys l2) (hd₃ : DistinctKeys l3) :
(insertList l1 l2).Perm (insertList l3 l4)
theorem Std.Internal.List.getEntry?_insertList_of_contains_left_eq_false {α : 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) (not_contains : containsKey k l = false) :
theorem Std.Internal.List.getKey?_insertList {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
theorem Std.Internal.List.getKey_insertList_of_contains_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) {m : containsKey k (insertList l toInsert) = true} (contains : containsKey k toInsert = true) :
theorem Std.Internal.List.getKeyD_insertList_of_contains_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
containsKey k toInsert = true → getKeyD k (insertList l toInsert) fallback = getKeyD k toInsert fallback
theorem Std.Internal.List.getKey!_insertList_of_contains_right_eq_false {α : Type u} {β : α → Type v} [Inhabited α] [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : containsKey k toInsert = false) :
theorem Std.Internal.List.getKey?_insertList_of_contains_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (not_contains : containsKey k toInsert = false) :
theorem Std.Internal.List.getKey?_insertList_of_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) (not_contains : containsKey k l = false) :
theorem Std.Internal.List.getKey_insertList_of_contains_left_of_contains_right_eq_false {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} {m : containsKey k (insertList l toInsert) = true} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) (mem : containsKey k l = true) :
theorem Std.Internal.List.getKeyD_insertList {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
theorem Std.Internal.List.getKeyD_insertList_of_contains_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α} (not_contains : containsKey k toInsert = false) :
theorem Std.Internal.List.getKeyD_insertList_of_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) (not_contains : containsKey k l = false) :
theorem Std.Internal.List.getKey!_insertList_of_contains_left_eq_false {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] [Inhabited α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
containsKey k l = false → getKey! k (insertList l toInsert) = getKey! k toInsert
theorem Std.Internal.List.getValueCast?_insertList_of_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
containsKey k l = false → getValueCast? k (insertList l toInsert) = getValueCast? k toInsert
theorem Std.Internal.List.getValueCast?_of_insertList {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
theorem Std.Internal.List.getValueCastD_of_insertList {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} {fallback : β k} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
getValueCastD k (insertList l toInsert) fallback = getValueCastD k toInsert (getValueCastD k l fallback)
theorem Std.Internal.List.getValueCast_insertList_of_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) (contains : containsKey k (insertList l toInsert) = true) (not_contains : containsKey k l = false) :
theorem Std.Internal.List.getKey_insertList_of_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) (contains : containsKey k (insertList l toInsert) = true) (not_contains : containsKey k l = false) :
theorem Std.Internal.List.getValueCast_insertList_of_contains_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) (contains : containsKey k toInsert = true) {h : containsKey k (insertList l toInsert) = true} :
theorem Std.Internal.List.getValueCastD_insertList_of_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} {fallback : β k} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) (not_contains : containsKey k l = false) :
theorem Std.Internal.List.length_insertList_distinct {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
(∀ (a : α), containsKey a l = true → containsKey a toInsert = false) →
(insertList l toInsert).length = l.length + toInsert.length
theorem Std.Internal.List.getKey?_insertList_of_mem_of_not_mem {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (contains : containsKey k l = true) (not_contains : containsKey k toInsert = false) :
theorem Std.Internal.List.insertListIfNew_perm_insertList {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (hd₁ : DistinctKeys l₁) (hd₂ : DistinctKeys l₂) :
(insertListIfNew l₁ l₂).Perm (insertList l₂ l₁)
theorem Std.Internal.List.insertList_perm_insertSmallerList {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
(insertList l toInsert).Perm (insertSmallerList l toInsert)
theorem Std.Internal.List.length_right_le_length_insertList {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
theorem Std.Internal.List.insertList_insertEntry_right_equiv_insertEntry_insertList {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (p : (a : α) × β a) (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
(insertList l (insertEntry p.fst p.snd toInsert)).Perm (insertEntry p.fst p.snd (insertList l toInsert))
theorem Std.Internal.List.length_le_length_of_containsKey {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (dl₁ : DistinctKeys l₁) (dl₂ : DistinctKeys l₂) (h : ∀ (a : α), containsKey a l₁ = true → containsKey a l₂ = true) :
theorem Std.Internal.List.containsKey_of_length_eq {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (dl₁ : DistinctKeys l₁) (dl₂ : DistinctKeys l₂) (hl : l₂.length = l₁.length) (hs : ∀ (a : α), containsKey a l₁ = true → containsKey a l₂ = true) (a : α) :
containsKey a l₂ = true → containsKey a l₁ = true
Internal implementation detail of the hash map
Instances For
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) :
theorem Std.Internal.List.getKey?_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Prod.fst toInsert) :
theorem Std.Internal.List.getKey_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Prod.fst toInsert) {h : containsKey k' (insertListConst l toInsert) = true} :
theorem Std.Internal.List.getKey!_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Prod.fst toInsert) :
theorem Std.Internal.List.getKeyD_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' fallback : α} (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : k ∈ List.map Prod.fst toInsert) :
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) :
theorem Std.Internal.List.getValue?_insertList_of_contains_eq_false_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (not_contains : containsKey k toInsert = false) :
theorem Std.Internal.List.getValueD_insertList_of_contains_eq_false_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β} (not_contains : containsKey k toInsert = false) :
theorem Std.Internal.List.getValue_insertList_of_contains_eq_false_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (not_contains : containsKey k toInsert = false) {p1 : containsKey k (insertList l toInsert) = true} {p2 : containsKey k l = true} :
theorem Std.Internal.List.getValue?_insertList_of_contains_eq_false_left {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
containsKey k l = false → getValue? k (insertList l toInsert) = getValue? k toInsert
theorem Std.Internal.List.getValueD_insertList_of_contains_eq_false_left {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
containsKey k l = false → getValueD k (insertList l toInsert) fallback = getValueD k toInsert fallback
theorem Std.Internal.List.getValue?_insertList {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
theorem Std.Internal.List.getValueD_insertList {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) :
theorem Std.Internal.List.getValue_insertList_of_contains_eq_false_left {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) (contains : containsKey k (insertList l toInsert) = true) (not_contains : containsKey k l = false) :
theorem Std.Internal.List.getValue_insertList_of_contains_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) (contains : containsKey k toInsert = true) {h : containsKey k (insertList l toInsert) = true} :
theorem Std.Internal.List.getValue?_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) ∈ toInsert) :
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} :
theorem Std.Internal.List.getValue_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) ∈ toInsert) {h : containsKey k' (insertListConst l toInsert) = true} :
theorem Std.Internal.List.getValue!_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v : β} (distinct_l : DistinctKeys l) (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) ∈ toInsert) :
theorem Std.Internal.List.getValueD_insertListConst_of_mem {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback : β} (distinct_l : DistinctKeys l) (k_beq : (k == k') = true) (distinct_toInsert : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) toInsert) (mem : (k, v) ∈ toInsert) :
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.DistinctKeys.mapUnit {α : Type u} [BEq α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :
theorem Std.Internal.List.getEntry?_insertListIfNewUnit_of_contains_eq_false {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (not_contains : toInsert.contains k = false) :
theorem Std.Internal.List.containsKey_insertListIfNewUnit {α : Type u} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} :
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_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) :
theorem Std.Internal.List.getKey?_insertListIfNewUnit_of_contains {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (h : containsKey k l = true) :
theorem Std.Internal.List.getKey_insertListIfNewUnit_of_contains_eq_false_of_mem {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' : α} (k_beq : (k == k') = true) {h : containsKey k' (insertListIfNewUnit l toInsert) = true} (contains_eq_false : containsKey k l = false) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) toInsert) (mem : k ∈ toInsert) :
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} :
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) :
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) :
theorem Std.Internal.List.getKeyD_insertListIfNewUnit_of_contains {α : Type u} [BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α} (contains : containsKey k l = true) :
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) :
theorem Std.Internal.List.containsKey_alterKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.containsKey_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
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.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) :
theorem Std.Internal.List.getValueCast!_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} [Inhabited (β k')] {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCast! k' (alterKey k f l) = if heq : (k == k') = true then (Option.map (cast ⋯) (f (getValueCast? k l))).get! else getValueCast! k' l
theorem Std.Internal.List.getValueCastD_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCastD k' (alterKey k f l) fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (f (getValueCast? k l))).getD fallback
else getValueCastD k' l fallback
theorem Std.Internal.List.getKey?_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey!_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey_alterKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l) = true) :
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) :
theorem Std.Internal.List.Const.containsKey_alterKey_self {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {a : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (hl : DistinctKeys 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) :
theorem Std.Internal.List.Const.getValueD_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} {fallback : β} {f : Option β → Option β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getKey?_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} {f : Option β → Option β} (l : List ((_ : α) × β)) (hl : DistinctKeys 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) :
theorem Std.Internal.List.Const.getKey_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} {f : Option β → Option β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l) = true) :
theorem Std.Internal.List.Const.getKeyD_alterKey {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' fallback : α} {f : Option β → Option β} (l : List ((_ : α) × β)) (hl : DistinctKeys 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)
theorem Std.Internal.List.DistinctKeys.modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {f : β a → β a} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
DistinctKeys (List.modifyKey a f l)
theorem Std.Internal.List.getValueCast?_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCast? k' (modifyKey k f l) = if h : (k == k') = true then cast ⋯ (Option.map f (getValueCast? k l)) else getValueCast? k' l
@[simp]
theorem Std.Internal.List.getValueCast?_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCast_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l) = true) :
getValueCast k' (modifyKey k f l) h = if heq : (k == k') = true then cast ⋯ (f (getValueCast k l ⋯)) else getValueCast k' l ⋯
@[simp]
theorem Std.Internal.List.getValueCast_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) {h : containsKey k (modifyKey k f l) = true} :
theorem Std.Internal.List.getValueCast!_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCast! k' (modifyKey k f l) = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (getValueCast? k l))).get! else getValueCast! k' l
@[simp]
theorem Std.Internal.List.getValueCast!_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} [Inhabited (β k)] {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCastD_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
getValueCastD k' (modifyKey k f l) fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (getValueCast? k l))).getD fallback
else getValueCastD k' l fallback
@[simp]
theorem Std.Internal.List.getValueCastD_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
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) :
@[simp]
theorem Std.Internal.List.getKey_modifyKey_self {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {f : β k → β k} (l : List ((a : α) × β a)) :
DistinctKeys l → ∀ (h : containsKey k (modifyKey k f l) = true), getKey k (modifyKey k f l) h = k
theorem Std.Internal.List.getKeyD_modifyKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' fallback : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
@[simp]
theorem Std.Internal.List.Const.getValue?_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getValue_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l) = true) :
theorem Std.Internal.List.Const.getValue!_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} [hi : Inhabited β] {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
@[simp]
theorem Std.Internal.List.Const.getValue!_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} [Inhabited β] {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getValueD_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {fallback : β} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
@[simp]
theorem Std.Internal.List.Const.getValueD_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {fallback : β} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getKey!_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
@[simp]
theorem Std.Internal.List.Const.getKey_modifyKey_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l) = true) :
theorem Std.Internal.List.Const.getKeyD_modifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' fallback : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
theorem Std.Internal.List.DistinctKeys.constModifyKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
DistinctKeys (Const.modifyKey a f l)
theorem Std.Internal.List.guard_eq_map {α : Type u} {β : α → Type v} (p : (a : α) × β a → Prop) [DecidablePred p] :
theorem Std.Internal.List.getEntry?_filterMap' {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [EquivBEq α] {f : (a : α) × β a → Option ((a : α) × γ a)} (hf : ∀ (p : (a : α) × β a), Option.all (fun (x : (a : α) × γ a) => x.fst == p.fst) (f p) = true) {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getEntry?_filter {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {f : (a : α) × β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCast?_filter_containsKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
getValueCast? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = if containsKey k l₂ = true then getValueCast? k l₁ else none
theorem Std.Internal.List.getValueCast?_filter_not_contains {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) :
getValueCast? k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) = if l₂.contains k = true then none else getValueCast? k l₁
theorem Std.Internal.List.getValueCast?_filter_not_contains_map_fst {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
getValueCast? k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) = if containsKey k l₂ = true then none else getValueCast? k l₁
theorem Std.Internal.List.getValueCast?_filter_not_contains_of_contains_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) :
l₂.contains k = false →
getValueCast? k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) = getValueCast? k l₁
theorem Std.Internal.List.getValueCast?_filter_not_contains_map_fst_of_containsKey_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = false →
getValueCast? k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) = getValueCast? k l₁
theorem Std.Internal.List.getValueCast?_filter_not_contains_of_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false → getValueCast? k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) = none
theorem Std.Internal.List.getValueCast?_filter_not_contains_map_fst_of_containsKey_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false →
getValueCast? k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) = none
theorem Std.Internal.List.getValueCast?_filter_not_contains_of_contains_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) :
l₂.contains k = true → getValueCast? k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) = none
theorem Std.Internal.List.getValueCast?_filter_not_contains_map_fst_of_containsKey_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = true →
getValueCast? k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) = none
theorem Std.Internal.List.getKey?_filter_containsKey {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
getKey? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = if containsKey k l₂ = true then getKey? k l₁ else none
theorem Std.Internal.List.getKey?_filter_containsKey_of_containsKey_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = true → getKey? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = getKey? k l₁
theorem Std.Internal.List.eraseList_perm_filter_not_contains {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] (l toErase : List ((a : α) × β a)) (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey?_filter_containsKey_of_containsKey_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false → getKey? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = none
theorem Std.Internal.List.getKey?_filter_containsKey_of_containsKey_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = false → getKey? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = none
theorem Std.Internal.List.getValueCast?_filter_containsKey_of_containsKey_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = true →
getValueCast? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = getValueCast? k l₁
theorem Std.Internal.List.getValueCast?_filter_containsKey_of_containsKey_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false → getValueCast? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = none
theorem Std.Internal.List.getValueCast?_filter_containsKey_of_containsKey_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = false → getValueCast? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = none
theorem Std.Internal.List.getEntry?_filter_containsKey {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
getEntry? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = if containsKey k l₂ = true then getEntry? k l₁ else none
theorem Std.Internal.List.getEntry?_filter_containsKey_of_containsKey_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = true →
getEntry? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = getEntry? k l₁
theorem Std.Internal.List.getEntry?_filter_containsKey_of_containsKey_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false → getEntry? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = none
theorem Std.Internal.List.getEntry?_filter_containsKey_of_containsKey_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = false → getEntry? k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = none
theorem Std.Internal.List.getEntry?_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [EquivBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getEntry?_map {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [EquivBEq α] {f : (a : α) → β a → γ a} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.containsKey_filter_containsKey {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} :
containsKey k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = (containsKey k l₁ && containsKey k l₂)
theorem Std.Internal.List.containsKey_filter_containsKey_iff {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} :
containsKey k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = true ↔ containsKey k l₁ = true ∧ containsKey k l₂ = true
theorem Std.Internal.List.containsKey_filter_not_contains {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {hl₁ : DistinctKeys l₁} {k : α} :
containsKey k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) = (containsKey k l₁ && !l₂.contains k)
theorem Std.Internal.List.containsKey_filter_not_contains_map_fst {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} :
containsKey k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) = (containsKey k l₁ && !containsKey k l₂)
theorem Std.Internal.List.containsKey_filter_not_contains_iff {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {hl₁ : DistinctKeys l₁} {k : α} :
theorem Std.Internal.List.containsKey_filter_not_contains_map_fst_iff {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} :
containsKey k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) = true ↔ containsKey k l₁ = true ∧ ¬containsKey k l₂ = true
theorem Std.Internal.List.getValueCast_filter_not_contains {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) {h₁ : containsKey k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) = true} {h₂ : containsKey k l₁ = true} :
getValueCast k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) h₁ = getValueCast k l₁ h₂
theorem Std.Internal.List.getValueCast_filter_not_contains_map_fst {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) {h₁ : containsKey k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) = true} {h₂ : containsKey k l₁ = true} :
getValueCast k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) h₁ = getValueCast k l₁ h₂
theorem Std.Internal.List.getValueCast_filter_containsKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) {h₁ : containsKey k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = true} {h₂ : containsKey k l₁ = true} :
getValueCast k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) h₁ = getValueCast k l₁ h₂
theorem Std.Internal.List.getEntry_filter_containsKey {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) {h₁ : containsKey k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = true} {h₂ : containsKey k l₁ = true} :
theorem Std.Internal.List.getKey_filter_containsKey {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) {h₁ : containsKey k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = true} {h₂ : containsKey k l₁ = true} :
theorem Std.Internal.List.containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} :
containsKey k l₁ = false → containsKey k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = false
theorem Std.Internal.List.containsKey_filter_not_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {hl₁ : DistinctKeys l₁} {k : α} :
containsKey k l₁ = false → containsKey k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) = false
theorem Std.Internal.List.containsKey_filter_not_contains_map_fst_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} :
containsKey k l₁ = false →
containsKey k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) = false
theorem Std.Internal.List.containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} :
containsKey k l₂ = false → containsKey k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) = false
theorem Std.Internal.List.perm_filter_containsKey_of_perm {α : Type u} {β : α → Type v} {l₁ l₂ l₃ : List ((a : α) × β a)} [BEq α] [EquivBEq α] (h : l₂.Perm l₃) (wf₁ : DistinctKeys l₁) :
(List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁).Perm
(List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₃) l₁)
theorem Std.Internal.List.perm_filter_not_contains_map_fst_of_perm {α : Type u} {β : α → Type v} {l₁ l₂ l₃ : List ((a : α) × β a)} [BEq α] [EquivBEq α] (h : l₂.Perm l₃) (wf₁ : DistinctKeys l₁) :
theorem Std.Internal.List.congr_filter_containsKey_of_perm {α : Type u} {β : α → Type v} {l₁ l₂ l₃ l₄ : List ((a : α) × β a)} [BEq α] [EquivBEq α] (h₁ : l₁.Perm l₃) (h₂ : l₂.Perm l₄) (hd : DistinctKeys l₃) :
(List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁).Perm
(List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₄) l₃)
theorem Std.Internal.List.congr_filter_not_contains_map_fst_of_perm {α : Type u} {β : α → Type v} {l₁ l₂ l₃ l₄ : List ((a : α) × β a)} [BEq α] [EquivBEq α] (h₁ : l₁.Perm l₃) (h₂ : l₂.Perm l₄) (hd : DistinctKeys l₃) :
theorem Std.Internal.List.containsKey_filter_not_contains_of_contains_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {hl₁ : DistinctKeys l₁} {k : α} :
l₂.contains k = true → containsKey k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) = false
theorem Std.Internal.List.containsKey_filter_not_contains_map_fst_of_contains_map_fst_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} :
containsKey k l₂ = true →
containsKey k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) = false
theorem Std.Internal.List.getValueCastD_filter_not_contains {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
getValueCastD k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) fallback = if l₂.contains k = true then fallback else getValueCastD k l₁ fallback
theorem Std.Internal.List.getValueCastD_filter_not_contains_map_fst {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
getValueCastD k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback = if containsKey k l₂ = true then fallback else getValueCastD k l₁ fallback
theorem Std.Internal.List.getKey?_filter_not_contains {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKey?_filter_not_contains_map_fst {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKey?_filter_not_contains_of_contains_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKey?_filter_not_contains_map_fst_of_containsKey_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKey?_filter_not_contains_of_containsKey_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false → getKey? k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) = none
theorem Std.Internal.List.getKey?_filter_not_contains_map_fst_of_containsKey_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKey?_filter_not_contains_of_containsKey_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKey?_filter_not_contains_map_fst_of_containsKey_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKey_filter_not_contains {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) {h₁ : containsKey k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) = true} {h₂ : containsKey k l₁ = true} :
theorem Std.Internal.List.getKey_filter_not_contains_map_fst {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} (dl₁ : DistinctKeys l₁) {h₁ : containsKey k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) = true} {h₂ : containsKey k l₁ = true} :
theorem Std.Internal.List.getKeyD_filter_not_contains {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k fallback : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKeyD_filter_not_contains_map_fst {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKeyD_filter_not_contains_of_contains_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k fallback : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKeyD_filter_not_contains_map_fst_of_contains_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKeyD_filter_not_contains_of_contains_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k fallback : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKeyD_filter_not_contains_map_fst_of_contains_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getKeyD_filter_not_contains_of_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k fallback : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false →
getKeyD k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) fallback = fallback
theorem Std.Internal.List.getKeyD_filter_not_contains_map_fst_of_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValueCastD_filter_not_contains_of_containsKey_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false →
getValueCastD k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) fallback = fallback
theorem Std.Internal.List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false →
getValueCastD k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback = fallback
theorem Std.Internal.List.length_filter_not_contains_eq_length_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} (hl₁ : DistinctKeys l₁) (w : ∀ (a : α), containsKey a l₁ = true → l₂.contains a = false) :
theorem Std.Internal.List.length_filter_not_contains_map_fst_eq_length_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) (w : ∀ (a : α), containsKey a l₁ = true → containsKey a l₂ = false) :
theorem Std.Internal.List.size_filter_not_contains_add_size_inter_eq_size_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.size_filter_not_contains_map_fst_add_size_inter_eq_size_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (dl₁ : DistinctKeys l₁) :
(List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁).length + (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁).length = l₁.length
theorem Std.Internal.List.isEmpty_filter_not_contains_iff {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.isEmpty_filter_not_contains_map_fst_iff {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValue?_filter_not_contains {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValue?_filter_not_contains_map_fst {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValue?_filter_not_contains_of_contains_eq_false_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValue?_filter_not_contains_map_fst_of_contains_eq_false_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValue?_filter_not_contains_of_containsKey_eq_false_left {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false → getValue? k (List.filter (fun (p : (_ : α) × β) => !l₂.contains p.fst) l₁) = none
theorem Std.Internal.List.getValue?_filter_not_contains_map_fst_of_containsKey_eq_false_left {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValue?_filter_not_contains_map_fst_of_contains_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValue_filter_not_contains {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} (dl₁ : DistinctKeys l₁) {h₁ : containsKey k (List.filter (fun (p : (_ : α) × β) => !l₂.contains p.fst) l₁) = true} {h₂ : containsKey k l₁ = true} :
theorem Std.Internal.List.getValue_filter_not_contains_map_fst {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} (dl₁ : DistinctKeys l₁) {h₁ : containsKey k (List.filter (fun (p : (_ : α) × β) => !(List.map Sigma.fst l₂).contains p.fst) l₁) = true} {h₂ : containsKey k l₁ = true} :
theorem Std.Internal.List.getValueD_filter_not_contains {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValueD_filter_not_contains_map_fst {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValueD_filter_not_contains_of_containsKey_eq_false_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValueD_filter_not_contains_of_contains_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValueD_filter_not_contains_map_fst_of_contains_map_fst_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValueD_filter_not_contains_of_containsKey_eq_false_left {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false →
getValueD k (List.filter (fun (p : (_ : α) × β) => !l₂.contains p.fst) l₁) fallback = fallback
theorem Std.Internal.List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_left {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
theorem Std.Internal.List.getValueCastD_filter_not_contains_of_contains_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
l₂.contains k = true →
getValueCastD k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) fallback = fallback
theorem Std.Internal.List.getValueCastD_filter_not_contains_map_fst_of_contains_map_fst_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = true →
getValueCastD k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback = fallback
theorem Std.Internal.List.List.getValue?_filter_containsKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} (dl₁ : DistinctKeys l₁) :
getValue? k (List.filter (fun (p : (_ : α) × β) => containsKey p.fst l₂) l₁) = if containsKey k l₂ = true then getValue? k l₁ else none
theorem Std.Internal.List.List.getValue?_filter_containsKey_of_containsKey_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = true → getValue? k (List.filter (fun (p : (_ : α) × β) => containsKey p.fst l₂) l₁) = getValue? k l₁
theorem Std.Internal.List.List.getValue?_filter_containsKey_of_containsKey_eq_false_left {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false → getValue? k (List.filter (fun (p : (_ : α) × β) => containsKey p.fst l₂) l₁) = none
theorem Std.Internal.List.getValue?_filter_containsKey_of_containsKey_eq_false_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = false → getValue? k (List.filter (fun (p : (_ : α) × β) => containsKey p.fst l₂) l₁) = none
theorem Std.Internal.List.getValueCastD_filter_containsKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
getValueCastD k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) fallback = if containsKey k l₂ = true then getValueCastD k l₁ fallback else fallback
theorem Std.Internal.List.getValueCastD_filter_containsKey_of_containsKey_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = true →
getValueCastD k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) fallback = getValueCastD k l₁ fallback
theorem Std.Internal.List.getValueCastD_filter_containsKey_of_containsKey_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false →
getValueCastD k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) fallback = fallback
theorem Std.Internal.List.getValueCastD_filter_containsKey_of_containsKey_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = false →
getValueCastD k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) fallback = fallback
theorem Std.Internal.List.getValueCastD_filter_not_contains_of_contains_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
l₂.contains k = false →
getValueCastD k (List.filter (fun (p : (a : α) × β a) => !l₂.contains p.fst) l₁) fallback = getValueCastD k l₁ fallback
theorem Std.Internal.List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : β k} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = false →
getValueCastD k (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback = getValueCastD k l₁ fallback
theorem Std.Internal.List.getKeyD_filter_containsKey {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α} (dl₁ : DistinctKeys l₁) :
getKeyD k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) fallback = if containsKey k l₂ = true then getKeyD k l₁ fallback else fallback
theorem Std.Internal.List.getKeyD_filter_containsKey_of_containsKey_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = true →
getKeyD k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) fallback = getKeyD k l₁ fallback
theorem Std.Internal.List.getKeyD_filter_containsKey_of_containsKey_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false →
getKeyD k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) fallback = fallback
theorem Std.Internal.List.getKeyD_filter_containsKey_of_containsKey_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = false →
getKeyD k (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁) fallback = fallback
theorem Std.Internal.List.List.getValue_filter_containsKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} (dl₁ : DistinctKeys l₁) {h₁ : containsKey k (List.filter (fun (p : (_ : α) × β) => containsKey p.fst l₂) l₁) = true} {h₂ : containsKey k l₁ = true} :
theorem Std.Internal.List.List.getValueD_filter_containsKey {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
getValueD k (List.filter (fun (p : (_ : α) × β) => containsKey p.fst l₂) l₁) fallback = if containsKey k l₂ = true then getValueD k l₁ fallback else fallback
theorem Std.Internal.List.List.getValueD_filter_containsKey_of_containsKey_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = true →
getValueD k (List.filter (fun (p : (_ : α) × β) => containsKey p.fst l₂) l₁) fallback = getValueD k l₁ fallback
theorem Std.Internal.List.getValueD_filter_containsKey_of_containsKey_eq_false_left {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
containsKey k l₁ = false →
getValueD k (List.filter (fun (p : (_ : α) × β) => containsKey p.fst l₂) l₁) fallback = fallback
theorem Std.Internal.List.getValueD_filter_containsKey_of_containsKey_eq_false_right {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} (dl₁ : DistinctKeys l₁) :
containsKey k l₂ = false →
getValueD k (List.filter (fun (p : (_ : α) × β) => containsKey p.fst l₂) l₁) fallback = fallback
theorem Std.Internal.List.containsKey_of_containsKey_filterMap' {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [EquivBEq α] {f : (a : α) × β a → Option ((a : α) × γ a)} (hf : ∀ (p : (a : α) × β a), Option.all (fun (x : (a : α) × γ a) => x.fst == p.fst) (f p) = true) {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) (h : containsKey k (List.filterMap f l) = true) :
theorem Std.Internal.List.containsKey_of_containsKey_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [EquivBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) (h :
containsKey k
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = true) :
theorem Std.Internal.List.isSome_apply_of_containsKey_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) (h :
containsKey k
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = true) :
theorem Std.Internal.List.Const.isSome_apply_of_containsKey_filterMap {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) (h :
containsKey k (List.filterMap (fun (p : (_ : α) × β) => Option.map (fun (x : γ) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = true) :
theorem Std.Internal.List.containsKey_of_containsKey_filter {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) (h : containsKey k (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l) = true) :
theorem Std.Internal.List.Const.containsKey_filterMap {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
containsKey k (List.filterMap (fun (p : (_ : α) × β) => Option.map (fun (x : γ) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = if h : containsKey k l = true then (f (getKey k l h) (getValue k l h)).isSome else false
theorem Std.Internal.List.Const.containsKey_filter {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
containsKey k (List.filter (fun (p : (_ : α) × β) => f p.fst p.snd) l) = if h : containsKey k l = true then f (getKey k l h) (getValue k l h) else false
theorem Std.Internal.List.apply_eq_true_of_containsKey_filter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) (h : containsKey k (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l) = true) :
theorem Std.Internal.List.getValueCast?_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
getValueCast? k
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = (getValueCast? k l).bind (f k)
theorem Std.Internal.List.getValueCast!_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} [Inhabited (γ k)] (hl : DistinctKeys l) :
getValueCast! k
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = ((getValueCast? k l).bind (f k)).get!
theorem Std.Internal.List.getValueCastD_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) {fallback : γ k} :
getValueCastD k
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l)
fallback = ((getValueCast? k l).bind (f k)).getD fallback
theorem Std.Internal.List.getValueCast?_filter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
getValueCast? k (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l) = Option.filter (f k) (getValueCast? k l)
theorem Std.Internal.List.getValueCast!_filter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (hl : DistinctKeys l) :
getValueCast! k (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l) = (Option.filter (f k) (getValueCast? k l)).get!
theorem Std.Internal.List.getValueCastD_filter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) {fallback : β k} :
getValueCastD k (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l) fallback = (Option.filter (f k) (getValueCast? k l)).getD fallback
theorem Std.Internal.List.getValueCast?_map {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → γ a} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
getValueCast? k (List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) l) = Option.map (f k) (getValueCast? k l)
theorem Std.Internal.List.getValueCast!_map {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → γ a} {l : List ((a : α) × β a)} {k : α} [Inhabited (γ k)] (hl : DistinctKeys l) :
getValueCast! k (List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) l) = (Option.map (f k) (getValueCast? k l)).get!
theorem Std.Internal.List.getValueCastD_map {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → γ a} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) {fallback : γ k} :
getValueCastD k (List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) l) fallback = (Option.map (f k) (getValueCast? k l)).getD fallback
theorem Std.Internal.List.getValueCast_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) (h :
containsKey k
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = true) :
getValueCast k
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) h = (f k (getValueCast k l ⋯)).get ⋯
theorem Std.Internal.List.getValueCast_filter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) (h : containsKey k (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l) = true) :
theorem Std.Internal.List.getValueCast_map {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → γ a} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) (h : containsKey k (List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) l) = true) :
getValueCast k (List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) l) h = f k (getValueCast k l ⋯)
theorem Std.Internal.List.containsKey_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
containsKey k
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = Option.any (fun (x : β k) => (f k x).isSome) (getValueCast? k l)
theorem Std.Internal.List.containsKey_filter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
containsKey k (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l) = Option.any (f k) (getValueCast? k l)
theorem Std.Internal.List.containsKey_filter_key {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.containsKey_filterMap_iff {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
containsKey k
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = true ↔ ∃ (h : containsKey k l = true), (f k (getValueCast k l h)).isSome = true
theorem Std.Internal.List.containsKey_filter_iff {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
containsKey k (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l) = true ↔ ∃ (h : containsKey k l = true), f k (getValueCast k l h) = true
theorem Std.Internal.List.insertEntry_perm_filter {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] (k : α) (v : β k) {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.map_insertEntry_perm_filter_map {α : Type u} {β : Type v} [BEq α] [EquivBEq α] (k : α) (v : β) {l : List ((_ : α) × β)} (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.containsKey_filterMap_iff {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {f : α → β → Option γ} {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.containsKey_filter_iff {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {f : α → β → Bool} {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey?_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey!_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] [Inhabited α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKeyD_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k fallback : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getValueCast_eq_get_getValueCast? {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {a : α} {l : List ((a : α) × β a)} {h : containsKey a 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) {h : containsKey k (insertList l toInsert) = true} :
theorem Std.Internal.List.getKey?_filter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey?_filter_key {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey!_filter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Inhabited α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey!_filter_key {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] [Inhabited α] {f : α → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
getKey! k (List.filter (fun (p : (a : α) × β a) => f p.fst) l) = (Option.filter f (getKey? k l)).get!
theorem Std.Internal.List.getKeyD_filter {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k fallback : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKeyD_filter_key {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)} {k fallback : α} (hl : DistinctKeys l) :
getKeyD k (List.filter (fun (p : (a : α) × β a) => f p.fst) l) fallback = (Option.filter f (getKey? k l)).getD fallback
theorem Std.Internal.List.getKeyD_map {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [EquivBEq α] {f : (a : α) → β a → γ a} {l : List ((a : α) × β a)} {k fallback : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.getKey_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [EquivBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) {h :
containsKey k
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = true} :
theorem Std.Internal.List.getKey_filter {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) {h : containsKey k (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l) = true} :
theorem Std.Internal.List.getValue_filterMap {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) {h :
containsKey k (List.filterMap (fun (p : (_ : α) × β) => Option.map (fun (x : γ) => ⟨p.fst, x⟩) (f p.fst p.snd)) l) = true} :
theorem Std.Internal.List.getValue_filter {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) {h : containsKey k (List.filter (fun (p : (_ : α) × β) => f p.fst p.snd) l) = true} :
theorem Std.Internal.List.length_filterMap_eq_length_iff {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} (distinct : DistinctKeys l) :
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l).length = l.length ↔ ∀ (a : α) (h : containsKey a l = true), (f a (getValueCast a l h)).isSome = true
theorem Std.Internal.List.forall_mem_iff_forall_contains_getValueCast {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {p : (a : α) → β a → Prop} (distinct : DistinctKeys l) :
(∀ (x : (a : α) × β a), x ∈ l → p x.fst x.snd) ↔ ∀ (a : α) (h : containsKey a l = true), p a (getValueCast a l h)
theorem Std.Internal.List.length_filter_eq_length_iff {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} (distinct : DistinctKeys l) :
(List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l).length = l.length ↔ ∀ (a : α) (h : containsKey a l = true), f a (getValueCast a l h) = true
theorem Std.Internal.List.length_filter_key_eq_length_iff {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.length_filter_containsKey_eq_length_left {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) (w : ∀ (a : α), containsKey a l₁ = true → containsKey a l₂ = true) :
theorem Std.Internal.List.length_filter_containsKey_of_length_right {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys l₂) (w : ∀ (a : α), containsKey a l₂ = true → containsKey a l₁ = true) :
theorem Std.Internal.List.size_add_size_eq_size_insertList_add_size_filter_containsKey {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys l₂) :
l₁.length + l₂.length = (insertList l₁ l₂).length + (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁).length
theorem Std.Internal.List.length_filter_containsKey_le {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (dl₁ : DistinctKeys l₂) (dl₂ : DistinctKeys l₁) :
theorem Std.Internal.List.isEmpty_filter_containsKey_iff {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (dl₁ : DistinctKeys l₁) :
(List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁).isEmpty = true ↔ ∀ (k : α), containsKey k l₁ = true → containsKey k l₂ = false
theorem Std.Internal.List.isEmpty_filter_containsKey_comm {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (dl₁ : DistinctKeys l₁) (dl₂ : DistinctKeys l₂) :
(List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₂) l₁).isEmpty = (List.filter (fun (p : (a : α) × β a) => containsKey p.fst l₁) l₂).isEmpty
theorem Std.Internal.List.perm_filter_self_iff_forall_containsKey {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
(List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l).Perm l ↔ ∀ (a : α) (h : containsKey a l = true), f a (getValueCast a l h) = true
theorem Std.Internal.List.perm_filter_key_self_iff_forall_containsKey {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
(List.filter (fun (p : (a : α) × β a) => f p.fst) l).Perm l ↔ ∀ (a : α) (h : containsKey a l = true), f (getKey a l h) = true
theorem Std.Internal.List.Const.perm_filter_self_iff_forall_containsKey {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} (hl : DistinctKeys l) :
theorem Std.Internal.List.isEmpty_filterMap_eq_true {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} (distinct : DistinctKeys l) :
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) l).isEmpty = true ↔ ∀ (k : α) (h : containsKey k l = true), f k (getValueCast k l h) = none
theorem Std.Internal.List.isEmpty_filterMap_eq_false {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} (distinct : DistinctKeys l) :
theorem Std.Internal.List.isEmpty_filter_eq_true {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} (distinct : DistinctKeys l) :
(List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l).isEmpty = true ↔ ∀ (k : α) (h : containsKey k l = true), f k (getValueCast k l h) = false
theorem Std.Internal.List.isEmpty_filter_eq_false {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} (distinct : DistinctKeys l) :
theorem Std.Internal.List.isEmpty_filter_key_iff {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.perm_of_beqModel {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [(k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)] {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys l₂) :
theorem Std.Internal.List.Const.perm_of_beqModel {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {l₁ l₂ : List ((_ : α) × β)} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys l₂) :
theorem Std.Internal.List.Const.forall_mem_iff_forall_contains_getKey_getValue {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {l : List ((_ : α) × β)} {p : α → β → Prop} (distinct : DistinctKeys l) :
theorem Std.Internal.List.Const.getValue?_filterMap {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {f : α → β → Option γ} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k : α} :
theorem Std.Internal.List.Const.getValue?_filterMap_of_getKey?_eq_some {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {f : α → β → Option γ} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k k' : α} :
theorem Std.Internal.List.Const.getValue!_filterMap {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] [Inhabited γ] {f : α → β → Option γ} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k : α} :
theorem Std.Internal.List.Const.getValue!_filterMap_of_getKey?_eq_some {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] [Inhabited γ] {f : α → β → Option γ} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k k' : α} :
theorem Std.Internal.List.Const.getValueD_filterMap {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {fallback : γ} {f : α → β → Option γ} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k : α} :
theorem Std.Internal.List.Const.getValueD_filterMap_of_getKey?_eq_some {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {f : α → β → Option γ} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k k' : α} {fallback : γ} :
theorem Std.Internal.List.Const.getValue?_filter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {f : α → β → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k : α} :
theorem Std.Internal.List.Const.getValue?_filter_of_getKey?_eq_some {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {f : α → β → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k k' : α} :
getKey? k l = some k' →
getValue? k (List.filter (fun (p : (_ : α) × β) => f p.fst p.snd) l) = Option.filter (fun (x : β) => f k' x) (getValue? k l)
theorem Std.Internal.List.Const.getValue!_filter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited β] {f : α → β → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k : α} :
theorem Std.Internal.List.Const.getValue!_filter_of_getKey?_eq_some {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Inhabited β] {f : α → β → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k k' : α} :
theorem Std.Internal.List.Const.getValueD_filter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {fallback : β} {f : α → β → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k : α} :
theorem Std.Internal.List.Const.getValueD_filter_of_getKey?_eq_some {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {fallback : β} {f : α → β → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) {k k' : α} (h : getKey? k l = some k') :
getValueD k (List.filter (fun (p : (_ : α) × β) => f p.fst p.snd) l) fallback = (Option.filter (fun (x : β) => f k' x) (getValue? k l)).getD fallback
theorem Std.Internal.List.Const.getValue?_map {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {f : α → β → γ} {l : List ((_ : α) × β)} (hl : DistinctKeys l) {k : α} :
theorem Std.Internal.List.Const.getValue!_map {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] [Inhabited γ] {f : α → β → γ} {l : List ((_ : α) × β)} (hl : DistinctKeys l) {k : α} :
theorem Std.Internal.List.Const.getValueD_map {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {fallback : γ} {f : α → β → γ} {l : List ((_ : α) × β)} (hl : DistinctKeys l) {k : α} :
theorem Std.Internal.List.Const.getKey?_filterMap {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getKey!_filterMap {α : Type u} [BEq α] [EquivBEq α] [Inhabited α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getKeyD_filterMap {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)} {k fallback : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getKey?_filter {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getKey!_filter {α : Type u} [BEq α] [EquivBEq α] [Inhabited α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.getKeyD_filter {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} {k fallback : α} (hl : DistinctKeys l) :
theorem Std.Internal.List.Const.length_filterMap_eq_length_iff {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {f : α → β → Option γ} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
theorem Std.Internal.List.Const.length_filter_eq_length_iff {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {f : α → β → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
theorem Std.Internal.List.Const.length_filter_key_eq_length_iff {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {f : α → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
theorem Std.Internal.List.Const.isEmpty_filterMap_eq_true {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
theorem Std.Internal.List.Const.isEmpty_filterMap_eq_false {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
theorem Std.Internal.List.Const.isEmpty_filter_eq_true {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
theorem Std.Internal.List.Const.isEmpty_filter_eq_false {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
theorem Std.Internal.List.Const.isEmpty_filter_key_eq_true {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {f : α → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
theorem Std.Internal.List.Const.isEmpty_filter_key_eq_false {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {f : α → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
theorem Std.Internal.List.Const.toList_map' {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {l : List ((_ : α) × β)} :
theorem Std.Internal.List.Const.toList_map {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {l : List ((_ : α) × β)} :
theorem Std.Internal.List.minEntry?_eq_head? {α : Type u} {β : α → Type v} [Ord α] {l : List ((a : α) × β a)} (hl : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) :
theorem Std.Internal.List.minKey?_eq_some_iff_getKey?_eq_self_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.minKey?_eq_some_iff_mem_and_forall {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.minEntry?_of_perm {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.minKey?_of_perm {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.minEntry?_replaceEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.minEntry?_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.minKey?_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.isSome_minEntry?_insert {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.isSome_minKey?_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.minKey?_bind_getEntry? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.getKey_minKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} {hc : containsKey km l = true} (hkm : (minKey? l).get ⋯ = km) :
theorem Std.Internal.List.getKeyD_minKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km fallback : α} (hkm : minKey? l = some km) :
theorem Std.Internal.List.minKey?_bind_getKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.containsKey_minKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} (hkm : minKey? l = some km) :
theorem Std.Internal.List.min?_keys {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [LE α] [LawfulOrderOrd α] [Min α] [LawfulOrderLeftLeaningMin α] (l : List ((a : α) × β a)) :
theorem Std.Internal.List.head?_keys {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [LE α] [LawfulOrderOrd α] [Min α] [LawfulOrderLeftLeaningMin α] (l : List ((a : α) × β a)) (hs : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) :
theorem Std.Internal.List.minKey?_insertEntry_le_minKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) {km kmi : α} (hkm : minKey? l = some km) (hkmi : (minKey? (insertEntry k v l)).get ⋯ = kmi) :
theorem Std.Internal.List.minKey?_insertEntry_le_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) {kmi : α} (hkmi : (minKey? (insertEntry k v l)).get ⋯ = kmi) :
theorem Std.Internal.List.minKey?_le_of_containsKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k km : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hc : containsKey k l = true) (hkm : (minKey? l).get ⋯ = km) :
theorem Std.Internal.List.le_minKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.containsKey_minKey?_eraseKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {kme : α} (hkme : minKey? (eraseKey k l) = some kme) :
theorem Std.Internal.List.minEntry?_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.minKey?_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.isSome_minEntry?_insertIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.isSome_minKey?_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
theorem Std.Internal.List.minKey?_insertEntryIfNew_le_minKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) {km kmi : α} (hkm : minKey? l = some km) (hkmi : (minKey? (insertEntryIfNew k v l)).get ⋯ = kmi) :
theorem Std.Internal.List.minKey?_insertEntryIfNew_le_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k kmi : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) (hkmi : (minKey? (insertEntryIfNew k v l)).get ⋯ = kmi) :
theorem Std.Internal.List.minKey?_eq_head?_keys {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) :
theorem Std.Internal.List.minKey?_modifyKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : β k → β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.minKey?_alterKey_eq_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.Const.minKey?_modifyKey_eq_minKey? {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : β → β} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
theorem Std.Internal.List.Const.minKey?_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
theorem Std.Internal.List.minKey_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} {km : α} :
theorem Std.Internal.List.minKey_eq_iff_mem_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} {km : α} :
theorem Std.Internal.List.minKey_insertEntry_le_minKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {he : l.isEmpty = false} :
theorem Std.Internal.List.minKey_insertEntry_le_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.containsKey_minKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} :
theorem Std.Internal.List.minKey_le_of_containsKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) :
theorem Std.Internal.List.minKey_eraseKey_eq_iff_beq_minKey_eq_false {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {he : (eraseKey k l).isEmpty = false} :
theorem Std.Internal.List.minKey_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.minKey_insertEntryIfNew_le_minKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {he : l.isEmpty = false} :
theorem Std.Internal.List.minKey_insertEntryIfNew_le_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.minKey_modifyKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : β k → β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : (modifyKey k f l).isEmpty = false} :
theorem Std.Internal.List.minKey_alterKey_eq_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k) → Option (β k)} {he : (alterKey k f l).isEmpty = false} :
theorem Std.Internal.List.Const.minKey_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} {he : (modifyKey k f l).isEmpty = false} :
theorem Std.Internal.List.Const.minKey_modifyKey_eq_minKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} {he : (modifyKey k f l).isEmpty = false} :
theorem Std.Internal.List.Const.minKey_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : Option β → Option β} {he : (alterKey k f l).isEmpty = false} :
theorem Std.Internal.List.minKey!_of_perm {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l l' : List ((a : α) × β a)} (hd : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.minKey!_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km : α} :
theorem Std.Internal.List.minKey!_eq_iff_mem_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km : α} :
theorem Std.Internal.List.minKey!_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.minKey!_insertEntry_le_minKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} :
theorem Std.Internal.List.minKey!_insertEntry_le_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.containsKey_minKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
theorem Std.Internal.List.minKey!_le_of_containsKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) :
theorem Std.Internal.List.le_minKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} :
theorem Std.Internal.List.getKey_minKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : containsKey (minKey! l) l = true} :
theorem Std.Internal.List.getKey_minKey!_eq_minKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : containsKey (minKey! l) l = true} :
theorem Std.Internal.List.minKey!_eraseKey_eq_iff_beq_minKey!_eq_false {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) :
theorem Std.Internal.List.minKey!_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.minKey!_insertEntryIfNew_le_minKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} :
theorem Std.Internal.List.minKey!_insertEntryIfNew_le_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.minKey!_eq_head!_keys {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) :
theorem Std.Internal.List.minKey!_modifyKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : β k → β k} :
theorem Std.Internal.List.minKey!_alterKey_eq_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k) → Option (β k)} (he : (alterKey k f l).isEmpty = false) :
theorem Std.Internal.List.Const.minKey!_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} (he : (modifyKey k f l).isEmpty = false) :
theorem Std.Internal.List.Const.minKey!_modifyKey_eq_minKey! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} :
theorem Std.Internal.List.minKeyD_of_perm {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} {fallback : α} (hd : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.minKey_insertEntry_of_isEmpty {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty = true) :
theorem Std.Internal.List.minKey?_insertEntry_of_isEmpty {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty = true) :
theorem Std.Internal.List.minKeyD_insertEntry_of_isEmpty {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty = true) {fallback : α} :
theorem Std.Internal.List.minKey!_insertEntry_of_isEmpty {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty = true) :
theorem Std.Internal.List.minKey_insertEntryIfNew_of_isEmpty {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty = true) :
theorem Std.Internal.List.minKey?_insertEntryIfNew_of_isEmpty {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty = true) :
theorem Std.Internal.List.minKeyD_insertEntryIfNew_of_isEmpty {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty = true) {fallback : α} :
theorem Std.Internal.List.minKey!_insertEntryIfNew_of_isEmpty {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty = true) :
theorem Std.Internal.List.minKeyD_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km fallback : α} :
theorem Std.Internal.List.minKeyD_eq_iff_mem_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km fallback : α} :
theorem Std.Internal.List.minKeyD_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.minKeyD_insertEntry_le_minKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.minKeyD_insertEntry_le_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.containsKey_minKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback : α} :
theorem Std.Internal.List.minKeyD_le_of_containsKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) {fallback : α} :
theorem Std.Internal.List.le_minKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k fallback : α} :
theorem Std.Internal.List.getKey_minKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {fallback : α} {he : containsKey (minKeyD l fallback) l = true} :
theorem Std.Internal.List.getKey_minKeyD_eq_minKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {fallback : α} {he : containsKey (minKeyD l fallback) l = true} :
theorem Std.Internal.List.minKeyD_eraseKey_eq_iff_beq_minKeyD_eq_false {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k fallback : α} (he : (eraseKey k l).isEmpty = false) :
theorem Std.Internal.List.minKeyD_le_minKeyD_erase {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) {fallback : α} :
theorem Std.Internal.List.minKeyD_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.minKeyD_insertEntryIfNew_le_minKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.minKeyD_insertEntryIfNew_le_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.minKeyD_eq_headD_keys {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) {fallback : α} :
theorem Std.Internal.List.minKeyD_modifyKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : β k → β k} {fallback : α} :
theorem Std.Internal.List.minKeyD_alterKey_eq_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k) → Option (β k)} {fallback : α} (he : (alterKey k f l).isEmpty = false) :
theorem Std.Internal.List.Const.minKeyD_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} (he : (modifyKey k f l).isEmpty = false) {fallback : α} :
theorem Std.Internal.List.Const.minKeyD_modifyKey_eq_minKeyD {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} {fallback : α} :
theorem Std.Internal.List.Const.minKeyD_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : Option β → Option β} (he : (alterKey k f l).isEmpty = false) {fallback : α} :
theorem Std.Internal.List.maxKey?_eq_some_iff_getKey?_eq_self_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.maxKey?_eq_some_iff_mem_and_forall {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.maxKey?_of_perm {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.maxKey?_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.isSome_maxKey?_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.getKey_maxKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} {hc : containsKey km l = true} (hkm : (maxKey? l).get ⋯ = km) :
theorem Std.Internal.List.getKeyD_maxKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km fallback : α} (hkm : maxKey? l = some km) :
theorem Std.Internal.List.maxKey?_bind_getKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.containsKey_maxKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km : α} (hkm : maxKey? l = some km) :
theorem Std.Internal.List.maxKey?_le_maxKey?_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km kmi : α} (hkm : maxKey? l = some km) (hkmi : (maxKey? (insertEntry k v l)).get ⋯ = kmi) :
theorem Std.Internal.List.self_le_maxKey?_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {kmi : α} (hkmi : (maxKey? (insertEntry k v l)).get ⋯ = kmi) :
theorem Std.Internal.List.maxKey?_le_of_containsKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k km : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hc : containsKey k l = true) (hkm : (maxKey? l).get ⋯ = km) :
theorem Std.Internal.List.maxKey?_le {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.containsKey_maxKey?_eraseKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {kme : α} (hkme : maxKey? (eraseKey k l) = some kme) :
theorem Std.Internal.List.maxKey?_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.isSome_maxKey?_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.maxKey?_le_maxKey?_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km kmi : α} (hkm : maxKey? l = some km) (hkmi : (maxKey? (insertEntryIfNew k v l)).get ⋯ = kmi) :
theorem Std.Internal.List.self_le_maxKey?_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k kmi : α} {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hkmi : (maxKey? (insertEntryIfNew k v l)).get ⋯ = kmi) :
theorem Std.Internal.List.maxKey?_eq_getLast?_keys {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) :
theorem Std.Internal.List.maxKey?_modifyKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : β k → β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.maxKey?_alterKey_eq_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
theorem Std.Internal.List.Const.maxKey?_modifyKey_eq_maxKey? {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : β → β} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
theorem Std.Internal.List.Const.maxKey?_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
theorem Std.Internal.List.maxKey_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} {km : α} :
theorem Std.Internal.List.maxKey_eq_iff_mem_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} {km : α} :
theorem Std.Internal.List.maxKey_le_maxKey_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {he : l.isEmpty = false} :
theorem Std.Internal.List.self_le_maxKey_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.containsKey_maxKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : l.isEmpty = false} :
theorem Std.Internal.List.le_maxKey_of_containsKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) :
theorem Std.Internal.List.maxKey_eraseKey_eq_iff_beq_maxKey_eq_false {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {he : (eraseKey k l).isEmpty = false} :
theorem Std.Internal.List.maxKey_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.maxKey_le_maxKey_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {he : l.isEmpty = false} :
theorem Std.Internal.List.self_le_maxKey_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.maxKey_eq_getLast_keys {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) {he : l.isEmpty = false} :
theorem Std.Internal.List.maxKey_modifyKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k : α} {f : β k → β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : (modifyKey k f l).isEmpty = false} :
theorem Std.Internal.List.maxKey_alterKey_eq_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k) → Option (β k)} {he : (alterKey k f l).isEmpty = false} :
theorem Std.Internal.List.Const.maxKey_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} {he : (modifyKey k f l).isEmpty = false} :
theorem Std.Internal.List.Const.maxKey_modifyKey_eq_maxKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} {he : (modifyKey k f l).isEmpty = false} :
theorem Std.Internal.List.Const.maxKey_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : Option β → Option β} {he : (alterKey k f l).isEmpty = false} :
theorem Std.Internal.List.maxKey!_of_perm {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l l' : List ((a : α) × β a)} (hd : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.maxKey!_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km : α} :
theorem Std.Internal.List.maxKey!_eq_iff_mem_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km : α} :
theorem Std.Internal.List.maxKey!_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.maxKey!_le_maxKey!_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} :
theorem Std.Internal.List.self_le_maxKey!_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.containsKey_maxKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
theorem Std.Internal.List.le_maxKey!_of_containsKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) :
theorem Std.Internal.List.maxKey!_le {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} :
theorem Std.Internal.List.getKey_maxKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : containsKey (maxKey! l) l = true} :
theorem Std.Internal.List.getKey_maxKey!_eq_maxKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he : containsKey (maxKey! l) l = true} :
theorem Std.Internal.List.maxKey!_eraseKey_eq_iff_beq_maxKey!_eq_false {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) :
theorem Std.Internal.List.maxKey!_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.maxKey!_le_maxKey!_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} :
theorem Std.Internal.List.self_le_maxKey!_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} :
theorem Std.Internal.List.maxKey!_eq_getLast!_keys {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) :
theorem Std.Internal.List.maxKey!_modifyKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : β k → β k} :
theorem Std.Internal.List.maxKey!_alterKey_eq_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k) → Option (β k)} (he : (alterKey k f l).isEmpty = false) :
theorem Std.Internal.List.Const.maxKey!_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} (he : (modifyKey k f l).isEmpty = false) :
theorem Std.Internal.List.Const.maxKey!_modifyKey_eq_maxKey! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] [Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} :
theorem Std.Internal.List.maxKeyD_of_perm {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} {fallback : α} (hd : DistinctKeys l) (hp : l.Perm l') :
theorem Std.Internal.List.maxKeyD_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km fallback : α} :
theorem Std.Internal.List.maxKeyD_eq_iff_mem_and_forall {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km fallback : α} :
theorem Std.Internal.List.maxKeyD_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.maxKeyD_le_maxKeyD_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.self_le_maxKeyD_insertEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.containsKey_maxKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback : α} :
theorem Std.Internal.List.le_maxKeyD_of_containsKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (hc : containsKey k l = true) {fallback : α} :
theorem Std.Internal.List.maxKeyD_le {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k fallback : α} :
theorem Std.Internal.List.getKey_maxKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {fallback : α} {he : containsKey (maxKeyD l fallback) l = true} :
theorem Std.Internal.List.getKey_maxKeyD_eq_maxKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {fallback : α} {he : containsKey (maxKeyD l fallback) l = true} :
theorem Std.Internal.List.maxKeyD_eraseKey_eq_iff_beq_maxKeyD_eq_false {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k fallback : α} (he : (eraseKey k l).isEmpty = false) :
theorem Std.Internal.List.maxKeyD_eraseKey_le_maxKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} (he : (eraseKey k l).isEmpty = false) {fallback : α} :
theorem Std.Internal.List.maxKeyD_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.maxKeyD_le_maxKeyD_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.self_le_maxKeyD_insertEntryIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {v : β k} {fallback : α} :
theorem Std.Internal.List.maxKeyD_eq_getLastD_keys {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (ho : List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) l) {fallback : α} :
theorem Std.Internal.List.maxKeyD_modifyKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : β k → β k} {fallback : α} :
theorem Std.Internal.List.maxKeyD_alterKey_eq_self {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k : α} {f : Option (β k) → Option (β k)} {fallback : α} (he : (alterKey k f l).isEmpty = false) :
theorem Std.Internal.List.Const.maxKeyD_modifyKey {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} (he : (modifyKey k f l).isEmpty = false) {fallback : α} :
theorem Std.Internal.List.Const.maxKeyD_modifyKey_eq_maxKeyD {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : β → β} {fallback : α} :
theorem Std.Internal.List.Const.maxKeyD_alterKey_eq_self {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k : α} {f : Option β → Option β} (he : (alterKey k f l).isEmpty = false) {fallback : α} :
theorem Std.Internal.List.distinctKeys_interSmallerFn {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] (l sofar : List ((a : α) × β a)) (k : α) (hs : DistinctKeys sofar) :
DistinctKeys (interSmallerFn l sofar k)
theorem Std.Internal.List.getEntry?_interSmallerFn {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] (l sofar : List ((a : α) × β a)) (k k' : α) :
getEntry? k' (interSmallerFn l sofar k) = (Option.filter (fun (kv : (a : α) × β a) => k == kv.fst) (getEntry? k' l)).or (getEntry? k' sofar)
@[simp]
theorem Std.Internal.List.getEntry?_interSmaller {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] (l₁ l₂ : List ((a : α) × β a)) (k : α) :
getEntry? k (interSmaller l₁ l₂) = Option.filter (fun (kv : (a : α) × β a) => containsKey kv.fst l₂) (getEntry? k l₁)
theorem Std.Internal.List.distinctKeys_interSmaller {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {l₁ l₂ : List ((a : α) × β a)} :
DistinctKeys (interSmaller l₁ l₂)
theorem Std.Internal.List.interSmaller_perm_filter {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] (l₁ l₂ : List ((a : α) × β a)) (h₁ : DistinctKeys l₁) :
(interSmaller l₁ l₂).Perm (List.filter (fun (kv : (a : α) × β a) => containsKey kv.fst l₂) l₁)