Loogle!

Result

Found 352 declarations mentioning Option.getD. Of these, only the first 200 are shown.

• Option.getD 📋 Init.Prelude
  {α : Type u_1} (opt : Option α) (dflt : α) : α
• Option.getD_none 📋 Init.Data.Option.Basic
  {α✝ : Type u_1} {a : α✝} : none.getD a = a
• Option.getD_some 📋 Init.Data.Option.Basic
  {α✝ : Type u_1} {a b : α✝} : (some a).getD b = a
• 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.or_some' 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {a : α} {o : Option α} : o.or (some a) = some (o.getD a)
• 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.getLastD_eq_getLast? 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {l : List α} : l.getLastD a = l.getLast?.getD a
• List.headD_eq_head?_getD 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {l : List α} : l.headD a = l.head?.getD a
• List.tail_eq_tail? 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} : l.tail = l.tail?.getD []
• List.getLast!_eq_getLast?_getD 📋 Init.Data.List.Lemmas
  {α : Type u_1} [Inhabited α] {l : List α} : l.getLast! = l.getLast?.getD default
• List.tailD_eq_tail? 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l l' : List α} : l.tailD l' = l.tail?.getD l'
• List.getLast?_cons 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} {a : α} : (a :: l).getLast? = some (l.getLast?.getD a)
• 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.head?_concat 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} {a : α} : (l ++ [a]).head? = some (l.head?.getD a)
• 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
• Lean.Omega.IntList.get.eq_1 📋 Init.Omega.IntList
  (xs : Lean.Omega.IntList) (i : ℕ) : xs.get i = xs[i]?.getD 0
• Lean.Omega.IntList.add_def 📋 Init.Omega.IntList
  (xs ys : Lean.Omega.IntList) : xs + ys = List.zipWithAll (fun x y => x.getD 0 + y.getD 0) xs ys
• Lean.Omega.IntList.sub_def 📋 Init.Omega.IntList
  (xs ys : Lean.Omega.IntList) : xs - ys = List.zipWithAll (fun x y => x.getD 0 - y.getD 0) xs ys
• Lean.Omega.normalize.eq_1 📋 Init.Omega.Constraint
  (p : Lean.Omega.Constraint × Lean.Omega.Coeffs) : Lean.Omega.normalize p = (Lean.Omega.normalize? p).getD p
• Lean.Omega.positivize.eq_1 📋 Init.Omega.Constraint
  (p : Lean.Omega.Constraint × Lean.Omega.Coeffs) : Lean.Omega.positivize p = (Lean.Omega.positivize? p).getD p
• 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
• String.fromUTF8.loop.eq_def 📋 Init.Data.String.Extra
  (a : ByteArray) (i : ℕ) (acc : String) : String.fromUTF8.loop a i acc = if i < a.size then let c := (String.utf8DecodeChar? a i).getD default; String.fromUTF8.loop a (i + c.utf8Size) (acc.push c) else acc
