Loogle!

Result

Found 2075 declarations whose name contains "_def". Of these, only the first 200 are shown.

• sizeOf_default 📋 Init.SizeOf
  {α : Sort u_1} (n : α) : sizeOf n = 0
• id_def 📋 Init.Core
  {α : Sort u} (a : α) : id a = a
• iff_def 📋 Init.Core
  {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (b → a)
• iff_def' 📋 Init.Core
  {a b : Prop} : (a ↔ b) ↔ (b → a) ∧ (a → b)
• Function.comp_def 📋 Init.Core
  {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} (f : β → δ) (g : α → β) : f ∘ g = fun x => f (g x)
• Prod.lexLt_def 📋 Init.Core
  {α : Type u_1} {β : Type u_2} [LT α] [LT β] (s t : α × β) : s.lexLt t = (s.1 < t.1 ∨ s.1 = t.1 ∧ s.2 < t.2)
• Nat.max_def 📋 Init.Data.Nat.Basic
  {n m : ℕ} : max n m = if n ≤ m then m else n
• Nat.min_def 📋 Init.Data.Nat.Basic
  {n m : ℕ} : min n m = if n ≤ m then n else m
• Prod.lex_def 📋 Init.WF
  {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} {p q : α × β} : Prod.Lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2
• Nat.mod_def 📋 Init.Data.Nat.Div.Basic
  (m k : ℕ) : m % k = m - k * (m / k)
• Fin.neg_def 📋 Init.Data.Fin.Basic
  {n : ℕ} (a : Fin n) : -a = ⟨(n - ↑a) % n, ⋯⟩
• outOfBounds_eq_default 📋 Init.GetElem
  {α : Sort u_1} [Inhabited α] : outOfBounds = default
• LawfulGetElem.getElem!_def 📋 Init.GetElem
  {cont : Type u} {idx : Type v} {elem : outParam (Type w)} {dom : outParam (cont → idx → Prop)} {ge : GetElem? cont idx elem dom} [self : LawfulGetElem cont idx elem dom] [Inhabited elem] (c : cont) (i : idx) : c[i]! = match c[i]? with | some e => e | none => default
• LawfulGetElem.getElem?_def 📋 Init.GetElem
  {cont : Type u} {idx : Type v} {elem : outParam (Type w)} {dom : outParam (cont → idx → Prop)} {ge : GetElem? cont idx elem dom} [self : LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = if h : dom c i then some c[i] else none
• Array.mem_def 📋 Init.Data.Array.Basic
  {α : Type u} {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList
• Nat.log2_def 📋 Init.Data.Nat.Log2
  (n : ℕ) : n.log2 = if 2 ≤ n then (n / 2).log2 + 1 else 0
• Int.add_def 📋 Init.Data.Int.Lemmas
  {a b : ℤ} : a.add b = a + b
• Int.mul_def 📋 Init.Data.Int.Lemmas
  {a b : ℤ} : a.mul b = a * b
• Int.nonneg_def 📋 Init.Data.Int.Order
  {a : ℤ} : a.NonNeg ↔ ∃ n, a = ↑n
• Int.le_def 📋 Init.Data.Int.Order
  {a b : ℤ} : a ≤ b ↔ (b - a).NonNeg
• Int.max_def 📋 Init.Data.Int.Order
  (n m : ℤ) : max n m = if n ≤ m then m else n
• Int.min_def 📋 Init.Data.Int.Order
  (n m : ℤ) : min n m = if n ≤ m then n else m
• Int.div_def 📋 Init.Data.Int.DivMod.Bootstrap
  (a b : ℤ) : a / b = a.ediv b
• Int.dvd_def 📋 Init.Data.Int.DivMod.Bootstrap
  (a b : ℤ) : (a ∣ b) = ∃ c, b = a * c
• Int.emod_def 📋 Init.Data.Int.DivMod.Bootstrap
  (a b : ℤ) : a % b = a - b * (a / b)
• Int.bmod_def 📋 Init.Data.Int.DivMod.Bootstrap
  (x : ℤ) (m : ℕ) : x.bmod m = if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m
• Nat.gcd_def 📋 Init.Data.Nat.Gcd
  (x y : ℕ) : x.gcd y = if x = 0 then y else (y % x).gcd x
• Lean.Omega.IntList.neg_def 📋 Init.Omega.IntList
  (xs : Lean.Omega.IntList) : -xs = List.map (fun x => -x) xs
• Lean.Omega.IntList.smul_def 📋 Init.Omega.IntList
  (xs : Lean.Omega.IntList) (i : ℤ) : i * xs = List.map (fun x => i * x) xs
• Lean.Omega.IntList.mul_def 📋 Init.Omega.IntList
  (xs ys : Lean.Omega.IntList) : xs * ys = List.zipWith (fun x1 x2 => x1 * x2) xs ys
• 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
• Fin.le_def 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {a b : Fin n} : a ≤ b ↔ ↑a ≤ ↑b
• Fin.lt_def 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {a b : Fin n} : a < b ↔ ↑a < ↑b
• Fin.intCast_def 📋 Init.Data.Fin.Lemmas
  {n : ℕ} [NeZero n] (x : ℤ) : ↑x = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs
• Fin.add_def 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (a b : Fin n) : a + b = ⟨(↑a + ↑b) % n, ⋯⟩
• Fin.mul_def 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (a b : Fin n) : a * b = ⟨↑a * ↑b % n, ⋯⟩
• Fin.mod_def 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (a m : Fin n) : a % m = ⟨↑a % ↑m, ⋯⟩
• Fin.sub_def 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (a b : Fin n) : a - b = ⟨(n - ↑b + ↑a) % n, ⋯⟩
• Option.mem_def 📋 Init.Data.Option.Instances
  {α : Type u_1} {a : α} {b : Option α} : a ∈ b ↔ b = some a
• Option.choice_eq_default 📋 Init.Data.Option.Lemmas
  {α : Type u_1} [Subsingleton α] [Inhabited α] : Option.choice α = some default
• Option.pure_def 📋 Init.Data.Option.Lemmas
  {α : Type u_1} : pure = some
• Option.guard_def 📋 Init.Data.Option.Lemmas
  {α : Type u_1} (p : α → Bool) : Option.guard p = fun x => if p x = true then some x else none
• List.flatMap_def 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : List.flatMap f l = (List.map f l).flatten
• List.subset_def 📋 Init.Data.List.Sublist
  {α : Type u_1} {l₁ l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂
• Int.mod_def' 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℤ) : m % n = m.emod n
• Int.fmod_def 📋 Init.Data.Int.DivMod.Lemmas
  (a b : ℤ) : a.fmod b = a - b * a.fdiv b
• Int.tmod_def 📋 Init.Data.Int.DivMod.Lemmas
  (a b : ℤ) : a.tmod b = a - b * a.tdiv b
• BitVec.le_def 📋 Init.Data.BitVec.Lemmas
  {n : ℕ} {x y : BitVec n} : x ≤ y ↔ x.toNat ≤ y.toNat
• BitVec.lt_def 📋 Init.Data.BitVec.Lemmas
  {n : ℕ} {x y : BitVec n} : x < y ↔ x.toNat < y.toNat
• BitVec.not_def 📋 Init.Data.BitVec.Lemmas
  {v : ℕ} {x : BitVec v} : ~~~x = BitVec.allOnes v ^^^ x
• BitVec.add_def 📋 Init.Data.BitVec.Lemmas
  {n : ℕ} (x y : BitVec n) : x + y = BitVec.ofNat n (x.toNat + y.toNat)
• BitVec.udiv_def 📋 Init.Data.BitVec.Lemmas
  {n : ℕ} {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat)
• BitVec.umod_def 📋 Init.Data.BitVec.Lemmas
  {n : ℕ} {x y : BitVec n} : x % y = BitVec.ofNat n (x.toNat % y.toNat)
• BitVec.sub_def 📋 Init.Data.BitVec.Lemmas
  {n : ℕ} (x y : BitVec n) : x - y = BitVec.ofNat n (2 ^ n - y.toNat + x.toNat)
• BitVec.rotateLeft_def 📋 Init.Data.BitVec.Lemmas
  {w : ℕ} {x : BitVec w} {r : ℕ} : x.rotateLeft r = x <<< (r % w) ||| x >>> (w - r % w)
• BitVec.rotateRight_def 📋 Init.Data.BitVec.Lemmas
  {w : ℕ} {x : BitVec w} {r : ℕ} : x.rotateRight r = x >>> (r % w) ||| x <<< (w - r % w)
• BitVec.append_def 📋 Init.Data.BitVec.Lemmas
  {v w : ℕ} (x : BitVec v) (y : BitVec w) : x ++ y = x.shiftLeftZeroExtend w ||| BitVec.setWidth' ⋯ y
• BitVec.mul_def 📋 Init.Data.BitVec.Lemmas
  {n : ℕ} {x y : BitVec n} : x * y = { toFin := x.toFin * y.toFin }
• USize.one_def 📋 Init.Data.UInt.Lemmas
  : 1 = { toBitVec := 1 }
• USize.zero_def 📋 Init.Data.UInt.Lemmas
  : 0 = { toBitVec := 0 }
• UInt16.one_def 📋 Init.Data.UInt.Lemmas
  : 1 = { toBitVec := 1 }
• UInt16.zero_def 📋 Init.Data.UInt.Lemmas
  : 0 = { toBitVec := 0 }
• UInt32.one_def 📋 Init.Data.UInt.Lemmas
  : 1 = { toBitVec := 1 }
• UInt32.zero_def 📋 Init.Data.UInt.Lemmas
  : 0 = { toBitVec := 0 }
• UInt64.one_def 📋 Init.Data.UInt.Lemmas
  : 1 = { toBitVec := 1 }
• UInt64.zero_def 📋 Init.Data.UInt.Lemmas
  : 0 = { toBitVec := 0 }
• UInt8.one_def 📋 Init.Data.UInt.Lemmas
  : 1 = { toBitVec := 1 }
• UInt8.zero_def 📋 Init.Data.UInt.Lemmas
  : 0 = { toBitVec := 0 }
• USize.add_def 📋 Init.Data.UInt.Lemmas
  (a b : USize) : a + b = { toBitVec := a.toBitVec + b.toBitVec }
• USize.mod_def 📋 Init.Data.UInt.Lemmas
  (a b : USize) : a % b = { toBitVec := a.toBitVec % b.toBitVec }
• USize.mul_def 📋 Init.Data.UInt.Lemmas
  (a b : USize) : a * b = { toBitVec := a.toBitVec * b.toBitVec }
• USize.sub_def 📋 Init.Data.UInt.Lemmas
  (a b : USize) : a - b = { toBitVec := a.toBitVec - b.toBitVec }
• UInt16.add_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt16) : a + b = { toBitVec := a.toBitVec + b.toBitVec }
• UInt16.mod_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt16) : a % b = { toBitVec := a.toBitVec % b.toBitVec }
• UInt16.mul_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt16) : a * b = { toBitVec := a.toBitVec * b.toBitVec }
• UInt16.sub_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt16) : a - b = { toBitVec := a.toBitVec - b.toBitVec }
• UInt32.add_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt32) : a + b = { toBitVec := a.toBitVec + b.toBitVec }
• UInt32.mod_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt32) : a % b = { toBitVec := a.toBitVec % b.toBitVec }
• UInt32.mul_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt32) : a * b = { toBitVec := a.toBitVec * b.toBitVec }
• UInt32.sub_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt32) : a - b = { toBitVec := a.toBitVec - b.toBitVec }
• UInt64.add_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt64) : a + b = { toBitVec := a.toBitVec + b.toBitVec }
• UInt64.mod_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt64) : a % b = { toBitVec := a.toBitVec % b.toBitVec }
• UInt64.mul_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt64) : a * b = { toBitVec := a.toBitVec * b.toBitVec }
• UInt64.sub_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt64) : a - b = { toBitVec := a.toBitVec - b.toBitVec }
• UInt8.add_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt8) : a + b = { toBitVec := a.toBitVec + b.toBitVec }
• UInt8.mod_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt8) : a % b = { toBitVec := a.toBitVec % b.toBitVec }
• UInt8.mul_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt8) : a * b = { toBitVec := a.toBitVec * b.toBitVec }
• UInt8.sub_def 📋 Init.Data.UInt.Lemmas
  (a b : UInt8) : a - b = { toBitVec := a.toBitVec - b.toBitVec }
