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} {c : Nat} : Raw.emptyWithCapacity c = (Raw₀.emptyWithCapacity c).val

theorem Std.DHashMap.Internal.Raw.emptyc_eq {α : Type u} {β : α → Type v} : ∅ = Raw₀.emptyWithCapacity.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.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.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_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.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_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.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?_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.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.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.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.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.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.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_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.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.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.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.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.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.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.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.ofList_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {l : List ((a : α) × β a)} : Raw.ofList l = (Raw₀.emptyWithCapacity.insertMany l).val.val

theorem Std.DHashMap.Internal.Raw.ofArray_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {a : Array ((a : α) × β a)} : Raw.ofArray a = (Raw₀.emptyWithCapacity.insertMany a).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.union_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁.union m₂ = (Raw₀.union ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩).val

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

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

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

theorem Std.DHashMap.Internal.Raw.diff_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁.diff m₂ = (Raw₀.diff ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩).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.ofList_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {l : List (α × β)} : Raw.Const.ofList l = (Raw₀.Const.insertMany Raw₀.emptyWithCapacity l).val.val

theorem Std.DHashMap.Internal.Raw.Const.ofArray_eq {α : Type u} {β : Type v} [BEq α] [Hashable α] {a : Array (α × β)} : Raw.Const.ofArray a = (Raw₀.Const.insertMany Raw₀.emptyWithCapacity a).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.unitOfList_eq {α : Type u} [BEq α] [Hashable α] {l : List α} : Raw.Const.unitOfList l = (Raw₀.Const.insertManyIfNewUnit Raw₀.emptyWithCapacity l).val.val

theorem Std.DHashMap.Internal.Raw.Const.unitOfArray_eq {α : Type u} [BEq α] [Hashable α] {a : Array α} : Raw.Const.unitOfArray a = (Raw₀.Const.insertManyIfNewUnit Raw₀.emptyWithCapacity a).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_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.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.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.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?_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.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