Loogle!
Result
Found 908 declarations whose name contains "getD". Of these, only the first 200 are shown.
- Option.getD 📋 Init.Prelude
{α : Type u_1} (opt : Option α) (dflt : α) : α - Array.getD 📋 Init.Prelude
{α : Type u_1} (a : Array α) (i : ℕ) (v₀ : α) : α - Option.getD_none 📋 Init.Data.Option.Basic
{α✝ : Type u_1} {a : α✝} : none.getD a = a - Option.getDM 📋 Init.Data.Option.Basic
{m : Type u_1 → Type u_2} {α : Type u_1} [Pure m] (x : Option α) (y : m α) : m α - Option.getD_some 📋 Init.Data.Option.Basic
{α✝ : Type u_1} {a b : α✝} : (some a).getD b = a - Subarray.getD 📋 Init.Data.Array.Subarray
{α : Type u_1} (s : Subarray α) (i : ℕ) (v₀ : α) : α - Lean.TSyntax.getDocString 📋 Init.Meta
(stx : Lean.TSyntax `Lean.Parser.Command.docComment) : String - Option.get!_eq_getD 📋 Init.Data.Option.Lemmas
{α : Type u_1} [Inhabited α] (o : Option α) : o.get! = o.getD default - Option.get!_eq_getD_default 📋 Init.Data.Option.Lemmas
{α : Type u_1} [Inhabited α] (o : Option α) : o.get! = o.getD default - Option.getD_of_ne_none 📋 Init.Data.Option.Lemmas
{α : Type u_1} {x : Option α} (hx : x ≠ none) (y : α) : some (x.getD y) = x - Option.get_eq_getD 📋 Init.Data.Option.Lemmas
{α : Type u_1} {fallback : α} (o : Option α) {h : o.isSome = true} : o.get h = o.getD fallback - Option.getD_or 📋 Init.Data.Option.Lemmas
{α : Type u_1} {o o' : Option α} {fallback : α} : (o.or o').getD fallback = o.getD (o'.getD fallback) - Option.getD_map 📋 Init.Data.Option.Lemmas
{α : Type u_1} {β : Type u_2} (f : α → β) (x : α) (o : Option α) : (Option.map f o).getD (f x) = f (o.getD x) - Option.getD_eq_iff 📋 Init.Data.Option.Lemmas
{α : Type u_1} {o : Option α} {a b : α} : o.getD a = b ↔ o = some b ∨ o = none ∧ a = b - List.getD 📋 Init.Data.List.BasicAux
{α : Type u_1} (as : List α) (i : ℕ) (fallback : α) : α - List.getD_nil 📋 Init.Data.List.BasicAux
{n : ℕ} {α✝ : Type u_1} {d : α✝} : [].getD n d = d - List.headD_eq_head?_getD 📋 Init.Data.List.Lemmas
{α : Type u_1} {a : α} {l : List α} : l.headD a = l.head?.getD a - List.getLast!_eq_getLast?_getD 📋 Init.Data.List.Lemmas
{α : Type u_1} [Inhabited α] {l : List α} : l.getLast! = l.getLast?.getD default - List.get!_eq_getD 📋 Init.Data.List.Lemmas
{α : Type u_1} [Inhabited α] (l : List α) (i : ℕ) : l.get! i = l.getD i default - List.getD_cons_zero 📋 Init.Data.List.Lemmas
{α✝ : Type u_1} {x : α✝} {xs : List α✝} {d : α✝} : (x :: xs).getD 0 d = x - List.getD_cons_succ 📋 Init.Data.List.Lemmas
{α✝ : Type u_1} {x : α✝} {xs : List α✝} {n : ℕ} {d : α✝} : (x :: xs).getD (n + 1) d = xs.getD n d - List.getD_eq_getElem?_getD 📋 Init.Data.List.Lemmas
{α : Type u_1} {l : List α} {i : ℕ} {a : α} : l.getD i a = l[i]?.getD a - List.getD.eq_1 📋 Init.Data.List.Lemmas
{α : Type u_1} (as : List α) (i : ℕ) (fallback : α) : as.getD i fallback = as[i]?.getD fallback - List.getElem!_eq_getElem?_getD 📋 Init.Data.List.Lemmas
{α : Type u_1} [Inhabited α] {l : List α} {i : ℕ} : l[i]! = l[i]?.getD default - List.getD_getElem? 📋 Init.Data.List.Lemmas
{α : Type u_1} {l : List α} {i : ℕ} {d : α} : l[i]?.getD d = if p : i < l.length then l[i] else d - BitVec.getMsbD_eq_getMsb?_getD 📋 Init.Data.BitVec.Lemmas
{w : ℕ} (x : BitVec w) (i : ℕ) : x.getMsbD i = (x.getMsb? i).getD false - BitVec.getLsbD_eq_getElem?_getD 📋 Init.Data.BitVec.Lemmas
{w : ℕ} {x : BitVec w} {i : ℕ} : x.getLsbD i = x[i]?.getD false - List.findIdx_eq_getD_findIdx? 📋 Init.Data.List.Find
{α : Type u_1} {xs : List α} {p : α → Bool} : List.findIdx p xs = (List.findIdx? p xs).getD xs.length - List.le_max?_getD_of_mem 📋 Init.Data.List.Nat.Basic
{l : List ℕ} {a k : ℕ} (h : a ∈ l) : a ≤ l.max?.getD k - List.le_maximum?_getD_of_mem 📋 Init.Data.List.Nat.Basic
{l : List ℕ} {a k : ℕ} (h : a ∈ l) : a ≤ l.max?.getD k - List.min?_getD_le_of_mem 📋 Init.Data.List.Nat.Basic
{l : List ℕ} {a k : ℕ} (h : a ∈ l) : l.min?.getD k ≤ a - List.minimum?_getD_le_of_mem 📋 Init.Data.List.Nat.Basic
{l : List ℕ} {a k : ℕ} (h : a ∈ l) : l.min?.getD k ≤ a - Option.getD.eq_2 📋 Init.Data.Array.Lemmas
{α : Type u_1} (dflt : α) : none.getD dflt = dflt - Option.getD.eq_1 📋 Init.Data.Array.Lemmas
{α : Type u_1} (dflt x : α) : (some x).getD dflt = x - Array.get!_eq_getD 📋 Init.Data.Array.Lemmas
{α : Type u_1} {n : ℕ} [Inhabited α] (xs : Array α) : xs.get! n = xs.getD n default - Array.getD_eq_get? 📋 Init.Data.Array.Lemmas
{α : Type u_1} {xs : Array α} {i : ℕ} {d : α} : xs.getD i d = xs[i]?.getD d - Array.getD_eq_getD_getElem? 📋 Init.Data.Array.Lemmas
{α : Type u_1} {xs : Array α} {i : ℕ} {d : α} : xs.getD i d = xs[i]?.getD d - Array.getElem!_eq_getD 📋 Init.Data.Array.Lemmas
{α : Type u_1} [Inhabited α] {xs : Array α} {i : ℕ} : xs[i]! = xs.getD i default - Array.get!_eq_getD_getElem? 📋 Init.Data.Array.Lemmas
{α : Type u_1} [Inhabited α] (xs : Array α) (i : ℕ) : xs.get! i = xs[i]?.getD default - Array.getD_get?_setIfInBounds 📋 Init.Data.Array.Lemmas
{α : Type u_1} {xs : Array α} {i : ℕ} {v d : α} : (xs.setIfInBounds i v)[i]?.getD d = if i < xs.size then v else d - Array.getD_getElem?_setIfInBounds 📋 Init.Data.Array.Lemmas
{α : Type u_1} {xs : Array α} {i : ℕ} {v d : α} : (xs.setIfInBounds i v)[i]?.getD d = if i < xs.size then v else d - Array.getD_setD 📋 Init.Data.Array.Lemmas
{α : Type u_1} {xs : Array α} {i : ℕ} {v d : α} : (xs.setIfInBounds i v)[i]?.getD d = if i < xs.size then v else d - Array.getD_get? 📋 Init.Data.Array.Lemmas
{α : Type u_1} {xs : Array α} {i : ℕ} {d : α} : xs[i]?.getD d = if p : i < xs.size then xs[i] else d - Array.getD_getElem? 📋 Init.Data.Array.Lemmas
{α : Type u_1} {xs : Array α} {i : ℕ} {d : α} : xs[i]?.getD d = if p : i < xs.size then xs[i] else d - Vector.getD 📋 Init.Data.Vector.Basic
{α : Type u_1} {n : ℕ} (xs : Vector α n) (i : ℕ) (default : α) : α - Array.findIdx_eq_getD_findIdx? 📋 Init.Data.Array.Find
{α : Type u_1} {xs : Array α} {p : α → Bool} : Array.findIdx p xs = (Array.findIdx? p xs).getD xs.size - Vector.getD_getElem? 📋 Init.Data.Vector.Lemmas
{α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {d : α} : xs[i]?.getD d = if p : i < n then xs[i] else d - Lean.Order.Option.monotone_getDM 📋 Init.Internal.Order.Lemmas
{m : Type u → Type v} [Monad m] [(α : Type u) → Lean.Order.PartialOrder (m α)] {α : Type u} {γ : Type w} [Lean.Order.PartialOrder γ] (o : Option α) (y : γ → m α) (hmono : Lean.Order.monotone y) : Lean.Order.monotone fun x => o.getDM (y x) - Std.DHashMap.Internal.AssocList.getD 📋 Std.Data.DHashMap.Internal.AssocList.Basic
{α : Type u} {β : Type v} [BEq α] (a : α) (fallback : β) : (Std.DHashMap.Internal.AssocList α fun x => β) → β - Std.DHashMap.Internal.Raw₀.Const.getD 📋 Std.Data.DHashMap.Internal.Defs
{α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α) (fallback : β) : β - Std.DHashMap.Internal.Raw₀.getD 📋 Std.Data.DHashMap.Internal.Defs
{α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : β a) : β a - Std.DHashMap.Raw.Const.getD 📋 Std.Data.DHashMap.Raw
{α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α fun x => β) (a : α) (fallback : β) : β - Std.DHashMap.Raw.getD 📋 Std.Data.DHashMap.Raw
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] (m : Std.DHashMap.Raw α β) (a : α) (fallback : β a) : β a - Std.DHashMap.Const.getD 📋 Std.Data.DHashMap.Basic
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (m : Std.DHashMap α fun x => β) (a : α) (fallback : β) : β - Std.DHashMap.getD 📋 Std.Data.DHashMap.Basic
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.DHashMap α β) (a : α) (fallback : β a) : β a - Std.DHashMap.Internal.Raw.Const.getD_eq 📋 Std.Data.DHashMap.Internal.Raw
{α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α fun x => β} (h : m.WF) {a : α} {fallback : β} : Std.DHashMap.Raw.Const.getD m a fallback = Std.DHashMap.Internal.Raw₀.Const.getD ⟨m, ⋯⟩ a fallback - Std.DHashMap.Internal.Raw.getD_eq 📋 Std.Data.DHashMap.Internal.Raw
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α} {fallback : β a} : m.getD a fallback = Std.DHashMap.Internal.Raw₀.getD ⟨m, ⋯⟩ a fallback - Std.DHashMap.Raw.getD.eq_1 📋 Std.Data.DHashMap.Internal.Raw
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] (m : Std.DHashMap.Raw α β) (a : α) (fallback : β a) : m.getD a fallback = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.getD ⟨m, h⟩ a fallback else fallback - Std.DHashMap.Raw.Const.getD.eq_1 📋 Std.Data.DHashMap.Internal.Raw
{α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α fun x => β) (a : α) (fallback : β) : Std.DHashMap.Raw.Const.getD m a fallback = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.Const.getD ⟨m, h⟩ a fallback else fallback - Std.Internal.List.maxKeyD_eq_getD_maxKey? 📋 Std.Data.Internal.List.Associative
{α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} : Std.Internal.List.maxKeyD l fallback = (Std.Internal.List.maxKey? l).getD fallback - Std.Internal.List.minKeyD_eq_getD_minKey? 📋 Std.Data.Internal.List.Associative
{α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback : α} : Std.Internal.List.minKeyD l fallback = (Std.Internal.List.minKey? l).getD fallback - Std.DHashMap.Internal.AssocList.getD.eq_1 📋 Std.Data.DHashMap.Internal.AssocList.Lemmas
{α : Type u} {β : Type v} [BEq α] (a : α) (fallback : β) : Std.DHashMap.Internal.AssocList.getD a fallback Std.DHashMap.Internal.AssocList.nil = fallback - Std.DHashMap.Internal.AssocList.getD_eq 📋 Std.Data.DHashMap.Internal.AssocList.Lemmas
{α : Type u} {β : Type v} [BEq α] {l : Std.DHashMap.Internal.AssocList α fun x => β} {a : α} {fallback : β} : Std.DHashMap.Internal.AssocList.getD a fallback l = Std.Internal.List.getValueD a l.toList fallback - Std.DHashMap.Internal.AssocList.getD.eq_2 📋 Std.Data.DHashMap.Internal.AssocList.Lemmas
{α : Type u} {β : Type v} [BEq α] (a : α) (fallback : β) (k : α) (v : β) (es : Std.DHashMap.Internal.AssocList α fun x => β) : Std.DHashMap.Internal.AssocList.getD a fallback (Std.DHashMap.Internal.AssocList.cons k v es) = bif k == a then v else Std.DHashMap.Internal.AssocList.getD a fallback es - Std.DHashMap.Internal.Raw₀.Const.getDₘ 📋 Std.Data.DHashMap.Internal.Model
{α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α) (fallback : β) : β - Std.DHashMap.Internal.Raw₀.getDₘ 📋 Std.Data.DHashMap.Internal.Model
{α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : β a) : β a - Std.DHashMap.Internal.Raw₀.Const.getD_eq_getDₘ 📋 Std.Data.DHashMap.Internal.Model
{α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α) (fallback : β) : Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = Std.DHashMap.Internal.Raw₀.Const.getDₘ m a fallback - Std.DHashMap.Internal.Raw₀.Const.getDₘ.eq_1 📋 Std.Data.DHashMap.Internal.Model
{α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α) (fallback : β) : Std.DHashMap.Internal.Raw₀.Const.getDₘ m a fallback = (Std.DHashMap.Internal.Raw₀.Const.get?ₘ m a).getD fallback - Std.DHashMap.Internal.Raw₀.getD_eq_getDₘ 📋 Std.Data.DHashMap.Internal.Model
{α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : β a) : m.getD a fallback = m.getDₘ a fallback - Std.DHashMap.Internal.Raw₀.getDₘ.eq_1 📋 Std.Data.DHashMap.Internal.Model
{α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : β a) : m.getDₘ a fallback = (m.get?ₘ a).getD fallback - Std.DHashMap.Internal.Raw₀.getD.eq_1 📋 Std.Data.DHashMap.Internal.Model
{α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] (a : α) (fallback : β a) (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size) : Std.DHashMap.Internal.Raw₀.getD ⟨{ size := size, buckets := buckets }, hm⟩ a fallback = Std.DHashMap.Internal.AssocList.getCastD a fallback buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))] - Std.DHashMap.Internal.Raw₀.Const.getD.eq_1 📋 Std.Data.DHashMap.Internal.Model
{α : Type u} {β : Type v} [BEq α] [Hashable α] (a : α) (fallback : β) (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size) : Std.DHashMap.Internal.Raw₀.Const.getD ⟨{ size := size, buckets := buckets }, hm⟩ a fallback = Std.DHashMap.Internal.AssocList.getD a fallback buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))] - Std.DHashMap.Internal.Raw₀.getD_eq_getValueCastD 📋 Std.Data.DHashMap.Internal.WF
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α} {fallback : β a} : m.getD a fallback = Std.Internal.List.getValueCastD a (Std.DHashMap.Internal.toListModel (↑m).buckets) fallback - Std.DHashMap.Internal.Raw₀.getDₘ_eq_getValueCastD 📋 Std.Data.DHashMap.Internal.WF
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α} {fallback : β a} : m.getDₘ a fallback = Std.Internal.List.getValueCastD a (Std.DHashMap.Internal.toListModel (↑m).buckets) fallback - Std.DHashMap.Internal.Raw₀.Const.getD_eq_getValueD 📋 Std.Data.DHashMap.Internal.WF
{α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α fun x => β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α} {fallback : β} : Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = Std.Internal.List.getValueD a (Std.DHashMap.Internal.toListModel (↑m).buckets) fallback - Std.DHashMap.Internal.Raw₀.Const.getDₘ_eq_getValueD 📋 Std.Data.DHashMap.Internal.WF
{α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α fun x => β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α} {fallback : β} : Std.DHashMap.Internal.Raw₀.Const.getDₘ m a fallback = Std.Internal.List.getValueD a (Std.DHashMap.Internal.toListModel (↑m).buckets) fallback - Std.DHashMap.Internal.Raw₀.Const.getD_empty 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} {a : α} {fallback : β} {c : ℕ} : Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c) a fallback = fallback - Std.DHashMap.Internal.Raw₀.Const.getD_emptyWithCapacity 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {a : α} {fallback : β} {c : ℕ} : Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c) a fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_empty 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u_1} {β : α → Type u_2} [BEq α] [Hashable α] [LawfulBEq α] {a : α} {fallback : β a} {c : ℕ} : (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).getD a fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_emptyWithCapacity 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {a : α} {fallback : β a} {c : ℕ} : (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).getD a fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_erase_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k : α} {fallback : β k} : (m.erase k).getD k fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_insert_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback b : β a} : (m.insert a b).getD a fallback = b - Std.DHashMap.Internal.Raw₀.getD_eq_fallback 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β a} : m.contains a = false → m.getD a fallback = fallback - Std.DHashMap.Internal.Raw₀.getKeyD_eq_getD_getKey? 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {a fallback : α} : m.getKeyD a fallback = (m.getKey? a).getD fallback - Std.DHashMap.Internal.Raw₀.getD_eq_getD_get? 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β a} : m.getD a fallback = (m.get? a).getD fallback - Std.DHashMap.Internal.Raw₀.Const.getD_eq_getD 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β} : Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = m.getD a fallback - Std.DHashMap.Internal.Raw₀.get!_eq_getD_default 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} [Inhabited (β a)] : m.get! a = m.getD a default - Std.DHashMap.Internal.Raw₀.Const.getD_erase_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {k : α} {fallback : β} : Std.DHashMap.Internal.Raw₀.Const.getD (m.erase k) k fallback = fallback - Std.DHashMap.Internal.Raw₀.Const.getD_eq_getD_get? 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {a : α} {fallback : β} : Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = (Std.DHashMap.Internal.Raw₀.Const.get? m a).getD fallback - Std.DHashMap.Internal.Raw₀.Const.getD_insert_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {k : α} {fallback v : β} : Std.DHashMap.Internal.Raw₀.Const.getD (m.insert k v) k fallback = v - Std.DHashMap.Internal.Raw₀.Const.get!_eq_getD_default 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : (↑m).WF) {a : α} : Std.DHashMap.Internal.Raw₀.Const.get! m a = Std.DHashMap.Internal.Raw₀.Const.getD m a default - Std.DHashMap.Internal.Raw₀.Const.getD_eq_fallback 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {a : α} {fallback : β} : m.contains a = false → Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = fallback - Std.DHashMap.Internal.Raw₀.get_eq_getD 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β a} {h✝ : m.contains a = true} : m.get a h✝ = m.getD a fallback - Std.DHashMap.Internal.Raw₀.get?_eq_some_getD 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β a} : m.contains a = true → m.get? a = some (m.getD a fallback) - Std.DHashMap.Internal.Raw₀.Const.getD_congr 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {a b : α} {fallback : β} (hab : (a == b) = true) : Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = Std.DHashMap.Internal.Raw₀.Const.getD m b fallback - Std.DHashMap.Internal.Raw₀.getD_filter 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {f : (a : α) → β a → Bool} {k : α} {fallback : β k} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.filter f m).getD k fallback = (Option.filter (f k) (m.get? k)).getD fallback - Std.DHashMap.Internal.Raw₀.Const.getD_insertManyIfNewUnit_list 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {l : List α} {k : α} {fallback : Unit} : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)) k fallback = () - Std.DHashMap.Internal.Raw₀.Const.get_eq_getD 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {a : α} {fallback : β} {h✝ : m.contains a = true} : Std.DHashMap.Internal.Raw₀.Const.get m a h✝ = Std.DHashMap.Internal.Raw₀.Const.getD m a fallback - Std.DHashMap.Internal.Raw₀.getD_alter_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {k : α} {fallback : β k} (h : (↑m).WF) {f : Option (β k) → Option (β k)} : (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback - Std.DHashMap.Internal.Raw₀.Const.get?_eq_some_getD 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {a : α} {fallback : β} : m.contains a = true → Std.DHashMap.Internal.Raw₀.Const.get? m a = some (Std.DHashMap.Internal.Raw₀.Const.getD m a fallback) - Std.DHashMap.Internal.Raw₀.Const.getD_alter_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {k : α} {fallback : β} (h : (↑m).WF) {f : Option β → Option β} : Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.Const.alter m k f) k fallback = (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback - Std.DHashMap.Internal.Raw₀.Const.getD_modify_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (h : (↑m).WF) {k : α} {fallback : β} {f : β → β} : Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.Const.modify m k f) k fallback = (Option.map f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback - Std.DHashMap.Internal.Raw₀.getD_modify_self 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k : α} {fallback : β k} {f : β k → β k} : (m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback - Std.DHashMap.Internal.Raw₀.getD_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.map f m).getD k fallback = (Option.map (f k) (m.get? k)).getD fallback - Std.DHashMap.Internal.Raw₀.getD_of_isEmpty 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {a : α} {fallback : β a} : (↑m).isEmpty = true → m.getD a fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_filterMap 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {γ : α → Type w} [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.filterMap f m).getD k fallback = ((m.get? k).bind (f k)).getD fallback - Std.DHashMap.Internal.Raw₀.getD_erase 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k a : α} {fallback : β a} : (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback - Std.DHashMap.Internal.Raw₀.Const.getD_insertManyIfNewUnit_emptyWithCapacity_list 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {l : List α} {k : α} {fallback : Unit} : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k fallback = () - Std.DHashMap.Internal.Raw₀.Const.getD_insertManyIfNewUnit_empty_list 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u_1} [BEq α] [Hashable α] {l : List α} {k : α} {fallback : Unit} : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k fallback = () - Std.DHashMap.Internal.Raw₀.Const.getD_erase 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {k a : α} {fallback : β} : Std.DHashMap.Internal.Raw₀.Const.getD (m.erase k) a fallback = if (k == a) = true then fallback else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback - Std.DHashMap.Internal.Raw₀.Const.getD_insert 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {k a : α} {fallback v : β} : Std.DHashMap.Internal.Raw₀.Const.getD (m.insert k v) a fallback = if (k == a) = true then v else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback - Std.DHashMap.Internal.Raw₀.Const.getD_of_isEmpty 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {a : α} {fallback : β} : (↑m).isEmpty = true → Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = fallback - Std.DHashMap.Internal.Raw₀.Const.getD_filter_of_getKey?_eq_some 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β} (h : (↑m).WF) : m.getKey? k = some k' → Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.filter f m) k fallback = (Option.filter (fun x => f k' x) (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback - Std.DHashMap.Internal.Raw₀.Const.getD_map_of_getKey?_eq_some 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k k' : α} {fallback : γ} (h : (↑m).WF) : m.getKey? k = some k' → Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.map f m) k fallback = (Option.map (f k') (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback - Std.DHashMap.Internal.Raw₀.Const.getD_filterMap_of_getKey?_eq_some 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k k' : α} {fallback : γ} (h : (↑m).WF) : m.getKey? k = some k' → Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.filterMap f m) k fallback = ((Std.DHashMap.Internal.Raw₀.Const.get? m k).bind fun x => f k' x).getD fallback - Std.DHashMap.Internal.Raw₀.Const.getD_alter 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {k k' : α} {fallback : β} (h : (↑m).WF) {f : Option β → Option β} : Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.Const.alter m k f) k' fallback = if (k == k') = true then (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback else Std.DHashMap.Internal.Raw₀.Const.getD m k' fallback - Std.DHashMap.Internal.Raw₀.Const.getD_modify 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (h : (↑m).WF) {k k' : α} {fallback : β} {f : β → β} : Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.Const.modify m k f) k' fallback = if (k == k') = true then (Option.map f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback else Std.DHashMap.Internal.Raw₀.Const.getD m k' fallback - Std.DHashMap.Internal.Raw₀.getD_insert 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k a : α} {fallback : β a} {v : β k} : (m.insert k v).getD a fallback = if h : (k == a) = true then cast ⋯ v else m.getD a fallback - Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k fallback = fallback - Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_empty_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k fallback = fallback - Std.DHashMap.Internal.Raw₀.Const.getD_insertIfNew 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {k a : α} {fallback v : β} : Std.DHashMap.Internal.Raw₀.Const.getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ m.contains k = false then v else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback - Std.DHashMap.Internal.Raw₀.Const.getD_filter 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β} (h : (↑m).WF) : Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.filter f m) k fallback = ((Std.DHashMap.Internal.Raw₀.Const.get? m k).pfilter fun x h' => f (m.getKey k ⋯) x).getD fallback - Std.DHashMap.Internal.Raw₀.getD_eq_of_equiv 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β) [LawfulBEq α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) (h : (↑m₁).Equiv ↑m₂) {k : α} {fallback : β k} : m₁.getD k fallback = m₂.getD k fallback - Std.DHashMap.Internal.Raw₀.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getD k fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_insertMany_empty_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u_1} {β : α → Type u_2} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getD k fallback = fallback - Std.DHashMap.Internal.Raw₀.getD_alter 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {k k' : α} {fallback : β k'} (h : (↑m).WF) {f : Option (β k) → Option (β k)} : (m.alter k f).getD k' fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).getD fallback else m.getD k' fallback - Std.DHashMap.Internal.Raw₀.Const.getD_filterMap 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} {fallback : γ} (h : (↑m).WF) : Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.filterMap f m) k fallback = ((Std.DHashMap.Internal.Raw₀.Const.get? m k).pbind fun x h' => f (m.getKey k ⋯) x).getD fallback - Std.DHashMap.Internal.Raw₀.getD_modify 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k k' : α} {fallback : β k'} {f : β k → β k} : (m.modify k f).getD k' fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).getD fallback else m.getD k' fallback - Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List (α × β)} {k : α} {fallback : β} (h' : (List.map Prod.fst l).contains k = false) : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k fallback = Std.DHashMap.Internal.Raw₀.Const.getD m k fallback - Std.DHashMap.Internal.Raw₀.Const.getD_eq_of_equiv 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) (h : (↑m₁).Equiv ↑m₂) {k : α} {fallback : β} : Std.DHashMap.Internal.Raw₀.Const.getD m₁ k fallback = Std.DHashMap.Internal.Raw₀.Const.getD m₂ k fallback - Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v fallback : β} (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l) (mem : (k, v) ∈ l) : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k' fallback = v - Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_empty_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u_1} [BEq α] [Hashable α] {β : Type u_2} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v fallback : β} (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l) (mem : (k, v) ∈ l) : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k' fallback = v - Std.DHashMap.Internal.Raw₀.getD_insertMany_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) : (↑(m.insertMany l)).getD k fallback = m.getD k fallback - Std.DHashMap.Internal.Raw₀.Const.getD_map 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ} (h : (↑m).WF) : Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.map f m) k fallback = (Option.pmap (fun v h => f (m.getKey k h) v) (Std.DHashMap.Internal.Raw₀.Const.get? m k) ⋯).getD fallback - Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v fallback : β} (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l) (mem : (k, v) ∈ l) : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k' fallback = v - Std.DHashMap.Internal.Raw₀.getD_insertIfNew 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k a : α} {fallback : β a} {v : β k} : (m.insertIfNew k v).getD a fallback = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.getD a fallback - Std.DHashMap.Internal.Raw₀.getD_insertMany_emptyWithCapacity_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getD k' fallback = cast ⋯ v - Std.DHashMap.Internal.Raw₀.getD_insertMany_empty_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u_1} {β : α → Type u_2} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getD k' fallback = cast ⋯ v - Std.DHashMap.Internal.Raw₀.getD_insertMany_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
{α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (↑(m.insertMany l)).getD k' fallback = cast ⋯ v - Std.DHashMap.Const.getD_unitOfList 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {l : List α} {k : α} {fallback : Unit} : Std.DHashMap.Const.getD (Std.DHashMap.Const.unitOfList l) k fallback = () - Std.DHashMap.Const.getD_emptyWithCapacity 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {a : α} {fallback : β} {c : ℕ} : Std.DHashMap.Const.getD (Std.DHashMap.emptyWithCapacity c) a fallback = fallback - Std.DHashMap.Const.getD_empty 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {a : α} {fallback : β} : Std.DHashMap.Const.getD ∅ a fallback = fallback - Std.DHashMap.Const.getD_emptyc 📋 Std.Data.DHashMap.Lemmas
{α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type u_2} {a : α} {fallback : β} : Std.DHashMap.Const.getD ∅ a fallback = fallback - Std.DHashMap.getD_emptyWithCapacity 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {a : α} {fallback : β a} {c : ℕ} : (Std.DHashMap.emptyWithCapacity c).getD a fallback = fallback - Std.DHashMap.getD_empty 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {a : α} {fallback : β a} : ∅.getD a fallback = fallback - Std.DHashMap.getD_emptyc 📋 Std.Data.DHashMap.Lemmas
{α : Type u_1} {β : α → Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {a : α} {fallback : β a} : ∅.getD a fallback = fallback - Std.DHashMap.getD_erase_self 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k : α} {fallback : β k} : (m.erase k).getD k fallback = fallback - Std.DHashMap.Const.getD_eq_getD 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α] {a : α} {fallback : β} : Std.DHashMap.Const.getD m a fallback = m.getD a fallback - Std.DHashMap.Const.getD_erase_self 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} : Std.DHashMap.Const.getD (m.erase k) k fallback = fallback - Std.DHashMap.getD_insert_self 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k : α} {fallback v : β k} : (m.insert k v).getD k fallback = v - Std.DHashMap.getD_of_isEmpty 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} : m.isEmpty = true → m.getD a fallback = fallback - Std.DHashMap.getD_eq_fallback_of_contains_eq_false 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} : m.contains a = false → m.getD a fallback = fallback - Std.DHashMap.getKeyD_eq_getD_getKey? 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.getKeyD a fallback = (m.getKey? a).getD fallback - Std.DHashMap.Const.getD_eq_getD_get? 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : Std.DHashMap.Const.getD m a fallback = (Std.DHashMap.Const.get? m a).getD fallback - Std.DHashMap.Const.getD_insert_self 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} : Std.DHashMap.Const.getD (m.insert k v) k fallback = v - Std.DHashMap.getD_eq_getD_get? 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} : m.getD a fallback = (m.get? a).getD fallback - Std.DHashMap.Const.get!_eq_getD_default 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : Std.DHashMap.Const.get! m a = Std.DHashMap.Const.getD m a default - Std.DHashMap.Const.getD_of_isEmpty 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : m.isEmpty = true → Std.DHashMap.Const.getD m a fallback = fallback - Std.DHashMap.get!_eq_getD_default 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] : m.get! a = m.getD a default - Std.DHashMap.Const.getD_eq_fallback_of_contains_eq_false 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : m.contains a = false → Std.DHashMap.Const.getD m a fallback = fallback - Std.DHashMap.getD_eq_fallback 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} : a ∉ m → m.getD a fallback = fallback - Std.DHashMap.Const.getD_congr 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β} (hab : (a == b) = true) : Std.DHashMap.Const.getD m a fallback = Std.DHashMap.Const.getD m b fallback - Std.DHashMap.Const.getD_insertManyIfNewUnit_list 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α fun x => Unit} {l : List α} {k : α} {fallback : Unit} : Std.DHashMap.Const.getD (Std.DHashMap.Const.insertManyIfNewUnit m l) k fallback = () - Std.DHashMap.Const.getD_eq_fallback 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : a ∉ m → Std.DHashMap.Const.getD m a fallback = fallback - Std.DHashMap.Const.getD_ofList_of_contains_eq_false 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) : Std.DHashMap.Const.getD (Std.DHashMap.Const.ofList l) k fallback = fallback - Std.DHashMap.Equiv.getD_eq 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : Std.DHashMap α β} [LawfulBEq α] {k : α} {fallback : β k} (h : m₁.Equiv m₂) : m₁.getD k fallback = m₂.getD k fallback - Std.DHashMap.get?_eq_some_getD_of_contains 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} : m.contains a = true → m.get? a = some (m.getD a fallback) - Std.DHashMap.Const.get?_eq_some_getD_of_contains 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : m.contains a = true → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.getD m a fallback) - Std.DHashMap.get_eq_getD 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} {h : a ∈ m} : m.get a h = m.getD a fallback - Std.DHashMap.Const.getD_alter_self 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : Option β → Option β} : Std.DHashMap.Const.getD (Std.DHashMap.Const.alter m k f) k fallback = (f (Std.DHashMap.Const.get? m k)).getD fallback - Std.DHashMap.Equiv.constGetD_eq 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} (h : m₁.Equiv m₂) : Std.DHashMap.Const.getD m₁ k fallback = Std.DHashMap.Const.getD m₂ k fallback - Std.DHashMap.Const.getD_modify_self 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} : Std.DHashMap.Const.getD (Std.DHashMap.Const.modify m k f) k fallback = (Option.map f (Std.DHashMap.Const.get? m k)).getD fallback - Std.DHashMap.Const.get_eq_getD 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} {h : a ∈ m} : Std.DHashMap.Const.get m a h = Std.DHashMap.Const.getD m a fallback - Std.DHashMap.get?_eq_some_getD 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} : a ∈ m → m.get? a = some (m.getD a fallback) - Std.DHashMap.getD_alter_self 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k : α} {fallback : β k} {f : Option (β k) → Option (β k)} : (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback - Std.DHashMap.getD_filter 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {f : (a : α) → β a → Bool} {k : α} {fallback : β k} : (Std.DHashMap.filter f m).getD k fallback = (Option.filter (f k) (m.get? k)).getD fallback - Std.DHashMap.getD_ofList_of_contains_eq_false 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) : (Std.DHashMap.ofList l).getD k fallback = fallback - Std.DHashMap.Const.get?_eq_some_getD 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : a ∈ m → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.getD m a fallback) - Std.DHashMap.getD_modify_self 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k} : (m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback - Std.DHashMap.getD_map 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k} : (Std.DHashMap.map f m).getD k fallback = (Option.map (f k) (m.get? k)).getD fallback - Std.DHashMap.getD_filterMap 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k} : (Std.DHashMap.filterMap f m).getD k fallback = ((m.get? k).bind (f k)).getD fallback - Std.DHashMap.getD_erase 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k a : α} {fallback : β a} : (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback - Std.DHashMap.Const.getD_erase 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} : Std.DHashMap.Const.getD (m.erase k) a fallback = if (k == a) = true then fallback else Std.DHashMap.Const.getD m a fallback - Std.DHashMap.Const.getD_insert 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : Std.DHashMap.Const.getD (m.insert k v) a fallback = if (k == a) = true then v else Std.DHashMap.Const.getD m a fallback - Std.DHashMap.Const.getD_filter_of_getKey?_eq_some 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β} : m.getKey? k = some k' → Std.DHashMap.Const.getD (Std.DHashMap.filter f m) k fallback = (Option.filter (fun x => f k' x) (Std.DHashMap.Const.get? m k)).getD fallback - Std.DHashMap.Const.getD_filterMap_of_getKey?_eq_some 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k k' : α} {fallback : γ} (h : m.getKey? k = some k') : Std.DHashMap.Const.getD (Std.DHashMap.filterMap f m) k fallback = ((Std.DHashMap.Const.get? m k).bind (f k')).getD fallback - Std.DHashMap.Const.getD_map_of_getKey?_eq_some 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ} (h : m.getKey? k = some k') : Std.DHashMap.Const.getD (Std.DHashMap.map f m) k fallback = (Option.map (f k') (Std.DHashMap.Const.get? m k)).getD fallback - Std.DHashMap.Const.getD_alter 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β} : Std.DHashMap.Const.getD (Std.DHashMap.Const.alter m k f) k' fallback = if (k == k') = true then (f (Std.DHashMap.Const.get? m k)).getD fallback else Std.DHashMap.Const.getD m k' fallback - Std.DHashMap.Const.getD_modify 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} : Std.DHashMap.Const.getD (Std.DHashMap.Const.modify m k f) k' fallback = if (k == k') = true then (Option.map f (Std.DHashMap.Const.get? m k)).getD fallback else Std.DHashMap.Const.getD m k' fallback - Std.DHashMap.Const.getD_ofList_of_mem 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v fallback : β} (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l) (mem : (k, v) ∈ l) : Std.DHashMap.Const.getD (Std.DHashMap.Const.ofList l) k' fallback = v - Std.DHashMap.Const.getD_insertMany_list_of_contains_eq_false 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) : Std.DHashMap.Const.getD (Std.DHashMap.Const.insertMany m l) k fallback = Std.DHashMap.Const.getD m k fallback - Std.DHashMap.getD_insert 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} : (m.insert k v).getD a fallback = if h : (k == a) = true then cast ⋯ v else m.getD a fallback - Std.DHashMap.getD_insertMany_list_of_contains_eq_false 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) : (m.insertMany l).getD k fallback = m.getD k fallback - Std.DHashMap.getD_alter 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} : (m.alter k f).getD k' fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).getD fallback else m.getD k' fallback - Std.DHashMap.Const.getD_filter 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β} : Std.DHashMap.Const.getD (Std.DHashMap.filter f m) k fallback = ((Std.DHashMap.Const.get? m k).pfilter fun x h' => f (m.getKey k ⋯) x).getD fallback - Std.DHashMap.Const.getD_insertMany_list_of_mem 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v fallback : β} (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l) (mem : (k, v) ∈ l) : Std.DHashMap.Const.getD (Std.DHashMap.Const.insertMany m l) k' fallback = v - Std.DHashMap.getD_modify 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k} : (m.modify k f).getD k' fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).getD fallback else m.getD k' fallback - Std.DHashMap.Const.getD_filterMap 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} {fallback : γ} : Std.DHashMap.Const.getD (Std.DHashMap.filterMap f m) k fallback = ((Std.DHashMap.Const.get? m k).pbind fun x h' => f (m.getKey k ⋯) x).getD fallback - Std.DHashMap.Const.getD_insertIfNew 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : Std.DHashMap.Const.getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ k ∉ m then v else Std.DHashMap.Const.getD m a fallback - Std.DHashMap.getD_ofList_of_mem 📋 Std.Data.DHashMap.Lemmas
{α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (Std.DHashMap.ofList l).getD k' fallback = cast ⋯ v
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision 19971e9 serving mathlib revision f167e8d