• Char.le_def 📋 Init.Data.Char.Lemmas
  {a b : Char} : a ≤ b ↔ a.val ≤ b.val
• Char.lt_def 📋 Init.Data.Char.Lemmas
  {a b : Char} : a < b ↔ a.val < b.val
• Array.swap_def 📋 Init.Data.List.ToArray
  {α : Type u_1} (xs : Array α) (i j : ℕ) (hi : i < xs.size) (hj : j < xs.size) : xs.swap i j hi hj = (xs.set i xs[j] hi).set j xs[i] ⋯
• Array.singleton_def 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {v : α} : Array.singleton v = #[v]
• Array.flatMap_def 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} : Array.flatMap f xs = (Array.map f xs).flatten
• Array.setIfInBounds_def 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (xs : Array α) (i : ℕ) (a : α) : xs.setIfInBounds i a = if h : i < xs.size then xs.set i a h else xs
• Array.swapAt!_def 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xs : Array α} {i : ℕ} {v : α} (h : i < xs.size) : xs.swapAt! i v = (xs[i], xs.set i v h)
• Array.swapAt_def 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xs : Array α} {i : ℕ} {v : α} (hi : i < xs.size) : xs.swapAt i v hi = (xs[i], xs.set i v hi)
• Array.swapIfInBounds_def 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xs : Array α} {i j : ℕ} : xs.swapIfInBounds i j = if h₁ : i < xs.size then if h₂ : j < xs.size then xs.swap i j h₁ h₂ else xs else xs
• Int.Linear.eq_def'_cert 📋 Init.Data.Int.Linear
  (x : Int.Linear.Var) (e : Int.Linear.Expr) (p : Int.Linear.Poly) : Bool
