Loogle!

Result

Found 69970 declarations mentioning Nat. Of these, only the first 200 are shown.

• Nat 📋 Init.Prelude
  : Type
• Lean.defaultMaxRecDepth 📋 Init.Prelude
  : ℕ
• Lean.firstFrontendMacroScope 📋 Init.Prelude
  : ℕ
• Lean.reservedMacroScope 📋 Init.Prelude
  : ℕ
• Nat.zero 📋 Init.Prelude
  : ℕ
• UInt16.size 📋 Init.Prelude
  : ℕ
• UInt32.size 📋 Init.Prelude
  : ℕ
• UInt64.size 📋 Init.Prelude
  : ℕ
• UInt8.size 📋 Init.Prelude
  : ℕ
• USize.size 📋 Init.Prelude
  : ℕ
• System.Platform.numBits 📋 Init.Prelude
  : ℕ
• BitVec 📋 Init.Prelude
  (w : ℕ) : Type
• Fin 📋 Init.Prelude
  (n : ℕ) : Type
• instAddNat 📋 Init.Prelude
  : Add ℕ
• instDecidableEqNat 📋 Init.Prelude
  : DecidableEq ℕ
• instInhabitedNat 📋 Init.Prelude
  : Inhabited ℕ
• instLENat 📋 Init.Prelude
  : LE ℕ
• instLTNat 📋 Init.Prelude
  : LT ℕ
• instMinNat 📋 Init.Prelude
  : Min ℕ
• instMulNat 📋 Init.Prelude
  : Mul ℕ
• instNatPowNat 📋 Init.Prelude
  : NatPow ℕ
• instSubNat 📋 Init.Prelude
  : Sub ℕ
• Char.ofNat 📋 Init.Prelude
  (n : ℕ) : Char
• Char.utf8Size 📋 Init.Prelude
  (c : Char) : ℕ
• Nat.instDiv 📋 Init.Prelude
  : Div ℕ
• Nat.instMod 📋 Init.Prelude
  : Mod ℕ
• Nat.isValidChar 📋 Init.Prelude
  (n : ℕ) : Prop
• Nat.succ 📋 Init.Prelude
  (n : ℕ) : ℕ
• Substring.bsize 📋 Init.Prelude
  : Substring → ℕ
• UInt32.toNat 📋 Init.Prelude
  (n : UInt32) : ℕ
• Lean.Syntax.getNumArgs 📋 Init.Prelude
  (stx : Lean.Syntax) : ℕ
• String.Pos.byteIdx 📋 Init.Prelude
  (self : String.Pos) : ℕ
• String.Pos.mk 📋 Init.Prelude
  (byteIdx : ℕ) : String.Pos
• Lean.Macro.Context.currRecDepth 📋 Init.Prelude
  (self : Lean.Macro.Context) : ℕ
• Lean.Macro.Context.maxRecDepth 📋 Init.Prelude
  (self : Lean.Macro.Context) : ℕ
• Nat.pred 📋 Init.Prelude
  : ℕ → ℕ
• String.utf8ByteSize 📋 Init.Prelude
  : String → ℕ
• UInt8.ofNat 📋 Init.Prelude
  (n : ℕ) : UInt8
• OfNat 📋 Init.Prelude
  (α : Type u) : ℕ → Type u
• Nat.le 📋 Init.Prelude
  (n : ℕ) : ℕ → Prop
• Nat.lt 📋 Init.Prelude
  (n m : ℕ) : Prop
• Nat.modCore 📋 Init.Prelude
  (x y : ℕ) : ℕ
• Lean.Name.mkNum 📋 Init.Prelude
  (p : Lean.Name) (v : ℕ) : Lean.Name
• Lean.Name.num 📋 Init.Prelude
  (pre : Lean.Name) (i : ℕ) : Lean.Name
• Lean.ParserDescr.cat 📋 Init.Prelude
  (catName : Lean.Name) (rbp : ℕ) : Lean.ParserDescr
• Lean.Syntax.getArg 📋 Init.Prelude
  (stx : Lean.Syntax) (i : ℕ) : Lean.Syntax
• Lean.Syntax.matchesNull 📋 Init.Prelude
  (stx : Lean.Syntax) (n : ℕ) : Bool
