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: relating operations on Raw to operations on Raw₀

theorem Std.DHashMap.Internal.Raw.empty_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {c : Nat} : Raw.empty c = (Raw₀.empty c).val

theorem Std.DHashMap.Internal.Raw.emptyc_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] : ∅ = Raw₀.empty.val

theorem Std.DHashMap.Internal.Raw.insert_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} : m.insert a b = (Raw₀.insert ⟨m, ⋯⟩ a b).val

theorem Std.DHashMap.Internal.Raw.insert_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} : m.val.insert a b = (m.insert a b).val

theorem Std.DHashMap.Internal.Raw.insertIfNew_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} : m.insertIfNew a b = (Raw₀.insertIfNew ⟨m, ⋯⟩ a b).val

theorem Std.DHashMap.Internal.Raw.insertIfNew_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} : m.val.insertIfNew a b = (m.insertIfNew a b).val

theorem Std.DHashMap.Internal.Raw.containsThenInsert_snd_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} : (m.containsThenInsert a b).snd = (Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).snd.val

theorem Std.DHashMap.Internal.Raw.containsThenInsert_snd_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} : (m.val.containsThenInsert a b).snd = (m.containsThenInsert a b).snd.val

theorem Std.DHashMap.Internal.Raw.containsThenInsert_fst_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} : (m.containsThenInsert a b).fst = (Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).fst

theorem Std.DHashMap.Internal.Raw.containsThenInsert_fst_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} : (m.val.containsThenInsert a b).fst = (m.containsThenInsert a b).fst

theorem Std.DHashMap.Internal.Raw.containsThenInsertIfNew_snd_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} : (m.containsThenInsertIfNew a b).snd = (Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).snd.val

theorem Std.DHashMap.Internal.Raw.containsThenInsertIfNew_snd_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} : (m.val.containsThenInsertIfNew a b).snd = (m.containsThenInsertIfNew a b).snd.val

theorem Std.DHashMap.Internal.Raw.containsThenInsertIfNew_fst_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} : (m.containsThenInsertIfNew a b).fst = (Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).fst

theorem Std.DHashMap.Internal.Raw.containsThenInsertIfNew_fst_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} : (m.val.containsThenInsertIfNew a b).fst = (m.containsThenInsertIfNew a b).fst

theorem Std.DHashMap.Internal.Raw.getThenInsertIfNew?_snd_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} : (m.getThenInsertIfNew? a b).snd = (Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).snd.val

theorem Std.DHashMap.Internal.Raw.getThenInsertIfNew?_snd_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} {b : β a} : (m.val.getThenInsertIfNew? a b).snd = (m.getThenInsertIfNew? a b).snd.val

theorem Std.DHashMap.Internal.Raw.getThenInsertIfNew?_fst_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} : (m.getThenInsertIfNew? a b).fst = (Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).fst

theorem Std.DHashMap.Internal.Raw.getThenInsertIfNew?_fst_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} {b : β a} : (m.val.getThenInsertIfNew? a b).fst = (m.getThenInsertIfNew? a b).fst

theorem Std.DHashMap.Internal.Raw.get?_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α} : m.get? a = Raw₀.get? ⟨m, ⋯⟩ a

theorem Std.DHashMap.Internal.Raw.get?_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} : m.val.get? a = m.get? a

theorem Std.DHashMap.Internal.Raw.contains_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} : m.contains a = Raw₀.contains ⟨m, ⋯⟩ a

theorem Std.DHashMap.Internal.Raw.contains_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} : m.val.contains a = m.contains a

theorem Std.DHashMap.Internal.Raw.get_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {a : α} {h : a ∈ m} : m.get a h = Raw₀.get ⟨m, ⋯⟩ a ⋯

theorem Std.DHashMap.Internal.Raw.get_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} {h : a ∈ m.val} : m.val.get a h = m.get a ⋯

theorem Std.DHashMap.Internal.Raw.getD_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α} {fallback : β a} : m.getD a fallback = Raw₀.getD ⟨m, ⋯⟩ a fallback

theorem Std.DHashMap.Internal.Raw.getD_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} {fallback : β a} : m.val.getD a fallback = m.getD a fallback

theorem Std.DHashMap.Internal.Raw.get!_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α} [Inhabited (β a)] : m.get! a = Raw₀.get! ⟨m, ⋯⟩ a

theorem Std.DHashMap.Internal.Raw.get!_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} [Inhabited (β a)] : m.val.get! a = m.get! a

theorem Std.DHashMap.Internal.Raw.getKey?_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} : m.getKey? a = Raw₀.getKey? ⟨m, ⋯⟩ a

theorem Std.DHashMap.Internal.Raw.getKey?_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} : m.val.getKey? a = m.getKey? a

theorem Std.DHashMap.Internal.Raw.getKey_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} {a : α} {h : a ∈ m} : m.getKey a h = Raw₀.getKey ⟨m, ⋯⟩ a ⋯

theorem Std.DHashMap.Internal.Raw.getKey_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {h : a ∈ m.val} : m.val.getKey a h = m.getKey a ⋯

theorem Std.DHashMap.Internal.Raw.getKeyD_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a fallback : α} : m.getKeyD a fallback = Raw₀.getKeyD ⟨m, ⋯⟩ a fallback

theorem Std.DHashMap.Internal.Raw.getKeyD_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {a fallback : α} : m.val.getKeyD a fallback = m.getKeyD a fallback

theorem Std.DHashMap.Internal.Raw.getKey!_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [Inhabited α] {m : Raw α β} (h : m.WF) {a : α} : m.getKey! a = Raw₀.getKey! ⟨m, ⋯⟩ a

theorem Std.DHashMap.Internal.Raw.getKey!_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [Inhabited α] {m : Raw₀ α β} {a : α} : m.val.getKey! a = m.getKey! a

theorem Std.DHashMap.Internal.Raw.erase_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} : m.erase a = (Raw₀.erase ⟨m, ⋯⟩ a).val

theorem Std.DHashMap.Internal.Raw.erase_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} : m.val.erase a = (m.erase a).val

theorem Std.DHashMap.Internal.Raw.filterMap_eq {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → Option (δ a)} : Raw.filterMap f m = (Raw₀.filterMap f ⟨m, ⋯⟩).val

theorem Std.DHashMap.Internal.Raw.filterMap_val {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} : Raw.filterMap f m.val = (Raw₀.filterMap f m).val

theorem Std.DHashMap.Internal.Raw.map_eq {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → δ a} : Raw.map f m = (Raw₀.map f ⟨m, ⋯⟩).val

theorem Std.DHashMap.Internal.Raw.map_val {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw₀ α β} {f : (a : α) → β a → δ a} : Raw.map f m.val = (Raw₀.map f m).val

theorem Std.DHashMap.Internal.Raw.filter_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → Bool} : Raw.filter f m = (Raw₀.filter f ⟨m, ⋯⟩).val

theorem Std.DHashMap.Internal.Raw.filter_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {f : (a : α) → β a → Bool} : Raw.filter f m.val = (Raw₀.filter f m).val

theorem Std.DHashMap.Internal.Raw.insertMany_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {l : ρ} : m.insertMany l = (Raw₀.insertMany ⟨m, ⋯⟩ l).val.val

theorem Std.DHashMap.Internal.Raw.insertMany_val {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {l : ρ} : m.val.insertMany l = (m.insertMany l).val.val

theorem Std.DHashMap.Internal.Raw.ofList_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {l : List ((a : α) × β a)} : Raw.ofList l = (Raw₀.empty.insertMany l).val.val

theorem Std.DHashMap.Internal.Raw.alter_eq {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.WF) {k : α} {f : Option (β k) → Option (β k)} : m.alter k f = (Raw₀.alter ⟨m, ⋯⟩ k f).val

theorem Std.DHashMap.Internal.Raw.modify_eq {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.WF) {k : α} {f : β k → β k} : m.modify k f = (Raw₀.modify ⟨m, ⋯⟩ k f).val

theorem Std.DHashMap.Internal.Raw.Const.insertMany_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {ρ : Type w} [ForIn Id ρ (α × β)] {l : ρ} : Raw.Const.insertMany m l = (Raw₀.Const.insertMany ⟨m, ⋯⟩ l).val.val

theorem Std.DHashMap.Internal.Raw.Const.insertMany_val {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw₀ α fun (x : α) => β} {ρ : Type w} [ForIn Id ρ (α × β)] {l : ρ} : Raw.Const.insertMany m.val l = (Raw₀.Const.insertMany m l).val.val

theorem Std.DHashMap.Internal.Raw.Const.ofList_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {l : List (α × β)} : Raw.Const.ofList l = (Raw₀.Const.insertMany Raw₀.empty l).val.val

theorem Std.DHashMap.Internal.Raw.Const.insertManyIfNewUnit_eq {α : Type u} {ρ : Type w} [ForIn Id ρ α] [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} {l : ρ} (h : m.WF) : Raw.Const.insertManyIfNewUnit m l = (Raw₀.Const.insertManyIfNewUnit ⟨m, ⋯⟩ l).val.val

theorem Std.DHashMap.Internal.Raw.Const.insertManyIfNewUnit_val {α : Type u} {ρ : Type w} [ForIn Id ρ α] [BEq α] [Hashable α] {m : Raw₀ α fun (x : α) => Unit} {l : ρ} : Raw.Const.insertManyIfNewUnit m.val l = (Raw₀.Const.insertManyIfNewUnit m l).val.val

theorem Std.DHashMap.Internal.Raw.Const.unitOfList_eq {α : Type u} [BEq α] [Hashable α] {l : List α} : Raw.Const.unitOfList l = (Raw₀.Const.insertManyIfNewUnit Raw₀.empty l).val.val

theorem Std.DHashMap.Internal.Raw.Const.get?_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {a : α} : Raw.Const.get? m a = Raw₀.Const.get? ⟨m, ⋯⟩ a

theorem Std.DHashMap.Internal.Raw.Const.get?_val {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw₀ α fun (x : α) => β} {a : α} : Raw.Const.get? m.val a = Raw₀.Const.get? m a

theorem Std.DHashMap.Internal.Raw.Const.get_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} {a : α} {h : a ∈ m} : Raw.Const.get m a h = Raw₀.Const.get ⟨m, ⋯⟩ a ⋯

theorem Std.DHashMap.Internal.Raw.Const.get_val {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw₀ α fun (x : α) => β} {a : α} {h : a ∈ m.val} : Raw.Const.get m.val a h = Raw₀.Const.get m a ⋯

theorem Std.DHashMap.Internal.Raw.Const.getD_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {a : α} {fallback : β} : Raw.Const.getD m a fallback = Raw₀.Const.getD ⟨m, ⋯⟩ a fallback

theorem Std.DHashMap.Internal.Raw.Const.getD_val {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw₀ α fun (x : α) => β} {a : α} {fallback : β} : Raw.Const.getD m.val a fallback = Raw₀.Const.getD m a fallback

theorem Std.DHashMap.Internal.Raw.Const.get!_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] {m : Raw α fun (x : α) => β} (h : m.WF) {a : α} : Raw.Const.get! m a = Raw₀.Const.get! ⟨m, ⋯⟩ a

theorem Std.DHashMap.Internal.Raw.Const.get!_val {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] {m : Raw₀ α fun (x : α) => β} {a : α} : Raw.Const.get! m.val a = Raw₀.Const.get! m a

theorem Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_snd_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {a : α} {b : β} : (Raw.Const.getThenInsertIfNew? m a b).snd = (Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).snd.val

theorem Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_snd_val {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw₀ α fun (x : α) => β} {a : α} {b : β} : (Raw.Const.getThenInsertIfNew? m.val a b).snd = (Raw₀.Const.getThenInsertIfNew? m a b).snd.val

theorem Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_fst_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {a : α} {b : β} : (Raw.Const.getThenInsertIfNew? m a b).fst = (Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).fst

theorem Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_fst_val {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Raw₀ α fun (x : α) => β} {a : α} {b : β} : (Raw.Const.getThenInsertIfNew? m.val a b).fst = (Raw₀.Const.getThenInsertIfNew? m a b).fst

theorem Std.DHashMap.Internal.Raw.Const.alter_eq {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {k : α} {f : Option β → Option β} : Raw.Const.alter m k f = (Raw₀.Const.alter ⟨m, ⋯⟩ k f).val

theorem Std.DHashMap.Internal.Raw.Const.modify_eq {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] {m : Raw α fun (x : α) => β} (h : m.WF) {k : α} {f : β → β} : Raw.Const.modify m k f = (Raw₀.Const.modify ⟨m, ⋯⟩ k f).val