• List.flatten_join_iff 📋 Init.Data.List.Sublist
  {α : Type u_1} {L : List (List α)} {l : List α} : L.flatten.Sublist l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : ℕ) (x : i < L.length), L[i].Sublist (L'[i]?.getD [])
• List.flatten_sublist_iff 📋 Init.Data.List.Sublist
  {α : Type u_1} {L : List (List α)} {l : List α} : L.flatten.Sublist l ↔ ∃ L', l = L'.flatten ∧ ∀ (i : ℕ) (x : i < L.length), L[i].Sublist (L'[i]?.getD [])
• List.sublist_flatten_iff 📋 Init.Data.List.Sublist
  {α : Type u_1} {L : List (List α)} {l : List α} : l.Sublist L.flatten ↔ ∃ L', l = L'.flatten ∧ ∀ (i : ℕ) (x : i < L'.length), L'[i].Sublist (L[i]?.getD [])
• List.sublist_join_iff 📋 Init.Data.List.Sublist
  {α : Type u_1} {L : List (List α)} {l : List α} : l.Sublist L.flatten ↔ ∃ L', l = L'.flatten ∧ ∀ (i : ℕ) (x : i < L'.length), L'[i].Sublist (L[i]?.getD [])
• List.countP_filterMap 📋 Init.Data.List.Count
  {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → Option β} {l : List α} : List.countP p (List.filterMap f l) = List.countP (fun a => (Option.map p (f a)).getD false) l
• 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.findIdx?_flatten 📋 Init.Data.List.Find
  {α : Type u_1} {l : List (List α)} {p : α → Bool} : List.findIdx? p l.flatten = Option.map (fun i => (List.map List.length (List.take i l)).sum + (Option.map (fun xs => List.findIdx p xs) l[i]?).getD 0) (List.findIdx? (fun x => x.any p) l)
• List.findIdx?_join 📋 Init.Data.List.Find
  {α : Type u_1} {l : List (List α)} {p : α → Bool} : List.findIdx? p l.flatten = Option.map (fun i => (List.map List.length (List.take i l)).sum + (Option.map (fun xs => List.findIdx p xs) l[i]?).getD 0) (List.findIdx? (fun x => x.any p) l)
• List.getLast_take 📋 Init.Data.List.Nat.TakeDrop
  {α : Type u_1} {i : ℕ} {l : List α} (h : List.take i l ≠ []) : (List.take i l).getLast h = l[i - 1]?.getD (l.getLast ⋯)
• List.modify_eq_set 📋 Init.Data.List.Nat.Modify
  {α : Type u_1} [Inhabited α] (f : α → α) (i : ℕ) (l : List α) : l.modify i f = l.set i (f (l[i]?.getD default))
• List.modifyHead_eq_set 📋 Init.Data.List.Nat.Modify
  {α : Type u_1} [Inhabited α] (f : α → α) (l : List α) : List.modifyHead f l = l.set 0 (f (l[0]?.getD default))
• List.foldl_max 📋 Init.Data.List.MinMax
  {α : Type u_1} [Max α] [Std.IdempotentOp max] [Std.Associative max] {l : List α} {a : α} : List.foldl max a l = a ⊔ l.max?.getD a
• List.foldl_min 📋 Init.Data.List.MinMax
  {α : Type u_1} [Min α] [Std.IdempotentOp min] [Std.Associative min] {l : List α} {a : α} : List.foldl min a l = a ⊓ l.min?.getD a
• 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
• Array.findIdx.eq_1 📋 Init.Data.List.ToArray
  {α : Type u} (p : α → Bool) (as : Array α) : Array.findIdx p as = (Array.findIdx? p as).getD as.size
• 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.back!_eq_back? 📋 Init.Data.Array.Lemmas
  {α : Type u_1} [Inhabited α] {xs : Array α} : xs.back! = xs.back?.getD default
• Array.back_eq_back? 📋 Init.Data.Array.Lemmas
  {α : Type u_1} [Inhabited α] {xs : Array α} : xs.back! = xs.back?.getD 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.get!_eq_get? 📋 Init.Data.Array.Lemmas
  {α : Type u_1} [Inhabited α] (xs : Array α) (i : ℕ) : xs.get! i = xs[i]?.getD 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.get!_eq_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
• Array.countP_filterMap 📋 Init.Data.Array.Count
  {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → Option β} {xs : Array α} : Array.countP p (Array.filterMap f xs) = Array.countP (fun a => (Option.map p (f a)).getD false) xs
• 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
• Array.back!_filterMap 📋 Init.Data.Array.Find
  {β : Type u_1} {α : Type u_2} [Inhabited β] {f : α → Option β} {xs : Array α} : (Array.filterMap f xs).back! = (Array.findSomeRev? f xs).getD default
• Array.findIdx?_flatten 📋 Init.Data.Array.Find
  {α : Type u_1} {xss : Array (Array α)} {p : α → Bool} : Array.findIdx? p xss.flatten = Option.map (fun i => (Array.map Array.size (xss.take i)).sum + (Option.map (fun xs => Array.findIdx p xs) xss[i]?).getD 0) (Array.findIdx? (fun x => x.any p) xss)
• 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
• Std.Internal.List.minKeyD.eq_1 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] (xs : List ((a : α) × β a)) (fallback : α) : Std.Internal.List.minKeyD xs fallback = (Std.Internal.List.minKey? xs).getD fallback
• Std.Internal.List.getValueD_eq_getValue? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} : Std.Internal.List.getValueD a l fallback = (Std.Internal.List.getValue? a l).getD fallback
• Std.Internal.List.getValueD.eq_1 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] (a : α) (l : List ((_ : α) × β)) (fallback : β) : Std.Internal.List.getValueD a l fallback = (Std.Internal.List.getValue? a l).getD fallback
• Std.Internal.List.getKeyD_eq_getKey? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {a fallback : α} : Std.Internal.List.getKeyD a l fallback = (Std.Internal.List.getKey? a l).getD 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.Internal.List.getValueCastD_eq_getValueCast? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {fallback : β a} : Std.Internal.List.getValueCastD a l fallback = (Std.Internal.List.getValueCast? a l).getD fallback
• Std.Internal.List.Const.getValueD_modifyKey_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {fallback : β} {f : β → β} (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueD k (Std.Internal.List.Const.modifyKey k f l) fallback = (Option.map f (Std.Internal.List.getValue? k l)).getD fallback
• Std.Internal.List.getValueCastD_modifyKey_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k} (l : List ((a : α) × β a)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueCastD k (Std.Internal.List.modifyKey k f l) fallback = (Option.map f (Std.Internal.List.getValueCast? k l)).getD fallback
• Std.Internal.List.getKeyD_filter_key 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)} {k fallback : α} (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getKeyD k (List.filter (fun p => f p.fst) l) fallback = (Option.filter f (Std.Internal.List.getKey? k l)).getD fallback
• Std.Internal.List.Const.getValueD_alterKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} [BEq α] {β : Type v} [EquivBEq α] {k k' : α} {fallback : β} {f : Option β → Option β} (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueD k' (Std.Internal.List.Const.alterKey k f l) fallback = if (k == k') = true then (f (Std.Internal.List.getValue? k l)).getD fallback else Std.Internal.List.getValueD k' l fallback
• Std.Internal.List.Const.getValueD_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {fallback : β} {f : β → β} (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueD k' (Std.Internal.List.Const.modifyKey k f l) fallback = if (k == k') = true then (Option.map f (Std.Internal.List.getValue? k l)).getD fallback else Std.Internal.List.getValueD k' l fallback
• Std.Internal.List.getValueCastD_filter 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : Std.Internal.List.DistinctKeys l) {fallback : β k} : Std.Internal.List.getValueCastD k (List.filter (fun p => f p.fst p.snd) l) fallback = (Option.filter (f k) (Std.Internal.List.getValueCast? k l)).getD fallback
• Std.Internal.List.Const.getValueD_filter_of_getKey?_eq_some 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {fallback : β} {f : α → β → Bool} {l : List ((_ : α) × β)} (distinct : Std.Internal.List.DistinctKeys l) {k k' : α} (h : Std.Internal.List.getKey? k l = some k') : Std.Internal.List.getValueD k (List.filter (fun p => f p.fst p.snd) l) fallback = (Option.filter (fun x => f k' x) (Std.Internal.List.getValue? k l)).getD fallback
• Std.Internal.List.Const.getValueD_map_of_getKey?_eq_some 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {f : α → β → γ} {l : List ((_ : α) × β)} (hl : Std.Internal.List.DistinctKeys l) {k k' : α} {fallback : γ} (h : Std.Internal.List.getKey? k l = some k') : Std.Internal.List.getValueD k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) fallback = (Option.map (f k') (Std.Internal.List.getValue? k l)).getD fallback
• Std.Internal.List.Const.getKeyD_filter 📋 Std.Data.Internal.List.Associative
  {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} {k fallback : α} (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getKeyD k (List.filter (fun p => f p.fst p.snd) l) fallback = ((Std.Internal.List.getKey? k l).pfilter fun x h => f x (Std.Internal.List.getValue x l ⋯)).getD fallback
• Std.Internal.List.getValueCastD_map 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → γ a} {l : List ((a : α) × β a)} {k : α} (hl : Std.Internal.List.DistinctKeys l) {fallback : γ k} : Std.Internal.List.getValueCastD k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) fallback = (Option.map (f k) (Std.Internal.List.getValueCast? k l)).getD fallback
• Std.Internal.List.Const.getValueD_filterMap_of_getKey?_eq_some 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {f : α → β → Option γ} {l : List ((_ : α) × β)} (distinct : Std.Internal.List.DistinctKeys l) {k k' : α} {fallback : γ} : Std.Internal.List.getKey? k l = some k' → Std.Internal.List.getValueD k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) fallback = ((Std.Internal.List.getValue? k l).bind fun x => f k' x).getD fallback
• Std.Internal.List.Const.getValueD_filter 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {fallback : β} {f : α → β → Bool} {l : List ((_ : α) × β)} (distinct : Std.Internal.List.DistinctKeys l) {k : α} : Std.Internal.List.getValueD k (List.filter (fun p => f p.fst p.snd) l) fallback = ((Std.Internal.List.getValue? k l).pfilter fun v h => f (Std.Internal.List.getKey k l ⋯) v).getD fallback
• Std.Internal.List.getValueCastD_filterMap 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : Std.Internal.List.DistinctKeys l) {fallback : γ k} : Std.Internal.List.getValueCastD k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) fallback = ((Std.Internal.List.getValueCast? k l).bind (f k)).getD fallback
• Std.Internal.List.Const.getKeyD_filterMap 📋 Std.Data.Internal.List.Associative
  {α : Type u} [BEq α] [EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ} {l : List ((_ : α) × β)} {k fallback : α} (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getKeyD k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) fallback = ((Std.Internal.List.getKey? k l).pfilter fun x h => (f x (Std.Internal.List.getValue x l ⋯)).isSome).getD fallback
• Std.Internal.List.getValueCastD_alterKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueCastD k' (Std.Internal.List.alterKey k f l) fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (f (Std.Internal.List.getValueCast? k l))).getD fallback else Std.Internal.List.getValueCastD k' l fallback
• Std.Internal.List.getValueCastD_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k} (l : List ((a : α) × β a)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueCastD k' (Std.Internal.List.modifyKey k f l) fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (Std.Internal.List.getValueCast? k l))).getD fallback else Std.Internal.List.getValueCastD k' l fallback
• Std.Internal.List.getKeyD_filter 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k fallback : α} (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getKeyD k (List.filter (fun p => f p.fst p.snd) l) fallback = ((Std.Internal.List.getKey? k l).pfilter fun x h => f x (Std.Internal.List.getValueCast x l ⋯)).getD fallback
• Std.Internal.List.Const.getValueD_filterMap 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {fallback : γ} {f : α → β → Option γ} {l : List ((_ : α) × β)} (distinct : Std.Internal.List.DistinctKeys l) {k : α} : Std.Internal.List.getValueD k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) fallback = ((Std.Internal.List.getValue? k l).pbind fun v h => f (Std.Internal.List.getKey k l ⋯) v).getD fallback
• Std.Internal.List.Const.getValueD_map 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {fallback : γ} {f : α → β → γ} {l : List ((_ : α) × β)} (hl : Std.Internal.List.DistinctKeys l) {k : α} : Std.Internal.List.getValueD k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) fallback = (Option.pmap (fun v h => f (Std.Internal.List.getKey k l h) v) (Std.Internal.List.getValue? k l) ⋯).getD fallback
• Std.Internal.List.getKeyD_filterMap 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k fallback : α} (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getKeyD k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) fallback = ((Std.Internal.List.getKey? k l).pfilter fun x h => (f x (Std.Internal.List.getValueCast x l ⋯)).isSome).getD fallback
• Std.Internal.List.getKeyD.eq_1 📋 Std.Data.DHashMap.Internal.AssocList.Lemmas
  {α : Type u} {β : α → Type v} [BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α) : Std.Internal.List.getKeyD a l fallback = (Std.Internal.List.getKey? a l).getD fallback