• String.utf8ByteSize.go 📋 Init.Prelude
  : List Char → ℕ
• instDecidableEqBitVec 📋 Init.Prelude
  {w : ℕ} : DecidableEq (BitVec w)
• instDecidableEqFin 📋 Init.Prelude
  (n : ℕ) : DecidableEq (Fin n)
• instLEBitVec 📋 Init.Prelude
  {w : ℕ} : LE (BitVec w)
• instLEFin 📋 Init.Prelude
  {n : ℕ} : LE (Fin n)
• instLTBitVec 📋 Init.Prelude
  {w : ℕ} : LT (BitVec w)
• instLTFin 📋 Init.Prelude
  {n : ℕ} : LT (Fin n)
• instOfNatNat 📋 Init.Prelude
  (n : ℕ) : OfNat ℕ n
• BitVec.ofNat 📋 Init.Prelude
  (n i : ℕ) : BitVec n
• BitVec.toNat 📋 Init.Prelude
  {w : ℕ} (x : BitVec w) : ℕ
• Fin.val 📋 Init.Prelude
  {n : ℕ} (self : Fin n) : ℕ
• List.length 📋 Init.Prelude
  {α : Type u_1} : List α → ℕ
• List.lengthTR 📋 Init.Prelude
  {α : Type u_1} (as : List α) : ℕ
• Nat.add 📋 Init.Prelude
  : ℕ → ℕ → ℕ
• Nat.beq 📋 Init.Prelude
  : ℕ → ℕ → Bool
• Nat.ble 📋 Init.Prelude
  : ℕ → ℕ → Bool
• Nat.ctorElimType 📋 Init.Prelude
  {motive : ℕ → Sort u} (ctorIdx : ℕ) : Sort (max 1 u)
• Nat.div 📋 Init.Prelude
  (x y : ℕ) : ℕ
• Nat.mod 📋 Init.Prelude
  : ℕ → ℕ → ℕ
• Nat.mul 📋 Init.Prelude
  : ℕ → ℕ → ℕ
• Nat.pow 📋 Init.Prelude
  (m : ℕ) : ℕ → ℕ
• Nat.sub 📋 Init.Prelude
  : ℕ → ℕ → ℕ
• Lean.Name.ctorElimType 📋 Init.Prelude
  {motive : Lean.Name → Sort u} (ctorIdx : ℕ) : Sort (max 1 u)
• Lean.ParserDescr.ctorElimType 📋 Init.Prelude
  {motive : Lean.ParserDescr → Sort u} (ctorIdx : ℕ) : Sort (max 1 u)
• Lean.ParserDescr.node 📋 Init.Prelude
  (kind : Lean.SyntaxNodeKind) (prec : ℕ) (p : Lean.ParserDescr) : Lean.ParserDescr
• Lean.SourceInfo.ctorElimType 📋 Init.Prelude
  {motive : Lean.SourceInfo → Sort u} (ctorIdx : ℕ) : Sort (max 1 u)
• Lean.Syntax.ctorElimType 📋 Init.Prelude
  {motive_1 : Lean.Syntax → Sort u} (ctorIdx : ℕ) : Sort (max 1 u)
• Lean.Syntax.isNodeOf 📋 Init.Prelude
  (stx : Lean.Syntax) (k : Lean.SyntaxNodeKind) (n : ℕ) : Bool
• Nat.le.refl 📋 Init.Prelude
  {n : ℕ} : n.le n
• Lean.Macro.Exception.ctorElimType 📋 Init.Prelude
  {motive : Lean.Macro.Exception → Sort u} (ctorIdx : ℕ) : Sort (max 1 u)
• Lean.Syntax.Preresolved.ctorElimType 📋 Init.Prelude
  {motive : Lean.Syntax.Preresolved → Sort u} (ctorIdx : ℕ) : Sort (max 1 u)
• Array.emptyWithCapacity 📋 Init.Prelude
  {α : Type u} (c : ℕ) : Array α
• Array.mkEmpty 📋 Init.Prelude
  {α : Type u} (c : ℕ) : Array α