• Int.Linear.eq_def_cert 📋 Init.Data.Int.Linear
  (x : Int.Linear.Var) (xPoly p : Int.Linear.Poly) : Bool
• Int.Linear.eq_def'_norm_cert 📋 Init.Data.Int.Linear
  (x : Int.Linear.Var) (e : Int.Linear.Expr) (ePoly ePoly' p : Int.Linear.Poly) : Bool
• Int.Linear.eq_def 📋 Init.Data.Int.Linear
  (ctx : Int.Linear.Context) (x : Int.Linear.Var) (xPoly p : Int.Linear.Poly) : Int.Linear.eq_def_cert x xPoly p = true → Int.Linear.Var.denote ctx x = Int.Linear.Poly.denote' ctx xPoly → Int.Linear.Poly.denote' ctx p = 0
• Int.Linear.eq_def' 📋 Init.Data.Int.Linear
  (ctx : Int.Linear.Context) (x : Int.Linear.Var) (e : Int.Linear.Expr) (p : Int.Linear.Poly) : Int.Linear.eq_def'_cert x e p = true → Int.Linear.Var.denote ctx x = Int.Linear.Expr.denote ctx e → Int.Linear.Poly.denote' ctx p = 0
• Int.Linear.eq_def_norm 📋 Init.Data.Int.Linear
  (ctx : Int.Linear.Context) (x : Int.Linear.Var) (xPoly xPoly' p : Int.Linear.Poly) : Int.Linear.eq_def_cert x xPoly' p = true → Int.Linear.Var.denote ctx x = Int.Linear.Poly.denote' ctx xPoly → Int.Linear.Poly.denote' ctx xPoly = Int.Linear.Poly.denote' ctx xPoly' → Int.Linear.Poly.denote' ctx p = 0
• Int.Linear.eq_def'_norm 📋 Init.Data.Int.Linear
  (ctx : Int.Linear.Context) (x : Int.Linear.Var) (e : Int.Linear.Expr) (ePoly ePoly' p : Int.Linear.Poly) : Int.Linear.eq_def'_norm_cert x e ePoly ePoly' p = true → Int.Linear.Var.denote ctx x = Int.Linear.Expr.denote ctx e → Int.Linear.Poly.denote' ctx ePoly = Int.Linear.Poly.denote' ctx ePoly' → Int.Linear.Poly.denote' ctx p = 0
• Rat.inv_def 📋 Init.Data.Rat.Lemmas
  (a : ℚ) : a⁻¹ = Rat.divInt (↑a.den) a.num
• Rat.floor_def 📋 Init.Data.Rat.Lemmas
  (a : ℚ) : a.floor = a.num / ↑a.den
• Rat.max_def 📋 Init.Data.Rat.Lemmas
  {n m : ℚ} : max n m = if n ≤ m then m else n
• Rat.min_def 📋 Init.Data.Rat.Lemmas
  {n m : ℚ} : min n m = if n ≤ m then n else m
• Rat.div_def 📋 Init.Data.Rat.Lemmas
  (a b : ℚ) : a / b = a * b⁻¹
• Rat.ofScientific_true_def 📋 Init.Data.Rat.Lemmas
  {m e : ℕ} : Rat.ofScientific m true e = mkRat (↑m) (10 ^ e)
• Rat.ofScientific_false_def 📋 Init.Data.Rat.Lemmas
  {m e : ℕ} : Rat.ofScientific m false e = ↑(m * 10 ^ e)
• Rat.mul_def' 📋 Init.Data.Rat.Lemmas
  (a b : ℚ) : a * b = mkRat (a.num * b.num) (a.den * b.den)
• Rat.mul_def 📋 Init.Data.Rat.Lemmas
  (a b : ℚ) : a * b = Rat.normalize (a.num * b.num) (a.den * b.den) ⋯
• Rat.pow_def 📋 Init.Data.Rat.Lemmas
  (q : ℚ) (n : ℕ) : q ^ n = { num := q.num ^ n, den := q.den ^ n, den_nz := ⋯, reduced := ⋯ }
• Rat.mkRat_def 📋 Init.Data.Rat.Lemmas
  (n : ℤ) (d : ℕ) : mkRat n d = if d0 : d = 0 then 0 else Rat.normalize n d d0
• Rat.ofScientific_def' 📋 Init.Data.Rat.Lemmas
  {m : ℕ} {s : Bool} {e : ℕ} : OfScientific.ofScientific m s e = ↑m * 10 ^ if s = true then -↑e else ↑e
• Rat.add_def' 📋 Init.Data.Rat.Lemmas
  (a b : ℚ) : a + b = mkRat (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
• Rat.sub_def' 📋 Init.Data.Rat.Lemmas
  (a b : ℚ) : a - b = mkRat (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den)
• Rat.ofScientific_def 📋 Init.Data.Rat.Lemmas
  {m : ℕ} {s : Bool} {e : ℕ} : Rat.ofScientific m s e = if s = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)
• Rat.add_def 📋 Init.Data.Rat.Lemmas
  (a b : ℚ) : a + b = Rat.normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯
• Rat.sub_def 📋 Init.Data.Rat.Lemmas
  (a b : ℚ) : a - b = Rat.normalize (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den) ⋯
• Rat.ofScientific_def_eq_if 📋 Init.Data.Rat.Lemmas
  {m : ℕ} {s : Bool} {e : ℕ} : OfScientific.ofScientific m s e = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e
• Lean.Grind.LawfulOfScientific.ofScientific_def 📋 Init.Grind.Ring.OfScientific
  {α : Type u} {inst✝ : Lean.Grind.Field α} {inst✝¹ : OfScientific α} [self : Lean.Grind.LawfulOfScientific α] {m : ℕ} {s : Bool} {e : ℕ} : OfScientific.ofScientific m s e = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e
• Lean.Grind.node_def 📋 Init.Grind.PP
  : ℕ → {α : Sort u} → {a : α} → NodeDef
• Std.Shrink.inflate_deflate 📋 Init.Data.Iterators.Basic
  {α : Type u_1} {x : α} : (Std.Shrink.deflate x).inflate = x
• Vector.singleton_def 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {v : α} : Vector.singleton v = #v[v]
• Vector.flatMap_def 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {f : α → Vector β m} : xs.flatMap f = (Vector.map f xs).flatten
• Max.oppositeMin_def 📋 Init.Data.Order.Opposite
  {α : Type u_1} {min : Max α} : min.oppositeMin = { min := max }
• Min.oppositeMax_def 📋 Init.Data.Order.Opposite
  {α : Type u_1} {min : Min α} : min.oppositeMax = { max := Min.min }
• LE.opposite_def 📋 Init.Data.Order.Opposite
  {α : Type u_1} {le : LE α} : le.opposite = { le := fun a b => b ≤ a }
• LT.opposite_def 📋 Init.Data.Order.Opposite
  {α : Type u_1} {lt : LT α} : lt.opposite = { lt := fun a b => b < a }
• Std.Internal.List.getValue!_eq_getValueD_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} : Std.Internal.List.getValue! a l = Std.Internal.List.getValueD a l default
• Std.Internal.List.getValue!_eq_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} (h : Std.Internal.List.containsKey a l = false) : Std.Internal.List.getValue! a l = default
• Std.Internal.List.getKey!_eq_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} (h : Std.Internal.List.containsKey a l = false) : Std.Internal.List.getKey! a l = default
• Std.Internal.List.getKey!_eq_getKeyD_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} : Std.Internal.List.getKey! a l = Std.Internal.List.getKeyD a l default
• Std.Internal.List.maxKey!_eq_maxKeyD_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} : Std.Internal.List.maxKey! l = Std.Internal.List.maxKeyD l default
• Std.Internal.List.minKey!_eq_minKeyD_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} : Std.Internal.List.minKey! l = Std.Internal.List.minKeyD l default
• Std.Internal.List.getValueCast!_eq_getValueCastD_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] : Std.Internal.List.getValueCast! a l = Std.Internal.List.getValueCastD a l default
• Std.Internal.List.getValueCast!_eq_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (h : Std.Internal.List.containsKey a l = false) : Std.Internal.List.getValueCast! a l = default
• Std.Internal.List.maxKey!_eq_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (h : l.isEmpty = true) : Std.Internal.List.maxKey! l = default
• Std.Internal.List.minKey!_eq_default 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (h : l.isEmpty = true) : Std.Internal.List.minKey! l = default
• Std.DHashMap.Internal.Raw₀.getKey!_eq_getKeyD_default 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : (↑m).WF) {a : α} : m.getKey! a = m.getKeyD a default
• 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₀.get!_eq_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.contains a = false → m.get! a = default
• Std.DHashMap.Internal.Raw₀.getKey!_eq_default 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : (↑m).WF) {a : α} : m.contains a = false → m.getKey! a = default
• 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.get!_eq_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 : α} : m.contains a = false → Std.DHashMap.Internal.Raw₀.Const.get! m a = default
• Std.DHashMap.getKey!_eq_getKeyD_default 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.getKey! a = m.getKeyD a default
• 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.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.get!_eq_default_of_contains_eq_false 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] : m.contains a = false → m.get! a = default
• Std.DHashMap.getKey!_eq_default_of_contains_eq_false 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.contains a = false → m.getKey! a = default
• Std.DHashMap.Const.get!_eq_default_of_contains_eq_false 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m.contains a = false → Std.DHashMap.Const.get! m a = default
• Std.DHashMap.get!_eq_default 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] : a ∉ m → m.get! a = default
• Std.DHashMap.getKey!_eq_default 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : a ∉ m → m.getKey! a = default
• Std.DHashMap.Const.get!_eq_default 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : a ∉ m → Std.DHashMap.Const.get! m a = default
• Std.Internal.ComputableSmall.inflate_deflate 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {α : Type v} [self : Std.Internal.ComputableSmall α] {a : α} : Std.Internal.ComputableSmall.inflate (Std.Internal.ComputableSmall.deflate a) = a
• Std.Internal.USquash.inflate_deflate 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {α : Type v} {x✝ : Std.Internal.Small α} {x : α} : (Std.Internal.USquash.deflate x).inflate = x
• Std.DTreeMap.Internal.Impl.maxKey!_eq_maxKeyD_default 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Inhabited α] (h : t.WF) : t.maxKey! = t.maxKeyD default
• Std.DTreeMap.Internal.Impl.minKey!_eq_minKeyD_default 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Inhabited α] (h : t.WF) : t.minKey! = t.minKeyD default
• Std.DTreeMap.Internal.Impl.maxKey!_eq_default 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Inhabited α] (h : t.WF) (he : t.isEmpty = true) : t.maxKey! = default
• Std.DTreeMap.Internal.Impl.minKey!_eq_default 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Inhabited α] (h : t.WF) (he : t.isEmpty = true) : t.minKey! = default
• Std.DTreeMap.Internal.Impl.getKey!_eq_getKeyD_default 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Inhabited α] (h : t.WF) {a : α} : t.getKey! a = t.getKeyD a default
• Std.DTreeMap.Internal.Impl.Const.get!_eq_getD_default 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] [Inhabited β] (h : t.WF) {a : α} : Std.DTreeMap.Internal.Impl.Const.get! t a = Std.DTreeMap.Internal.Impl.Const.getD t a default
• Std.DTreeMap.Internal.Impl.getKey!_eq_default_of_contains_eq_false 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Inhabited α] (h : t.WF) {a : α} : Std.DTreeMap.Internal.Impl.contains a t = false → t.getKey! a = default
• Std.DTreeMap.Internal.Impl.Const.get!_eq_default_of_contains_eq_false 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] [Inhabited β] (h : t.WF) {a : α} : Std.DTreeMap.Internal.Impl.contains a t = false → Std.DTreeMap.Internal.Impl.Const.get! t a = default
• Std.DTreeMap.Internal.Impl.getKey!_eq_default 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Inhabited α] (h : t.WF) {a : α} : a ∉ t → t.getKey! a = default
• Std.DTreeMap.Internal.Impl.get!_eq_getD_default 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] : t.get! a = t.getD a default
• Std.DTreeMap.Internal.Impl.Const.get!_eq_default 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] [Inhabited β] (h : t.WF) {a : α} : a ∉ t → Std.DTreeMap.Internal.Impl.Const.get! t a = default
• Std.DTreeMap.Internal.Impl.get!_eq_default_of_contains_eq_false 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] : Std.DTreeMap.Internal.Impl.contains a t = false → t.get! a = default
• Std.DTreeMap.Internal.Impl.get!_eq_default 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {a : α} [Inhabited (β a)] : a ∉ t → t.get! a = default
• Std.DTreeMap.maxKey!_eq_maxKeyD_default 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α] : t.maxKey! = t.maxKeyD default
• Std.DTreeMap.minKey!_eq_minKeyD_default 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α] : t.minKey! = t.minKeyD default
• Std.DTreeMap.getKey!_eq_getKeyD_default 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α] {a : α} : t.getKey! a = t.getKeyD a default
• Std.DTreeMap.maxKey!_eq_default 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α] (he : t.isEmpty = true) : t.maxKey! = default
• Std.DTreeMap.minKey!_eq_default 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α] (he : t.isEmpty = true) : t.minKey! = default
• Std.DTreeMap.Const.get!_eq_getD_default 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] [Inhabited β] {a : α} : Std.DTreeMap.Const.get! t a = Std.DTreeMap.Const.getD t a default
• Std.DTreeMap.getKey!_eq_default_of_contains_eq_false 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α] {a : α} : t.contains a = false → t.getKey! a = default
• Std.DTreeMap.Const.get!_eq_default_of_contains_eq_false 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] [Inhabited β] {a : α} : t.contains a = false → Std.DTreeMap.Const.get! t a = default
• Std.DTreeMap.getKey!_eq_default 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α] {a : α} : a ∉ t → t.getKey! a = default
• Std.DTreeMap.get!_eq_getD_default 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a : α} [Inhabited (β a)] : t.get! a = t.getD a default
• Std.DTreeMap.Const.get!_eq_default 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] [Inhabited β] {a : α} : a ∉ t → Std.DTreeMap.Const.get! t a = default
• Std.DTreeMap.get!_eq_default_of_contains_eq_false 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a : α} [Inhabited (β a)] : t.contains a = false → t.get! a = default
• Std.DTreeMap.get!_eq_default 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a : α} [Inhabited (β a)] : a ∉ t → t.get! a = default
• Std.ExtDHashMap.get!_eq_getD_default 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] : m.get! a = m.getD a default
• Std.ExtDHashMap.getKey!_eq_getKeyD_default 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.getKey! a = m.getKeyD a default
• Std.ExtDHashMap.Const.get!_eq_getD_default 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : Std.ExtDHashMap.Const.get! m a = Std.ExtDHashMap.Const.getD m a default
• Std.ExtDHashMap.getKey!_eq_default_of_contains_eq_false 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.contains a = false → m.getKey! a = default
• Std.ExtDHashMap.Const.get!_eq_default_of_contains_eq_false 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m.contains a = false → Std.ExtDHashMap.Const.get! m a = default
• Std.ExtDHashMap.get!_eq_default_of_contains_eq_false 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] : m.contains a = false → m.get! a = default
• Std.ExtDHashMap.getKey!_eq_default 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : a ∉ m → m.getKey! a = default
• Std.ExtDHashMap.Const.get!_eq_default 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : a ∉ m → Std.ExtDHashMap.Const.get! m a = default
• Std.ExtDHashMap.get!_eq_default 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] : a ∉ m → m.get! a = default
• Std.ExtHashMap.getKey!_eq_getKeyD_default 📋 Std.Data.ExtHashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.getKey! a = m.getKeyD a default
• Std.ExtHashMap.getKey!_eq_default_of_contains_eq_false 📋 Std.Data.ExtHashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.contains a = false → m.getKey! a = default
• Std.ExtHashMap.getKey!_eq_default 📋 Std.Data.ExtHashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : a ∉ m → m.getKey! a = default
• Std.ExtHashMap.getElem!_eq_getD_default 📋 Std.Data.ExtHashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m[a]! = m.getD a default
• Std.ExtHashMap.getElem!_eq_default_of_contains_eq_false 📋 Std.Data.ExtHashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m.contains a = false → m[a]! = default
• Std.ExtHashMap.getElem!_eq_default 📋 Std.Data.ExtHashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : a ∉ m → m[a]! = default

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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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 128218b serving mathlib revision 4644b1d