• Std.Internal.List.getValueCastD.eq_1 📋 Std.Data.DHashMap.Internal.AssocList.Lemmas
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (a : α) (l : List ((a : α) × β a)) (fallback : β a) : Std.Internal.List.getValueCastD a l fallback = (Std.Internal.List.getValueCast? a l).getD fallback
• Std.DHashMap.Internal.Raw₀.getKeyDₘ.eq_1 📋 Std.Data.DHashMap.Internal.Model
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a fallback : α) : m.getKeyDₘ a fallback = (m.getKey?ₘ a).getD 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_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₀.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_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₀.getKeyD_filter_key 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k fallback : α} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.filter (fun k x => f k) m).getKeyD k fallback = (Option.filter f (m.getKey? k)).getD 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₀.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.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_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₀.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₀.getKeyD_filter 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {f : (a : α) → β a → Bool} {k fallback : α} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => f x (m.get x ⋯)).getD fallback
• Std.DHashMap.Internal.Raw₀.Const.getKeyD_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₀.filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => f x (Std.DHashMap.Internal.Raw₀.Const.get m x ⋯)).getD fallback
• Std.DHashMap.Internal.Raw₀.getKeyD_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 : α} (h : (↑m).WF) : (Std.DHashMap.Internal.Raw₀.filterMap f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => (f x (m.get x ⋯)).isSome).getD fallback
• Std.DHashMap.Internal.Raw₀.Const.getKeyD_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₀.filterMap f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => (f x (Std.DHashMap.Internal.Raw₀.Const.get m x ⋯)).isSome).getD 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_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_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.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.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.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.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.getKeyD_filter_key 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k fallback : α} : (Std.DHashMap.filter (fun k x => f k) m).getKeyD k fallback = (Option.filter f (m.getKey? k)).getD 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_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.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.getKeyD_filter 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {f : (a : α) → β a → Bool} {k fallback : α} : (Std.DHashMap.filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => f x (m.get x ⋯)).getD fallback
• Std.DHashMap.Const.getKeyD_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.filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => f x (Std.DHashMap.Const.get m x ⋯)).getD fallback
• Std.DHashMap.Const.getKeyD_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.filterMap f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => (f x (Std.DHashMap.Const.get m x ⋯)).isSome).getD fallback
• Std.DHashMap.getKeyD_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 : α} : (Std.DHashMap.filterMap f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => (f x (m.get x ⋯)).isSome).getD 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.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_map 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ} : Std.DHashMap.Const.getD (Std.DHashMap.map f m) k fallback = (Option.pmap (fun v h => f (m.getKey k h) v) (Std.DHashMap.Const.get? m k) ⋯).getD fallback
• Std.HashMap.getKeyD_eq_getD_getKey? 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.getKeyD a fallback = (m.getKey? a).getD fallback
• Std.HashMap.getKeyD_filter_key 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k fallback : α} : (Std.HashMap.filter (fun k x => f k) m).getKeyD k fallback = (Option.filter f (m.getKey? k)).getD fallback
• Std.HashMap.getD_eq_getD_getElem? 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : m.getD a fallback = m[a]?.getD fallback
• Std.HashMap.getD_alter_self 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : Option β → Option β} : (m.alter k f).getD k fallback = (f m[k]?).getD fallback
• Std.HashMap.getD_modify_self 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} : (m.modify k f).getD k fallback = (Option.map f m[k]?).getD fallback
• Std.HashMap.getD_filter_of_getKey?_eq_some 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β} : m.getKey? k = some k' → (Std.HashMap.filter f m).getD k fallback = (Option.filter (fun x => f k' x) m[k]?).getD fallback
• Std.HashMap.getD_filterMap_of_getKey?_eq_some 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k k' : α} {fallback : γ} (h : m.getKey? k = some k') : (Std.HashMap.filterMap f m).getD k fallback = (m[k]?.bind (f k')).getD fallback
• Std.HashMap.getD_map_of_getKey?_eq_some 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ} (h : m.getKey? k = some k') : (Std.HashMap.map f m).getD k fallback = (Option.map (f k') m[k]?).getD fallback
• Std.HashMap.getD_alter 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β} : (m.alter k f).getD k' fallback = if (k == k') = true then (f m[k]?).getD fallback else m.getD k' fallback
• Std.HashMap.getD_modify 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} : (m.modify k f).getD k' fallback = if (k == k') = true then (Option.map f m[k]?).getD fallback else m.getD k' fallback
• Std.HashMap.getKeyD_filter 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k fallback : α} : (Std.HashMap.filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => f x m[x]).getD fallback
• Std.HashMap.getKeyD_filterMap 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k fallback : α} : (Std.HashMap.filterMap f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x h' => (f x m[x]).isSome).getD fallback
• Std.HashMap.getD_filter 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β} : (Std.HashMap.filter f m).getD k fallback = (m[k]?.pfilter fun x h' => f (m.getKey k ⋯) x).getD fallback
• Std.HashMap.getD_filterMap 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} {fallback : γ} : (Std.HashMap.filterMap f m).getD k fallback = (m[k]?.pbind fun x h' => f (m.getKey k ⋯) x).getD fallback
• Std.HashMap.getD_map 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ} : (Std.HashMap.map f m).getD k fallback = (Option.pmap (fun v h => f (m.getKey k h) v) m[k]? ⋯).getD fallback
• Std.HashSet.getD_eq_getD_get? 📋 Std.Data.HashSet.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.getD a fallback = (m.get? a).getD fallback
• Std.HashSet.getD_filter 📋 Std.Data.HashSet.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k fallback : α} : (Std.HashSet.filter f m).getD k fallback = (Option.filter f (m.get? k)).getD fallback
• Std.DTreeMap.Internal.Impl.maxKeyD_eq_getD_maxKey? 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] {l : Std.DTreeMap.Internal.Impl α β} {fallback : α} : l.maxKeyD fallback = l.maxKey?.getD fallback
• Std.DTreeMap.Internal.Impl.minKeyD_eq_getD_minKey? 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] {l : Std.DTreeMap.Internal.Impl α β} {fallback : α} : l.minKeyD fallback = l.minKey?.getD fallback
• Std.DTreeMap.Internal.Impl.getKeyDₘ.eq_1 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β) (fallback : α) : Std.DTreeMap.Internal.Impl.getKeyDₘ k l fallback = (l.getKey?ₘ k).getD fallback
• Std.DTreeMap.Internal.Impl.Const.getDₘ.eq_1 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : Type v} [Ord α] (l : Std.DTreeMap.Internal.Impl α fun x => β) (k : α) (fallback : β) : Std.DTreeMap.Internal.Impl.Const.getDₘ l k fallback = (Std.DTreeMap.Internal.Impl.Const.get?ₘ l k).getD fallback
• Std.DTreeMap.Internal.Impl.getDₘ.eq_1 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] [Std.OrientedOrd α] [Std.LawfulEqOrd α] (k : α) (l : Std.DTreeMap.Internal.Impl α β) (fallback : β k) : Std.DTreeMap.Internal.Impl.getDₘ k l fallback = (l.get?ₘ k).getD fallback
• Std.DTreeMap.Internal.Impl.getKeyD_eq_getD_getKey? 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF) {a fallback : α} : t.getKeyD a fallback = (t.getKey? a).getD fallback
• Std.DTreeMap.Internal.Impl.Const.getD_eq_getD_get? 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF) {a : α} {fallback : β} : Std.DTreeMap.Internal.Impl.Const.getD t a fallback = (Std.DTreeMap.Internal.Impl.Const.get? t a).getD fallback
• Std.DTreeMap.Internal.Impl.getD_eq_getD_get? 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {a : α} {fallback : β a} : t.getD a fallback = (t.get? a).getD fallback
• Std.DTreeMap.Internal.Impl.Const.getD_alter!_self 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF) {k : α} {fallback : β} {f : Option β → Option β} : Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.alter! k f t) k fallback = (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
• Std.DTreeMap.Internal.Impl.Const.getD_modify_self 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} (h : t.WF) {k : α} {fallback : β} {f : β → β} : Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.modify k f t) k fallback = (Option.map f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
• Std.DTreeMap.Internal.Impl.getD_alter!_self 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {k : α} {fallback : β k} {f : Option (β k) → Option (β k)} : (Std.DTreeMap.Internal.Impl.alter! k f t).getD k fallback = (f (t.get? k)).getD fallback
• Std.DTreeMap.Internal.Impl.getD_modify_self 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {k : α} {fallback : β k} {f : β k → β k} : (Std.DTreeMap.Internal.Impl.modify k f t).getD k fallback = (Option.map f (t.get? k)).getD fallback
• Std.DTreeMap.Internal.Impl.Const.getD_alter! 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF) {k k' : α} {fallback : β} {f : Option β → Option β} : Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.alter! k f t) k' fallback = if compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback else Std.DTreeMap.Internal.Impl.Const.getD t k' fallback
• Std.DTreeMap.Internal.Impl.Const.getD_modify 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} (h : t.WF) {k k' : α} {fallback : β} {f : β → β} : Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.modify k f t) k' fallback = if compare k k' = Ordering.eq then (Option.map f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback else Std.DTreeMap.Internal.Impl.Const.getD t k' fallback
• Std.DTreeMap.Internal.Impl.Const.getD_alter_self 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF) {k : α} {fallback : β} {f : Option β → Option β} : Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl k fallback = (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
• Std.DTreeMap.Internal.Impl.getD_alter_self 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {k : α} {fallback : β k} {f : Option (β k) → Option (β k)} : (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getD k fallback = (f (t.get? k)).getD fallback
• Std.DTreeMap.Internal.Impl.Const.getD_alter 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF) {k k' : α} {fallback : β} {f : Option β → Option β} : Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl k' fallback = if compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback else Std.DTreeMap.Internal.Impl.Const.getD t k' fallback
• Std.DTreeMap.Internal.Impl.getD_alter! 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} : (Std.DTreeMap.Internal.Impl.alter! k f t).getD k' fallback = if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).getD fallback else t.getD k' fallback
• Std.DTreeMap.Internal.Impl.getD_modify 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {fallback : β k'} {f : β k → β k} : (Std.DTreeMap.Internal.Impl.modify k f t).getD k' fallback = if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).getD fallback else t.getD k' fallback
• Std.DTreeMap.Internal.Impl.Const.getD_insertMany!_list 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α} (fallback : β) : Std.DTreeMap.Internal.Impl.Const.getD (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k fallback = (List.findSomeRev? (fun x => match x with | (a, b) => if compare a k = Ordering.eq then some b else none) l).getD (Std.DTreeMap.Internal.Impl.Const.getD t k fallback)
• Std.DTreeMap.Internal.Impl.Const.get!_insertMany!_list 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited β] (h : t.WF) {l : List (α × β)} {k : α} : Std.DTreeMap.Internal.Impl.Const.get! (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k = (List.findSomeRev? (fun x => match x with | (a, b) => if compare a k = Ordering.eq then some b else none) l).getD (Std.DTreeMap.Internal.Impl.Const.get! t k)
• Std.DTreeMap.Internal.Impl.getD_alter 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} : (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getD k' fallback = if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).getD fallback else t.getD k' fallback
• Std.DTreeMap.Internal.Impl.Const.getD_insertMany_list 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α} (fallback : β) : Std.DTreeMap.Internal.Impl.Const.getD (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k fallback = (List.findSomeRev? (fun x => match x with | (a, b) => if compare a k = Ordering.eq then some b else none) l).getD (Std.DTreeMap.Internal.Impl.Const.getD t k fallback)
• Std.DTreeMap.Internal.Impl.Const.get!_insertMany_list 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited β] (h : t.WF) {l : List (α × β)} {k : α} : Std.DTreeMap.Internal.Impl.Const.get! (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k = (List.findSomeRev? (fun x => match x with | (a, b) => if compare a k = Ordering.eq then some b else none) l).getD (Std.DTreeMap.Internal.Impl.Const.get! t k)
• Std.DTreeMap.getKeyD_eq_getD_getKey? 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α} : t.getKeyD a fallback = (t.getKey? a).getD fallback
• Std.DTreeMap.Const.getD_eq_getD_get? 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α} {fallback : β} : Std.DTreeMap.Const.getD t a fallback = (Std.DTreeMap.Const.get? t a).getD fallback
• Std.DTreeMap.getD_eq_getD_get? 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a : α} {fallback : β a} : t.getD a fallback = (t.get? a).getD fallback
• Std.DTreeMap.Const.getD_alter_self 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α} {fallback : β} {f : Option β → Option β} : Std.DTreeMap.Const.getD (Std.DTreeMap.Const.alter t k f) k fallback = (f (Std.DTreeMap.Const.get? t k)).getD fallback
• Std.DTreeMap.Const.getD_modify_self 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k : α} {fallback : β} {f : β → β} : Std.DTreeMap.Const.getD (Std.DTreeMap.Const.modify t k f) k fallback = (Option.map f (Std.DTreeMap.Const.get? t k)).getD fallback
• Std.DTreeMap.getD_alter_self 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {k : α} {fallback : β k} {f : Option (β k) → Option (β k)} : (t.alter k f).getD k fallback = (f (t.get? k)).getD fallback
• Std.DTreeMap.getD_modify_self 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {k : α} {fallback : β k} {f : β k → β k} : (t.modify k f).getD k fallback = (Option.map f (t.get? k)).getD fallback
• Std.DTreeMap.Const.getD_alter 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α} {fallback : β} {f : Option β → Option β} : Std.DTreeMap.Const.getD (Std.DTreeMap.Const.alter t k f) k' fallback = if cmp k k' = Ordering.eq then (f (Std.DTreeMap.Const.get? t k)).getD fallback else Std.DTreeMap.Const.getD t k' fallback
• Std.DTreeMap.Const.getD_modify 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k k' : α} {fallback : β} {f : β → β} : Std.DTreeMap.Const.getD (Std.DTreeMap.Const.modify t k f) k' fallback = if cmp k k' = Ordering.eq then (Option.map f (Std.DTreeMap.Const.get? t k)).getD fallback else Std.DTreeMap.Const.getD t k' fallback
• Std.DTreeMap.getD_alter 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} : (t.alter k f).getD k' fallback = if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).getD fallback else t.getD k' fallback

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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 ?a

   If 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 ?b

4. By 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 find tsum_lt_tsum even though the hypothesis f i < g i is 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 bce1d65