• Array.size 📋 Init.Prelude
  {α : Type u} (a : Array α) : ℕ
• Char.ofNatAux 📋 Init.Prelude
  (n : ℕ) (h : n.isValidChar) : Char
• List.lengthTRAux 📋 Init.Prelude
  {α : Type u_1} : List α → ℕ → ℕ
• Lean.ParserDescr.trailingNode 📋 Init.Prelude
  (kind : Lean.SyntaxNodeKind) (prec lhsPrec : ℕ) (p : Lean.ParserDescr) : Lean.ParserDescr
• instPowNat 📋 Init.Prelude
  {α : Type u_1} [NatPow α] : Pow α ℕ
• Array.getD 📋 Init.Prelude
  {α : Type u_1} (a : Array α) (i : ℕ) (v₀ : α) : α
• List.ctorElimType 📋 Init.Prelude
  {α : Type u} {motive : List α → Sort u_1} (ctorIdx : ℕ) : Sort (max 1 u_1 (imax (u + 1) (u + 1) u_1))
• Nat.le_refl 📋 Init.Prelude
  (n : ℕ) : n ≤ n
• NatPow.mk 📋 Init.Prelude
  {α : Type u} (pow : α → ℕ → α) : NatPow α
• NatPow.pow 📋 Init.Prelude
  {α : Type u} [self : NatPow α] : α → ℕ → α
• OfNat.mk 📋 Init.Prelude
  {α : Type u} {x✝ : ℕ} (ofNat : α) : OfNat α x✝
• OfNat.ofNat 📋 Init.Prelude
  {α : Type u} (x✝ : ℕ) [self : OfNat α x✝] : α
• Option.ctorElimType 📋 Init.Prelude
  {α : Type u} {motive : Option α → Sort u_1} (ctorIdx : ℕ) : Sort (max 1 u_1 (imax (u + 1) u_1))
• List.set 📋 Init.Prelude
  {α : Type u_1} (l : List α) (n : ℕ) (a : α) : List α
• Nat.ble_self_eq_true 📋 Init.Prelude
  (n : ℕ) : n.ble n = true
• Nat.le_succ 📋 Init.Prelude
  (n : ℕ) : n ≤ n.succ
• Nat.lt_irrefl 📋 Init.Prelude
  (n : ℕ) : ¬n < n
• Nat.lt_succ_self 📋 Init.Prelude
  (n : ℕ) : n < n.succ
• Nat.pred_le 📋 Init.Prelude
  (n : ℕ) : n.pred ≤ n
• UInt16.ofBitVec 📋 Init.Prelude
  (toBitVec : BitVec 16) : UInt16
• UInt16.toBitVec 📋 Init.Prelude
  (self : UInt16) : BitVec 16
• UInt32.ofBitVec 📋 Init.Prelude
  (toBitVec : BitVec 32) : UInt32
• UInt32.toBitVec 📋 Init.Prelude
  (self : UInt32) : BitVec 32
• UInt64.ofBitVec 📋 Init.Prelude
  (toBitVec : BitVec 64) : UInt64
• UInt64.toBitVec 📋 Init.Prelude
  (self : UInt64) : BitVec 64
• UInt8.ofBitVec 📋 Init.Prelude
  (toBitVec : BitVec 8) : UInt8
• UInt8.toBitVec 📋 Init.Prelude
  (self : UInt8) : BitVec 8
• Lean.Macro.Context.mk 📋 Init.Prelude
  (methods : Lean.Macro.MethodsRef) (quotContext : Lean.Name) (currMacroScope : Lean.MacroScope) (currRecDepth maxRecDepth : ℕ) (ref : Lean.Syntax) : Lean.Macro.Context
• Array.get!Internal 📋 Init.Prelude
  {α : Type u} [Inhabited α] (a : Array α) (i : ℕ) : α
• Array.get!InternalBorrowed 📋 Init.Prelude
  {α : Type u} [Inhabited α] (a : Array α) (i : ℕ) : α
• Except.ctorElimType 📋 Init.Prelude
  {ε : Type u} {α : Type v} {motive : Except ε α → Sort u_1} (ctorIdx : ℕ) : Sort (max 1 (imax (u + 1) u_1) (imax (v + 1) u_1))
• Nat.not_succ_le_self 📋 Init.Prelude
  (n : ℕ) : ¬n.succ ≤ n
• UInt16.ofNatLT 📋 Init.Prelude
  (n : ℕ) (h : n < UInt16.size) : UInt16
• UInt32.ofNatLT 📋 Init.Prelude
  (n : ℕ) (h : n < UInt32.size) : UInt32
• UInt64.ofNatLT 📋 Init.Prelude
  (n : ℕ) (h : n < UInt64.size) : UInt64
• UInt8.ofNatLT 📋 Init.Prelude
  (n : ℕ) (h : n < UInt8.size) : UInt8
• USize.ofNatLT 📋 Init.Prelude
  (n : ℕ) (h : n < USize.size) : USize
• Nat.decEq 📋 Init.Prelude
  (n m : ℕ) : Decidable (n = m)
• Fin.mk 📋 Init.Prelude
  {n : ℕ} (val : ℕ) (isLt : val < n) : Fin n
• USize.size_pos 📋 Init.Prelude
  : 0 < USize.size
• Array.appendCore.loop 📋 Init.Prelude
  {α : Type u} (bs : Array α) (i j : ℕ) (as : Array α) : Array α
• Array.extract.loop 📋 Init.Prelude
  {α : Type u_1} (as : Array α) (i j : ℕ) (bs : Array α) : Array α
• Nat.le.step 📋 Init.Prelude
  {n m : ℕ} : n.le m → n.le m.succ
• Nat.decLe 📋 Init.Prelude
  (n m : ℕ) : Decidable (n ≤ m)
• Nat.decLt 📋 Init.Prelude
  (n m : ℕ) : Decidable (n < m)
• Fin.isLt 📋 Init.Prelude
  {n : ℕ} (self : Fin n) : ↑self < n
• Nat.zero_le 📋 Init.Prelude
  (n : ℕ) : 0 ≤ n
• EStateM.Result.ctorElimType 📋 Init.Prelude
  {ε σ α : Type u} {motive : EStateM.Result ε σ α → Sort u_1} (ctorIdx : ℕ) : Sort (max 1 (imax (u + 1) (u + 1) u_1))
• BitVec.decEq 📋 Init.Prelude
  {w : ℕ} (x y : BitVec w) : Decidable (x = y)
• Nat.not_lt_zero 📋 Init.Prelude
  (n : ℕ) : ¬n < 0
• Nat.succ_pos 📋 Init.Prelude
  (n : ℕ) : 0 < n.succ
• Nat.zero_lt_succ 📋 Init.Prelude
  (n : ℕ) : 0 < n.succ
• Nat.le.below 📋 Init.Prelude
  {n : ℕ} {motive : (a : ℕ) → n.le a → Prop} {a✝ : ℕ} (t : n.le a✝) : Prop
• Nat.eq_of_beq_eq_true 📋 Init.Prelude
  {n m : ℕ} : n.beq m = true → n = m
• Nat.not_succ_le_zero 📋 Init.Prelude
  (n : ℕ) : n.succ ≤ 0 → False
• Nat.le.below.refl 📋 Init.Prelude
  {n : ℕ} {motive : (a : ℕ) → n.le a → Prop} : Nat.le.below ⋯
• instDecidableLeBitVec 📋 Init.Prelude
  {w : ℕ} (x y : BitVec w) : Decidable (x ≤ y)
• instDecidableLtBitVec 📋 Init.Prelude
  {w : ℕ} (x y : BitVec w) : Decidable (x < y)
• Fin.decLe 📋 Init.Prelude
  {n : ℕ} (a b : Fin n) : Decidable (a ≤ b)
• Fin.decLt 📋 Init.Prelude
  {n : ℕ} (a b : Fin n) : Decidable (a < b)
• Nat.le_of_lt_succ 📋 Init.Prelude
  {m n : ℕ} : m < n.succ → m ≤ n
• Nat.le_step 📋 Init.Prelude
  {n m : ℕ} (h : n ≤ m) : n ≤ m.succ
• Nat.le_succ_of_le 📋 Init.Prelude
  {n m : ℕ} (h : n ≤ m) : n ≤ m.succ
