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
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.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.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.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_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_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.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)}
:
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?_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.Option.dmap_bind
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(x : Option α)
(f : α → Option β)
(g : (a : β) → x.bind f = some a → γ)
:
Std.Internal.List.Option.dmap✝ (x.bind f) g = x.pbind fun (a : α) (h : x = some a) => Std.Internal.List.Option.dmap✝ (f a) fun (b : β) (h' : f a = some b) => g b ⋯
theorem
Std.Internal.List.Option.dmap_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(x : Option α)
(f : α → β)
(g : (a : β) → Option.map f x = some a → γ)
:
Std.Internal.List.Option.dmap✝ (Option.map f x) g = Std.Internal.List.Option.dmap✝ x fun (a : α) (h : x = some a) => g (f a) ⋯
theorem
Std.Internal.List.Option.map_dmap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(x : Option α)
(f : (a : α) → x = some a → β)
(g : β → γ)
:
Option.map g (Std.Internal.List.Option.dmap✝ x f) = Std.Internal.List.Option.dmap✝ x fun (a : α) (h : x = some a) => g (f a h)
theorem
Std.Internal.List.Option.dmap_ite
{α : Type u_1}
{β : Type u_2}
(p : Prop)
[Decidable p]
(t e : Option α)
(f : (a : α) → (if p then t else e) = some a → β)
:
Std.Internal.List.Option.dmap✝ (if p then t else e) f = if h : p then Std.Internal.List.Option.dmap✝ t fun (a : α) (h' : t = some a) => f a ⋯
else Std.Internal.List.Option.dmap✝ e fun (a : α) (h' : e = some a) => f a ⋯
theorem
Std.Internal.List.Option.get_dmap
{α : Type u_1}
{β : Type u_2}
{x : Option α}
{f : (a : α) → x = some a → β}
(h : (Std.Internal.List.Option.dmap✝ x f).isSome = true)
:
theorem
Std.Internal.List.guard_eq_map
{α : Type u}
{β : α → Type v}
(p : (a : α) × β a → Prop)
[DecidablePred p]
:
theorem
Std.Internal.List.Option.dmap_eq_map
{α : Type u_1}
{β : Type u_2}
{x : Option α}
{f : α → β}
:
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.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_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.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.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.key_getValueCast_mem
{α : Type u}
{β : α → Type v}
[BEq α]
[LawfulBEq α]
{l : List ((a : α) × β a)}
{a : α}
(h : containsKey a l = 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.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.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.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!_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.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_minKey_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_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!_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_maxKey_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_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 : α}
: