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
Equations
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
Equations
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
Equations
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
Equations
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
Equations
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.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₁)