• Nat.lt_of_not_le 📋 Init.Prelude
  {a b : ℕ} (h : ¬a ≤ b) : b < a
• Nat.lt_or_ge 📋 Init.Prelude
  (n m : ℕ) : n < m ∨ n ≥ m
• Nat.lt_succ_of_le 📋 Init.Prelude
  {n m : ℕ} : n ≤ m → n < m.succ
• Nat.ne_of_beq_eq_false 📋 Init.Prelude
  {n m : ℕ} : n.beq m = false → ¬n = m
• Fin.Internal.ofNat 📋 Init.Prelude
  (n : ℕ) (hn : 0 < n) (a : ℕ) : Fin n
• Array.getInternal 📋 Init.Prelude
  {α : Type u} (a : Array α) (i : ℕ) (h : i < a.size) : α
• Array.getInternalBorrowed 📋 Init.Prelude
  {α : Type u} (a : Array α) (i : ℕ) (h : i < a.size) : α
• Nat.le_of_succ_le_succ 📋 Init.Prelude
  {n m : ℕ} : n.succ ≤ m.succ → n ≤ m
• Nat.pred_le_pred 📋 Init.Prelude
  {n m : ℕ} : n ≤ m → n.pred ≤ m.pred
• Nat.succ_le_succ 📋 Init.Prelude
  {n m : ℕ} : n ≤ m → n.succ ≤ m.succ
• Nat.ble_eq_true_of_le 📋 Init.Prelude
  {n m : ℕ} (h : n ≤ m) : n.ble m = true
• Nat.le_of_ble_eq_true 📋 Init.Prelude
  {n m : ℕ} (h : n.ble m = true) : n ≤ m
• Nat.ble_succ_eq_true 📋 Init.Prelude
  {n m : ℕ} : n.ble m = true → n.ble m.succ = true
• Nat.sub_le 📋 Init.Prelude
  (n m : ℕ) : n - m ≤ n
• Nat.le_antisymm 📋 Init.Prelude
  {n m : ℕ} (h₁ : n ≤ m) (h₂ : m ≤ n) : n = m
• Nat.not_le_of_not_ble_eq_true 📋 Init.Prelude
  {n m : ℕ} (h : ¬n.ble m = true) : ¬n ≤ m
• Array.extract 📋 Init.Prelude
  {α : Type u_1} (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : Array α
• Nat.eq_or_lt_of_le 📋 Init.Prelude
  {n m : ℕ} : n ≤ m → n = m ∨ n < m
• Nat.lt_of_le_of_ne 📋 Init.Prelude
  {n m : ℕ} (h₁ : n ≤ m) (h₂ : ¬n = m) : n < m
• USize.size_eq 📋 Init.Prelude
  : USize.size = 4294967296 ∨ USize.size = 18446744073709551616
• System.Platform.numBits_eq 📋 Init.Prelude
  : System.Platform.numBits = 32 ∨ System.Platform.numBits = 64
• Fin.eq_of_val_eq 📋 Init.Prelude
  {n : ℕ} {i j : Fin n} : ↑i = ↑j → i = j
• Fin.val_eq_of_eq 📋 Init.Prelude
  {n : ℕ} {i j : Fin n} (h : i = j) : ↑i = ↑j
• Nat.le_trans 📋 Init.Prelude
  {n m k : ℕ} : n ≤ m → m ≤ k → n ≤ k
• Nat.lt_add_one 📋 Init.Prelude
  (n : ℕ) : n < n + 1
• Nat.lt_of_le_of_lt 📋 Init.Prelude
  {n m k : ℕ} (h₁ : n ≤ m) (h₂ : m < k) : n < k
• Nat.lt_of_lt_of_le 📋 Init.Prelude
  {n m k : ℕ} : n < m → m ≤ k → n < k
• Nat.lt_trans 📋 Init.Prelude
  {n m k : ℕ} (h₁ : n < m) : m < k → n < k
• Nat.modCore_lt 📋 Init.Prelude
  {x y : ℕ} (hy : 0 < y) : x.modCore y < y
• Nat.div.go 📋 Init.Prelude
  (y : ℕ) (hy : 0 < y) (fuel x : ℕ) (hfuel : x < fuel) : ℕ
• Nat.modCore.go 📋 Init.Prelude
  (y : ℕ) (hy : 0 < y) (fuel x : ℕ) (hfuel : x < fuel) : ℕ
• noConfusion_of_Nat 📋 Init.Prelude
  {α : Sort u} (f : α → ℕ) {a b : α} (h : a = b) : Bool.rec False True ((f a).beq (f b))
• BitVec.ofFin 📋 Init.Prelude
  {w : ℕ} (toFin : Fin (2 ^ w)) : BitVec w
• BitVec.toFin 📋 Init.Prelude
  {w : ℕ} (self : BitVec w) : Fin (2 ^ w)
• System.Platform.getNumBits 📋 Init.Prelude
  : Unit → { n // n = 32 ∨ n = 64 }
• BitVec.ofNatLT 📋 Init.Prelude
  {w : ℕ} (i : ℕ) (p : i < 2 ^ w) : BitVec w
• Nat.mod_lt 📋 Init.Prelude
  (x : ℕ) {y : ℕ} (hy : 0 < y) : x % y < y
• Nat.succ_sub_succ_eq_sub 📋 Init.Prelude
  (n m : ℕ) : n.succ - m.succ = n - m
• Nat.le.brecOn 📋 Init.Prelude
  {n : ℕ} {motive : (a : ℕ) → n.le a → Prop} {a✝ : ℕ} (t : n.le a✝) (F_1 : ∀ (a : ℕ) (t : n.le a), Nat.le.below t → motive a t) : motive a✝ t
• Nat.modCoreGo_lt 📋 Init.Prelude
  {fuel y : ℕ} (hy : 0 < y) (x : ℕ) (hfuel : x < fuel) : Nat.modCore.go y hy fuel x hfuel < y
• Nat.le.below.step 📋 Init.Prelude
  {n : ℕ} {motive : (a : ℕ) → n.le a → Prop} {m : ℕ} (a✝ : n.le m) : Nat.le.below a✝ → motive m a✝ → Nat.le.below ⋯
• Nat.add_pos_right 📋 Init.Prelude
  {b : ℕ} (a : ℕ) (hb : 0 < b) : 0 < a + b
• Nat.div_rec_lemma 📋 Init.Prelude
  {x y : ℕ} : 0 < y ∧ y ≤ x → x - y < x
• Nat.pow_pos 📋 Init.Prelude
  {a n : ℕ} (h : 0 < a) : 0 < a ^ n
• Nat.sub_lt 📋 Init.Prelude
  {n m : ℕ} : 0 < n → 0 < m → n - m < n
• Nat.mul_pos 📋 Init.Prelude
  {n m : ℕ} (hn : 0 < n) (hm : 0 < m) : 0 < n * m
• Nat.div_rec_fuel_lemma 📋 Init.Prelude
  {x y fuel : ℕ} (hy : 0 < y) (hle : y ≤ x) (hfuel : x < fuel + 1) : x - y < fuel
• Lean.Parser.Category.toCtorIdx 📋 Init.Notation
  : Lean.Parser.Category → ℕ
• instSizeOfNat 📋 Init.SizeOf
  : SizeOf ℕ
• Lean.Name.sizeOf 📋 Init.SizeOf
  : Lean.Name → ℕ
• default.sizeOf 📋 Init.SizeOf
  (α : Sort u) : α → ℕ
• SizeOf.mk 📋 Init.SizeOf
  {α : Sort u} (sizeOf : α → ℕ) : SizeOf α
• SizeOf.sizeOf 📋 Init.SizeOf
  {α : Sort u} [self : SizeOf α] : α → ℕ
• sizeOf_nat 📋 Init.SizeOf
  (n : ℕ) : sizeOf n = n
• Bool.false.sizeOf_spec 📋 Init.SizeOf
  : sizeOf false = 1
• Bool.true.sizeOf_spec 📋 Init.SizeOf
  : sizeOf true = 1
• PUnit.unit.sizeOf_spec 📋 Init.SizeOf
  : sizeOf PUnit.unit = 1

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 0902274 serving mathlib revision 3540854