Loogle!

Result

Found 3005 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
• Nat.beq.eq_def 📋 Init.Data.Nat.Basic
  (x✝ x✝¹ : ℕ) : x✝.beq x✝¹ = match x✝, x✝¹ with | Nat.zero, Nat.zero => true | Nat.zero, n.succ => false | n.succ, Nat.zero => false | n.succ, m.succ => n.beq 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)
• Nat.modCore.go.eq_def 📋 Init.Data.Nat.Div.Basic
  (y : ℕ) (hy : 0 < y) (fuel x : ℕ) (hfuel : x < fuel) : Nat.modCore.go y hy fuel x hfuel = match fuel, hfuel with | fuel.succ, hfuel => if h : y ≤ x then Nat.modCore.go y hy fuel (x - y) ⋯ else x
• Nat.div.go.eq_def 📋 Init.Data.Nat.Div.Basic
  (y : ℕ) (hy : 0 < y) (fuel x : ℕ) (hfuel : x < fuel) : Nat.div.go y hy fuel x hfuel = match fuel, hfuel with | fuel.succ, hfuel => if h : y ≤ x then Nat.div.go y hy fuel (x - y) ⋯ + 1 else 0
• Nat.div.inductionOn.eq_def 📋 Init.Data.Nat.Div.Basic
  {motive : ℕ → ℕ → Sort u} (x y : ℕ) (ind : (x y : ℕ) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y) (base : (x y : ℕ) → ¬(0 < y ∧ y ≤ x) → motive x y) : Nat.div.inductionOn x y ind base = if h : 0 < y ∧ y ≤ x then ind x y h (Nat.div.inductionOn (x - y) y ind base) else base x y h
• Fin.neg_def 📋 Init.Data.Fin.Basic
  {n : ℕ} (a : Fin n) : -a = ⟨(n - ↑a) % n, ⋯⟩
• List.lengthTRAux.eq_def 📋 Init.Data.List.Basic
  {α : Type u_1} (x✝ : List α) (x✝¹ : ℕ) : x✝.lengthTRAux x✝¹ = match x✝, x✝¹ with | [], n => n | head :: as, n => as.lengthTRAux n.succ
• List.replicate.eq_def 📋 Init.Data.List.Basic
  {α : Type u} (x✝ : ℕ) (x✝¹ : α) : List.replicate x✝ x✝¹ = match x✝, x✝¹ with | 0, x => [] | n.succ, a => a :: List.replicate n a
• List.dropLast.eq_def 📋 Init.Data.List.Basic
  {α : Type u_1} (x✝ : List α) : x✝.dropLast = match x✝ with | [] => [] | [head] => [] | a :: as => a :: as.dropLast
• List.map.eq_def 📋 Init.Data.List.Basic
  {α : Type u_1} {β : Type u_2} (f : α → β) (x✝ : List α) : List.map f x✝ = match x✝ with | [] => [] | a :: as => f a :: List.map f as
• List.replicateTR.loop.eq_def 📋 Init.Data.List.Basic
  {α : Type u} (a : α) (x✝ : ℕ) (x✝¹ : List α) : List.replicateTR.loop a x✝ x✝¹ = match x✝, x✝¹ with | 0, as => as | n.succ, as => List.replicateTR.loop a n (a :: as)
• List.append.eq_def 📋 Init.Data.List.Basic
  {α : Type u_1} (x✝ x✝¹ : List α) : x✝.append x✝¹ = match x✝, x✝¹ with | [], bs => bs | a :: as, bs => a :: as.append bs
• List.concat.eq_def 📋 Init.Data.List.Basic
  {α : Type u} (x✝ : List α) (x✝¹ : α) : x✝.concat x✝¹ = match x✝, x✝¹ with | [], b => [b] | a :: as, b => a :: as.concat b
• List.reverseAux.eq_def 📋 Init.Data.List.Basic
  {α : Type u} (x✝ x✝¹ : List α) : x✝.reverseAux x✝¹ = match x✝, x✝¹ with | [], r => r | a :: l, r => l.reverseAux (a :: r)
• List.length.eq_def 📋 Init.Data.List.Basic
  {α : Type u_1} (x✝ : List α) : x✝.length = match x✝ with | [] => 0 | head :: as => as.length + 1
• List.elem.eq_def 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (a : α) (x✝ : List α) : List.elem a x✝ = match x✝ with | [] => false | b :: bs => match a == b with | true => true | false => List.elem a bs
• List.intersperse.eq_def 📋 Init.Data.List.Basic
  {α : Type u} (sep : α) (x✝ : List α) : List.intersperse sep x✝ = match x✝ with | [] => [] | [x] => [x] | x :: xs => x :: sep :: List.intersperse sep xs
• List.filter.eq_def 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (x✝ : List α) : List.filter p x✝ = match x✝ with | [] => [] | a :: as => match p a with | true => a :: List.filter p as | false => List.filter p as
• List.isPrefixOf.eq_def 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (x✝ x✝¹ : List α) : x✝.isPrefixOf x✝¹ = match x✝, x✝¹ with | [], x => true | x, [] => false | a :: as, b :: bs => a == b && as.isPrefixOf bs
• List.beq.eq_def 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (x✝ x✝¹ : List α) : x✝.beq x✝¹ = match x✝, x✝¹ with | [], [] => true | a :: as, b :: bs => a == b && as.beq bs | x, x_1 => false
• List.mapTR.loop.eq_def 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) (x✝ : List α) (x✝¹ : List β) : List.mapTR.loop f x✝ x✝¹ = match x✝, x✝¹ with | [], bs => bs.reverse | a :: as, bs => List.mapTR.loop f as (f a :: bs)
• List.set.eq_def 📋 Init.Data.List.Basic
  {α : Type u_1} (x✝ : List α) (x✝¹ : ℕ) (x✝² : α) : x✝.set x✝¹ x✝² = match x✝, x✝¹, x✝² with | head :: as, 0, b => b :: as | a :: as, n.succ, b => a :: as.set n b | [], x, x_1 => []
• List.erase.eq_def 📋 Init.Data.List.Basic
  {α : Type u_1} [BEq α] (x✝ : List α) (x✝¹ : α) : x✝.erase x✝¹ = match x✝, x✝¹ with | [], x => [] | a :: as, b => match a == b with | true => as | false => a :: as.erase b
• List.zipWith.eq_def 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (x✝ : List α) (x✝¹ : List β) : List.zipWith f x✝ x✝¹ = match x✝, x✝¹ with | x :: xs, y :: ys => f x y :: List.zipWith f xs ys | x, x_1 => []
• List.range'TR.go.eq_def 📋 Init.Data.List.Basic
  (step x✝ x✝¹ : ℕ) (x✝² : List ℕ) : List.range'TR.go step x✝ x✝¹ x✝² = match x✝, x✝¹, x✝² with | 0, x, acc => acc | n.succ, e, acc => List.range'TR.go step n (e - step) ((e - step) :: acc)
• List.filterTR.loop.eq_def 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (x✝ x✝¹ : List α) : List.filterTR.loop p x✝ x✝¹ = match x✝, x✝¹ with | [], acc => acc.reverse | a :: as, acc => match p a with | true => List.filterTR.loop p as (a :: acc) | false => List.filterTR.loop p as acc
• List.toByteArray.loop.eq_def 📋 Init.Data.ByteArray.Bootstrap
  (x✝ : List UInt8) (x✝¹ : ByteArray) : List.toByteArray.loop x✝ x✝¹ = match x✝, x✝¹ with | [], r => r | b :: bs, r => List.toByteArray.loop bs (r.push b)
• 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
• Array.findIdx?.loop.eq_def 📋 Init.Data.Array.Basic
  {α : Type u} (p : α → Bool) (as : Array α) (j : ℕ) : Array.findIdx?.loop p as j = if h : j < as.size then if p as[j] = true then some j else Array.findIdx?.loop p as (j + 1) else none
• Array.anyM.loop.eq_def 📋 Init.Data.Array.Basic
  {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (stop : ℕ) (h : stop ≤ as.size) (j : ℕ) : Array.anyM.loop p as stop h j = if hlt : j < stop then have this := ⋯; do let __do_lift ← p as[j] if __do_lift = true then pure true else Array.anyM.loop p as stop h (j + 1) else pure false
• Array.reverse.loop.eq_def 📋 Init.Data.Array.Basic
  {α : Type u} (as : Array α) (i : ℕ) (j : Fin as.size) : Array.reverse.loop as i j = if h : i < ↑j then have this := ⋯; let as_1 := as.swap i ↑j ⋯ ⋯; have this := ⋯; Array.reverse.loop as_1 (i + 1) ⟨↑j - 1, this⟩ else as
• List.drop.eq_def 📋 Init.Data.Array.GetLit
  {α : Type u} (x✝ : ℕ) (x✝¹ : List α) : List.drop x✝ x✝¹ = match x✝, x✝¹ with | 0, as => as | n.succ, [] => [] | n.succ, head :: as => List.drop n as
• Array.toListLitAux.eq_def 📋 Init.Data.Array.GetLit
  {α : Type u_1} (xs : Array α) (n : ℕ) (hsz : xs.size = n) (x✝ : ℕ) (x✝¹ : x✝ ≤ xs.size) (x✝² : List α) : xs.toListLitAux n hsz x✝ x✝¹ x✝² = match x✝, x✝¹, x✝² with | 0, x, acc => acc | i.succ, hi, acc => xs.toListLitAux n hsz i ⋯ (xs.getLit i hsz ⋯ :: acc)
• Lean.RArray.getImpl.eq_def 📋 Init.Data.RArray
  {α : Type u} (a : Lean.RArray α) (n : ℕ) : a.getImpl n = match a with | Lean.RArray.leaf x => x | Lean.RArray.branch p l r => if n < p then l.getImpl n else r.getImpl n
• Nat.Linear.Poly.norm.go.eq_def 📋 Init.Data.Nat.Linear
  (p r : Nat.Linear.Poly) : Nat.Linear.Poly.norm.go p r = match p with | [] => r | (k, v) :: p => Nat.Linear.Poly.norm.go p (Nat.Linear.Poly.insert k v r)
• Nat.Linear.Poly.isNonZero.eq_def 📋 Init.Data.Nat.Linear
  (p : Nat.Linear.Poly) : p.isNonZero = match p with | [] => false | (k, v) :: p => bif v == Nat.Linear.fixedVar then decide (k > 0) else Nat.Linear.Poly.isNonZero p
• Nat.Linear.instBEqPolyCnstr.beq.eq_def 📋 Init.Data.Nat.Linear
  (x✝ x✝¹ : Nat.Linear.PolyCnstr) : Nat.Linear.instBEqPolyCnstr.beq x✝ x✝¹ = match x✝, x✝¹ with | { eq := a, lhs := a_1, rhs := a_2 }, { eq := b, lhs := b_1, rhs := b_2 } => a == b && (a_1 == b_1 && a_2 == b_2) | x, x_1 => false
• Nat.Linear.Poly.insert.eq_def 📋 Init.Data.Nat.Linear
  (k : ℕ) (v : Nat.Linear.Var) (p : Nat.Linear.Poly) : Nat.Linear.Poly.insert k v p = match p with | [] => [(k, v)] | (k', v') :: p => bif Nat.blt v v' then (k, v) :: (k', v') :: p else bif Nat.beq v v' then (k + k', v') :: p else (k', v') :: Nat.Linear.Poly.insert k v p
• Nat.Linear.Expr.toPoly.go.eq_def 📋 Init.Data.Nat.Linear
  (coeff : ℕ) (x✝ : Nat.Linear.Expr) : Nat.Linear.Expr.toPoly.go coeff x✝ = match (motive := Nat.Linear.Expr → Nat.Linear.Poly → Nat.Linear.Poly) x✝ with | Nat.Linear.Expr.num k => bif k == 0 then id else fun x => (coeff * k, Nat.Linear.fixedVar) :: x | Nat.Linear.Expr.var i => fun x => (coeff, i) :: x | a.add b => Nat.Linear.Expr.toPoly.go coeff a ∘ Nat.Linear.Expr.toPoly.go coeff b | Nat.Linear.Expr.mulL k a => bif k == 0 then id else Nat.Linear.Expr.toPoly.go (coeff * k) a | a.mulR k => bif k == 0 then id else Nat.Linear.Expr.toPoly.go (coeff * k) a
• Nat.Linear.Poly.cancelAux.eq_def 📋 Init.Data.Nat.Linear
  (fuel : ℕ) (m₁ m₂ r₁ r₂ : Nat.Linear.Poly) : Nat.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂ = match fuel with | 0 => (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) | fuel.succ => match m₁, m₂ with | m₁, [] => (List.reverse r₁ ++ m₁, List.reverse r₂) | [], m₂ => (List.reverse r₁, List.reverse r₂ ++ m₂) | (k₁, v₁) :: m₁, (k₂, v₂) :: m₂ => bif Nat.blt v₁ v₂ then Nat.Linear.Poly.cancelAux fuel m₁ ((k₂, v₂) :: m₂) ((k₁, v₁) :: r₁) r₂ else bif Nat.blt v₂ v₁ then Nat.Linear.Poly.cancelAux fuel ((k₁, v₁) :: m₁) m₂ r₁ ((k₂, v₂) :: r₂) else bif k₁.blt k₂ then Nat.Linear.Poly.cancelAux fuel m₁ m₂ r₁ ((k₂.sub k₁, v₁) :: r₂) else bif k₂.blt k₁ then Nat.Linear.Poly.cancelAux fuel m₁ m₂ ((k₁.sub k₂, v₁) :: r₁) r₂ else Nat.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂
• 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.natAbs.eq_def 📋 Init.Data.Int.Order
  (m : ℤ) : m.natAbs = match m with | Int.ofNat m => m | Int.negSucc m => m.succ
• 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
• List.get.eq_def 📋 Init.Data.List.BasicAux
  {α : Type u} (x✝ : List α) (x✝¹ : Fin x✝.length) : x✝.get x✝¹ = match x✝, x✝¹ with | a :: tail, ⟨0, isLt⟩ => a | head :: as, ⟨i.succ, h⟩ => as.get ⟨i, ⋯⟩
• List.compareLex.eq_def 📋 Init.Data.Ord.Basic
  {α : Type u_1} (cmp : α → α → Ordering) (x✝ x✝¹ : List α) : List.compareLex cmp x✝ x✝¹ = match x✝, x✝¹ with | [], [] => Ordering.eq | [], x => Ordering.lt | x, [] => Ordering.gt | x :: xs, y :: ys => match cmp x y with | Ordering.lt => Ordering.lt | Ordering.eq => List.compareLex cmp xs ys | Ordering.gt => Ordering.gt
• 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, ⋯⟩
• Fin.reverseInduction.go.eq_def 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (cast : (i : Fin n) → motive i.succ → motive i.castSucc) (i : Fin (n + 1)) (j : ℕ) (h : j < n + 1) (h2 : ↑i ≤ j) (x : motive ⟨j, h⟩) : Fin.reverseInduction.go cast i j h h2 x = if hi : ↑i = j then _root_.cast ⋯ x else match j, h, h2, x, hi with | 0, h, h2, x, hi => ⋯.elim | j.succ, h, h2, x, hi => Fin.reverseInduction.go cast i j ⋯ ⋯ (cast ⟨j, ⋯⟩ x)
• Fin.foldr.loop.eq_def 📋 Init.Data.Fin.Fold
  {α : Sort u_1} (n : ℕ) (f : Fin n → α → α) (x✝ : ℕ) (x✝¹ : x✝ ≤ n) (x✝² : α) : Fin.foldr.loop n f x✝ x✝¹ x✝² = match x✝, x✝¹, x✝² with | 0, x, x_1 => x_1 | i.succ, h, x => Fin.foldr.loop n f i ⋯ (f ⟨i, h⟩ x)
• 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.findSome?.eq_def 📋 Init.Data.List.Control
  {α : Type u} {β : Type v} (f : α → Option β) (x✝ : List α) : List.findSome? f x✝ = match x✝ with | [] => none | a :: as => match f a with | some b => some b | none => List.findSome? f as
• List.foldlM.eq_def 📋 Init.Data.List.Control
  {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (x✝ : s → α → m s) (x✝¹ : s) (x✝² : List α) : List.foldlM x✝ x✝¹ x✝² = match x✝, x✝¹, x✝² with | x, s_1, [] => pure s_1 | f, s_1, a :: as => do let s' ← f s_1 a List.foldlM f s' as
• 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.flatten.eq_def 📋 Init.Data.List.Lemmas
  {α : Type u_1} (x✝ : List (List α)) : x✝.flatten = match x✝ with | [] => [] | l :: L => l.append L.flatten
• List.foldr.eq_def 📋 Init.Data.List.Lemmas
  {α : Type u} {β : Type v} (f : α → β → β) (init : β) (x✝ : List α) : List.foldr f init x✝ = match x✝ with | [] => init | a :: l => f a (List.foldr f init l)
• List.filterMap.eq_def 📋 Init.Data.List.Lemmas
  {α : Type u} {β : Type v} (f : α → Option β) (x✝ : List α) : List.filterMap f x✝ = match x✝ with | [] => [] | a :: as => match f a with | none => List.filterMap f as | some b => b :: List.filterMap f as
• List.isEqv.eq_def 📋 Init.Data.List.Lemmas
  {α : Type u} (x✝ x✝¹ : List α) (x✝² : α → α → Bool) : x✝.isEqv x✝¹ x✝² = match x✝, x✝¹, x✝² with | [], [], x => true | a :: as, b :: bs, eqv => eqv a b && as.isEqv bs eqv | x, x_1, x_2 => false
• List.eraseDupsBy.loop.eq_def 📋 Init.Data.List.Lemmas
  {α : Type u_1} (r : α → α → Bool) (x✝ x✝¹ : List α) : List.eraseDupsBy.loop r x✝ x✝¹ = match x✝, x✝¹ with | [], bs => bs.reverse | a :: as, bs => match bs.any (r a) with | true => List.eraseDupsBy.loop r as bs | false => List.eraseDupsBy.loop r as (a :: bs)
• List.splitAt.go.eq_def 📋 Init.Data.List.Lemmas
  {α : Type u} (l x✝ : List α) (x✝¹ : ℕ) (x✝² : List α) : List.splitAt.go l x✝ x✝¹ x✝² = match x✝, x✝¹, x✝² with | [], x, x_1 => (l, []) | x :: xs, n.succ, acc => List.splitAt.go l xs n (x :: acc) | xs, x, acc => (acc.reverse, xs)
• List.getLast.eq_def 📋 Init.Data.List.Lemmas
  {α : Type u} (x✝ : List α) (x✝¹ : x✝ ≠ []) : x✝.getLast x✝¹ = match x✝, x✝¹ with | [], h => absurd ⋯ h | [a], x => a | head :: b :: as, x => (b :: as).getLast ⋯
• List.partition.loop.eq_def 📋 Init.Data.List.Lemmas
  {α : Type u} (p : α → Bool) (x✝ : List α) (x✝¹ : List α × List α) : List.partition.loop p x✝ x✝¹ = match x✝, x✝¹ with | [], (bs, cs) => (bs.reverse, cs.reverse) | a :: as, (bs, cs) => match p a with | true => List.partition.loop p as (a :: bs, cs) | false => List.partition.loop p as (bs, a :: cs)
• List.take.eq_def 📋 Init.Data.List.TakeDrop
  {α : Type u} (x✝ : ℕ) (x✝¹ : List α) : List.take x✝ x✝¹ = match x✝, x✝¹ with | 0, x => [] | n.succ, [] => [] | n.succ, a :: as => a :: List.take n as
• List.dropWhile.eq_def 📋 Init.Data.List.TakeDrop
  {α : Type u} (p : α → Bool) (x✝ : List α) : List.dropWhile p x✝ = match x✝ with | [] => [] | a :: l => match p a with | true => List.dropWhile p l | false => a :: l
• List.takeWhile.eq_def 📋 Init.Data.List.TakeDrop
  {α : Type u} (p : α → Bool) (x✝ : List α) : List.takeWhile p x✝ = match x✝ with | [] => [] | hd :: tl => match p hd with | true => hd :: List.takeWhile p tl | false => []
• List.subset_def 📋 Init.Data.List.Sublist
  {α : Type u_1} {l₁ l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂
• List.isSublist.eq_def 📋 Init.Data.List.Sublist
  {α : Type u} [BEq α] (x✝ x✝¹ : List α) : x✝.isSublist x✝¹ = match x✝, x✝¹ with | [], x => true | x, [] => false | l₁@h:(hd₁ :: tl₁), hd₂ :: tl₂ => if (hd₁ == hd₂) = true then tl₁.isSublist tl₂ else l₁.isSublist tl₂
• List.countP.go.eq_def 📋 Init.Data.List.Count
  {α : Type u} (p : α → Bool) (x✝ : List α) (x✝¹ : ℕ) : List.countP.go p x✝ x✝¹ = match x✝, x✝¹ with | [], acc => acc | x :: xs, acc => bif p x then List.countP.go p xs (acc + 1) else List.countP.go p xs acc
• List.pmap.eq_def 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (x✝ : List α) (x✝¹ : ∀ a ∈ x✝, P a) : List.pmap f x✝ x✝¹ = match x✝, x✝¹ with | [], x => [] | a :: l, H => f a ⋯ :: List.pmap f l ⋯
• Array.foldlM.loop.eq_def 📋 Init.Data.Array.Bootstrap
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (as : Array α) (stop : ℕ) (h : stop ≤ as.size) (i j : ℕ) (b : β) : Array.foldlM.loop f as stop h i j b = if hlt : j < stop then match i with | 0 => pure b | i'.succ => have this := ⋯; do let __do_lift ← f b as[j] Array.foldlM.loop f as stop h i' (j + 1) __do_lift else pure b
• Array.foldrM.fold.eq_def 📋 Init.Data.Array.Bootstrap
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (as : Array α) (stop i : ℕ) (h : i ≤ as.size) (b : β) : Array.foldrM.fold f as stop i h b = if (i == stop) = true then pure b else match i, h with | 0, x => pure b | i.succ, h => have this := ⋯; do let __do_lift ← f as[i] b Array.foldrM.fold f as stop i ⋯ __do_lift
• List.mapM.loop.eq_def 📋 Init.Data.List.Monadic
  {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) (x✝ : List α) (x✝¹ : List β) : List.mapM.loop f x✝ x✝¹ = match x✝, x✝¹ with | [], bs => pure bs.reverse | a :: as, bs => do let __do_lift ← f a List.mapM.loop f as (__do_lift :: bs)
• List.mapM'.eq_def 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) (x✝ : List α) : List.mapM' f x✝ = match x✝ with | [] => pure [] | a :: l => do let __do_lift ← f a let __do_lift_1 ← List.mapM' f l pure (__do_lift :: __do_lift_1)
• List.flatMapM.loop.eq_def 📋 Init.Data.List.Monadic
  {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (x✝ : List α) (x✝¹ : List (List β)) : List.flatMapM.loop f x✝ x✝¹ = match x✝, x✝¹ with | [], bs => pure bs.reverse.flatten | a :: as, bs => do let bs' ← f a List.flatMapM.loop f as (bs' :: bs)
• List.zipWithM.loop.eq_def 📋 Init.Data.List.Monadic
  {m : Type u → Type v} [Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ) (x✝ : List α) (x✝¹ : List β) (x✝² : Array γ) : List.zipWithM.loop f x✝ x✝¹ x✝² = match x✝, x✝¹, x✝² with | a :: as, b :: bs, acc => do let __do_lift ← f a b List.zipWithM.loop f as bs (acc.push __do_lift) | x, x_1, acc => pure acc.toList
• List.filterMapM.loop.eq_def 📋 Init.Data.List.Monadic
  {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (x✝ : List α) (x✝¹ : List β) : List.filterMapM.loop f x✝ x✝¹ = match x✝, x✝¹ with | [], bs => pure bs.reverse | a :: as, bs => do let __do_lift ← f a match __do_lift with | none => List.filterMapM.loop f as bs | some b => List.filterMapM.loop f as (b :: bs)
• List.zipWithM'.eq_def 📋 Init.Data.List.Monadic
  {m : Type u → Type v} [Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ) (x✝ : List α) (x✝¹ : List β) : List.zipWithM' f x✝ x✝¹ = match x✝, x✝¹ with | x :: xs, y :: ys => do let z ← f x y let zs ← List.zipWithM' f xs ys pure (z :: zs) | x, x_1 => pure []
• List.forIn'.loop.eq_def 📋 Init.Data.List.Monadic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (f : (a : α) → a ∈ as → β → m (ForInStep β)) (x✝ : List α) (x✝¹ : β) (x✝² : ∃ bs, bs ++ x✝ = as) : List.forIn'.loop as f x✝ x✝¹ x✝² = match x✝, x✝¹, x✝² with | [], b, x => pure b | a :: as', b, h => have this := ⋯; do let __do_lift ← f a this b match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => have this := ⋯; List.forIn'.loop as f as' b this
• BitVec.hash.eq_def 📋 Init.Data.BitVec.Basic
  {n : ℕ} (bv : BitVec n) : bv.hash = if n ≤ 64 then (↑bv.toFin).toUInt64 else mixHash (↑bv.toFin).toUInt64 (BitVec.setWidth (n - 64) (bv >>> 64)).hash
• 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.ofBoolListBE.eq_def 📋 Init.Data.BitVec.Lemmas
  (x✝ : List Bool) : BitVec.ofBoolListBE x✝ = match x✝ with | [] => 0#0 | b :: bs => BitVec.cons b (BitVec.ofBoolListBE bs)
• BitVec.ofBoolListLE.eq_def 📋 Init.Data.BitVec.Lemmas
  (x✝ : List Bool) : BitVec.ofBoolListLE x✝ = match x✝ with | [] => 0#0 | b :: bs => (BitVec.ofBoolListLE bs).concat b
• 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.reverse.eq_def 📋 Init.Data.BitVec.Lemmas
  (x✝ : ℕ) (x✝¹ : BitVec x✝) : x✝¹.reverse = match x✝, x✝¹ with | 0, x => x | w.succ, x => (BitVec.truncate w x).reverse.concat x.msb
• 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 }
• BitVec.replicate.eq_def 📋 Init.Data.BitVec.Lemmas
  {w : ℕ} (x✝ : ℕ) (x✝¹ : BitVec w) : BitVec.replicate x✝ x✝¹ = match x✝, x✝¹ with | 0, x => 0#0 | n.succ, x => BitVec.cast ⋯ (x ++ BitVec.replicate n x)
• BitVec.sshiftRightRec.eq_def 📋 Init.Data.BitVec.Bitblast
  {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (n : ℕ) : x.sshiftRightRec y n = have shiftAmt := y &&& BitVec.twoPow w₂ n; match n with | 0 => x.sshiftRight' shiftAmt | n.succ => (x.sshiftRightRec y n).sshiftRight' shiftAmt
• BitVec.shiftLeftRec.eq_def 📋 Init.Data.BitVec.Bitblast
  {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (n : ℕ) : x.shiftLeftRec y n = have shiftAmt := y &&& BitVec.twoPow w₂ n; match n with | 0 => x <<< shiftAmt | n.succ => x.shiftLeftRec y n <<< shiftAmt
• BitVec.ushiftRightRec.eq_def 📋 Init.Data.BitVec.Bitblast
  {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (n : ℕ) : x.ushiftRightRec y n = have shiftAmt := y &&& BitVec.twoPow w₂ n; match n with | 0 => x >>> shiftAmt | n.succ => x.ushiftRightRec y n >>> shiftAmt
• BitVec.mulRec.eq_def 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (x y : BitVec w) (s : ℕ) : x.mulRec y s = have cur := if y.getLsbD s = true then x <<< s else 0; match s with | 0 => cur | s.succ => x.mulRec y s + cur
• BitVec.uppcRec.eq_def 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (x : BitVec w) (s : ℕ) (hs : s < w) : x.uppcRec s hs = match s, hs with | 0, hs => x.msb | i.succ, hs => x[w - 1 - i] || x.uppcRec i ⋯
• BitVec.resRec.eq_def 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (x y : BitVec w) (s : ℕ) (hs : s < w) (hslt : 0 < s) : x.resRec y s hs hslt = match hs0 : s, hs, hslt with | 0, hs, hslt => ⋯.elim | s'.succ, hs, hslt => match hs' : s', hs, hslt, hs0 with | 0, hs, hslt, hs0 => x.aandRec y 1 hs | s''.succ, hs, hslt, hs0 => x.resRec y s' ⋯ ⋯ || x.aandRec y s ⋯
• 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
• List.range'.eq_def 📋 Init.Data.List.Range
  (x✝ x✝¹ x✝² : ℕ) : List.range' x✝ x✝¹ x✝² = match x✝, x✝¹, x✝² with | x, 0, x_1 => [] | s, n.succ, step => s :: List.range' (s + step) n step
• List.eraseIdx.eq_def 📋 Init.Data.List.Impl
  {α : Type u} (x✝ : List α) (x✝¹ : ℕ) : x✝.eraseIdx x✝¹ = match x✝, x✝¹ with | [], x => [] | head :: as, 0 => as | a :: as, n.succ => a :: as.eraseIdx n
• List.eraseP.eq_def 📋 Init.Data.List.Impl
  {α : Type u} (p : α → Bool) (x✝ : List α) : List.eraseP p x✝ = match x✝ with | [] => [] | a :: l => bif p a then l else a :: List.eraseP p l
• List.find?.eq_def 📋 Init.Data.List.Impl
  {α : Type u} (p : α → Bool) (x✝ : List α) : List.find? p x✝ = match x✝ with | [] => none | a :: as => match p a with | true => some a | false => List.find? p as
• List.findSomeRev?.eq_def 📋 Init.Data.List.Impl
  {α : Type u} {β : Type v} (f : α → Option β) (x✝ : List α) : List.findSomeRev? f x✝ = match x✝ with | [] => none | a :: as => match List.findSomeRev? f as with | some b => some b | none => f a
• List.findRev?.eq_def 📋 Init.Data.List.Impl
  {α : Type u} (p : α → Bool) (x✝ : List α) : List.findRev? p x✝ = match x✝ with | [] => none | a :: as => match List.findRev? p as with | some b => some b | none => if p a = true then some a else none
• List.zipIdx.eq_def 📋 Init.Data.List.Impl
  {α : Type u} (x✝ : List α) (x✝¹ : ℕ) : x✝.zipIdx x✝¹ = match x✝, x✝¹ with | [], x => [] | x :: xs, n => (x, n) :: xs.zipIdx (n + 1)
• List.replace.eq_def 📋 Init.Data.List.Impl
  {α : Type u} [BEq α] (x✝ : List α) (x✝¹ x✝² : α) : x✝.replace x✝¹ x✝² = match x✝, x✝¹, x✝² with | [], x, x_1 => [] | a :: as, b, c => match b == a with | true => c :: as | false => a :: as.replace b c
• List.filterMapTR.go.eq_def 📋 Init.Data.List.Impl
  {α : Type u_1} {β : Type u_2} (f : α → Option β) (x✝ : List α) (x✝¹ : Array β) : List.filterMapTR.go f x✝ x✝¹ = match x✝, x✝¹ with | [], acc => acc.toList | a :: as, acc => match f a with | none => List.filterMapTR.go f as acc | some b => List.filterMapTR.go f as (acc.push b)
• List.findIdx.go.eq_def 📋 Init.Data.List.Find
  {α : Type u} (p : α → Bool) (x✝ : List α) (x✝¹ : ℕ) : List.findIdx.go p x✝ x✝¹ = match x✝, x✝¹ with | [], n => n | a :: l, n => bif p a then n else List.findIdx.go p l (n + 1)
• List.findIdx?.go.eq_def 📋 Init.Data.List.Find
  {α : Type u} (p : α → Bool) (x✝ : List α) (x✝¹ : ℕ) : List.findIdx?.go p x✝ x✝¹ = match x✝, x✝¹ with | [], x => none | a :: l, i => if p a = true then some i else List.findIdx?.go p l (i + 1)
• List.findFinIdx?.go.eq_def 📋 Init.Data.List.Find
  {α : Type u} (p : α → Bool) (l x✝ : List α) (x✝¹ : ℕ) (x✝² : x✝.length + x✝¹ = l.length) : List.findFinIdx?.go p l x✝ x✝¹ x✝² = match x✝, x✝¹, x✝² with | [], x, x_1 => none | a :: l_1, i, h => if p a = true then some ⟨i, ⋯⟩ else List.findFinIdx?.go p l l_1 (i + 1) ⋯
• 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.forIn'.loop.eq_def 📋 Init.Data.List.ToArray
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : (a : α) → a ∈ as → β → m (ForInStep β)) (i : ℕ) (h : i ≤ as.size) (b : β) : Array.forIn'.loop as f i h b = match i, h with | 0, x => pure b | i.succ, h => have h' := ⋯; have this := ⋯; have this := ⋯; do let __do_lift ← f as[as.size - 1 - i] ⋯ b match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => Array.forIn'.loop as f i ⋯ b
• 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.extract.loop.eq_def 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (as : Array α) (i j : ℕ) (bs : Array α) : Array.extract.loop as i j bs = if hlt : j < as.size then match i with | 0 => bs | i'.succ => Array.extract.loop as i' (j + 1) (bs.push (as.getInternal j hlt)) else bs
• 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
• ByteArray.toList.loop.eq_def 📋 Init.Data.ByteArray.Basic
  (bs : ByteArray) (i : ℕ) (r : List UInt8) : ByteArray.toList.loop bs i r = if i < bs.size then ByteArray.toList.loop bs (i + 1) (bs.get! i :: r) else r.reverse
• ByteArray.findIdx?.loop.eq_def 📋 Init.Data.ByteArray.Basic
  (a : ByteArray) (p : UInt8 → Bool) (i : ℕ) : ByteArray.findIdx?.loop a p i = if h : i < a.size then if p a[i] = true then some i else ByteArray.findIdx?.loop a p (i + 1) else none
• ByteArray.findFinIdx?.loop.eq_def 📋 Init.Data.ByteArray.Basic
  (a : ByteArray) (p : UInt8 → Bool) (i : ℕ) : ByteArray.findFinIdx?.loop a p i = if h : i < a.size then if p a[i] = true then some ⟨i, h⟩ else ByteArray.findFinIdx?.loop a p (i + 1) else none
• ByteArray.utf8DecodeChar?.assemble₂.eq_def 📋 Init.Data.String.Decode
  (w x : UInt8) : ByteArray.utf8DecodeChar?.assemble₂ w x = if ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = true then none else let r := ByteArray.utf8DecodeChar?.assemble₂Unchecked w x; if r < 128 then none else some { val := r, valid := ⋯ }
• Char.utf8Size.eq_def 📋 Init.Data.String.Decode
  (c : Char) : c.utf8Size = have v := c.val; if v ≤ UInt32.ofNatLT 127 Char.utf8Size._proof_1 then 1 else if v ≤ UInt32.ofNatLT 2047 Char.utf8Size._proof_2 then 2 else if v ≤ UInt32.ofNatLT 65535 Char.utf8Size._proof_3 then 3 else 4
• ByteArray.utf8DecodeChar?.assemble₄.eq_def 📋 Init.Data.String.Decode
  (w x y z : UInt8) : ByteArray.utf8DecodeChar?.assemble₄ w x y z = if (ByteArray.utf8DecodeChar?.isInvalidContinuationByte x || ByteArray.utf8DecodeChar?.isInvalidContinuationByte y || ByteArray.utf8DecodeChar?.isInvalidContinuationByte z) = true then none else let r := ByteArray.utf8DecodeChar?.assemble₄Unchecked w x y z; if h₁ : r < 65536 then none else if h₂ : 1114111 < r then none else some { val := r, valid := ⋯ }
• UInt8.utf8ByteSize.eq_def 📋 Init.Data.String.Decode
  (c : UInt8) (_h : c.IsUTF8FirstByte) : c.utf8ByteSize _h = if c &&& 128 = 0 then 1 else if c &&& 224 = 192 then 2 else if c &&& 240 = 224 then 3 else 4
• ByteArray.utf8DecodeChar?.assemble₃.eq_def 📋 Init.Data.String.Decode
  (w x y : UInt8) : ByteArray.utf8DecodeChar?.assemble₃ w x y = if (ByteArray.utf8DecodeChar?.isInvalidContinuationByte x || ByteArray.utf8DecodeChar?.isInvalidContinuationByte y) = true then none else let r := ByteArray.utf8DecodeChar?.assemble₃Unchecked w x y; if r < 2048 then none else if hr : 55296 ≤ r ∧ r ≤ 57343 then none else some { val := r, valid := ⋯ }
• ByteArray.utf8DecodeChar?.parseFirstByte.eq_def 📋 Init.Data.String.Decode
  (b : UInt8) : ByteArray.utf8DecodeChar?.parseFirstByte b = if (b &&& 128 == 0) = true then ByteArray.utf8DecodeChar?.FirstByte.done else if (b &&& 224 == 192) = true then ByteArray.utf8DecodeChar?.FirstByte.oneMore else if (b &&& 240 == 224) = true then ByteArray.utf8DecodeChar?.FirstByte.twoMore else if (b &&& 248 == 240) = true then ByteArray.utf8DecodeChar?.FirstByte.threeMore else ByteArray.utf8DecodeChar?.FirstByte.invalid
• String.utf8EncodeCharFast.eq_def 📋 Init.Data.String.Decode
  (c : Char) : String.utf8EncodeCharFast c = have v := c.val; if v ≤ 127 then [v.toUInt8] else if v ≤ 2047 then [(v >>> 6).toUInt8 &&& 31 ||| 192, v.toUInt8 &&& 63 ||| 128] else if v ≤ 65535 then [(v >>> 12).toUInt8 &&& 15 ||| 224, (v >>> 6).toUInt8 &&& 63 ||| 128, v.toUInt8 &&& 63 ||| 128] else [(v >>> 18).toUInt8 &&& 7 ||| 240, (v >>> 12).toUInt8 &&& 63 ||| 128, (v >>> 6).toUInt8 &&& 63 ||| 128, v.toUInt8 &&& 63 ||| 128]

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 6ff4759 serving mathlib revision 7379a9f