Loogle!

Result

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

• Lean.Syntax.missing 📋 Init.Prelude
  : Lean.Syntax
• Lean.Syntax.isMissing 📋 Init.Prelude
  : Lean.Syntax → Bool
• Lean.Parser.Tactic.SolveByElim.using_ 📋 Init.Tactics
  : Lean.ParserDescr
• Lean.Syntax.missing.sizeOf_spec 📋 Init.SizeOf
  : sizeOf Lean.Syntax.missing = 1
• Subsingleton 📋 Init.Core
  (α : Sort u) : Prop
• instSubsingletonEmpty 📋 Init.Core
  : Subsingleton Empty
• instSubsingletonPEmpty 📋 Init.Core
  : Subsingleton PEmpty.{u_1}
• instSubsingletonPUnit 📋 Init.Core
  : Subsingleton PUnit.{u_1}
• instSubsingleton 📋 Init.Core
  (p : Prop) : Subsingleton p
• Singleton 📋 Init.Core
  (α : outParam (Type u)) (β : Type v) : Type (max u v)
• instSubsingletonDecidable 📋 Init.Core
  (p : Prop) : Subsingleton (Decidable p)
• instSubsingletonSquash 📋 Init.Core
  {α : Sort u_1} : Subsingleton (Squash α)
• toBoolUsing 📋 Init.Core
  {p : Prop} (d : Decidable p) : Bool
• PUnit.subsingleton 📋 Init.Core
  (a b : PUnit.{u_1}) : a = b
• Singleton.mk 📋 Init.Core
  {α : outParam (Type u)} {β : Type v} (singleton : α → β) : Singleton α β
• Singleton.singleton 📋 Init.Core
  {α : outParam (Type u)} {β : Type v} [self : Singleton α β] : α → β
• Subsingleton.allEq 📋 Init.Core
  {α : Sort u} [self : Subsingleton α] (a b : α) : a = b
• Subsingleton.elim 📋 Init.Core
  {α : Sort u} [h : Subsingleton α] (a b : α) : a = b
• Subsingleton.intro 📋 Init.Core
  {α : Sort u} (allEq : ∀ (a b : α), a = b) : Subsingleton α
• instSubsingletonProd 📋 Init.Core
  {α : Type u_1} {β : Type u_2} [Subsingleton α] [Subsingleton β] : Subsingleton (α × β)
• ofBoolUsing_eq_true 📋 Init.Core
  {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p
• of_toBoolUsing_eq_true 📋 Init.Core
  {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p
• toBoolUsing_eq_true 📋 Init.Core
  {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true
• LawfulSingleton 📋 Init.Core
  (α : Type u) (β : Type v) [EmptyCollection β] [Insert α β] [Singleton α β] : Prop
• eq_iff_true_of_subsingleton 📋 Init.Core
  {α : Sort u_1} [Subsingleton α] (x y : α) : x = y ↔ True
• ofBoolUsing_eq_false 📋 Init.Core
  {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬p
• of_toBoolUsing_eq_false 📋 Init.Core
  {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬p
• Pi.instSubsingleton 📋 Init.Core
  {α : Sort u} {β : α → Sort v} [∀ (a : α), Subsingleton (β a)] : Subsingleton ((a : α) → β a)
• Relation.TransGen.single 📋 Init.Core
  {α : Sort u} {r : α → α → Prop} {a b : α} : r a b → Relation.TransGen r a b
• Subsingleton.helim 📋 Init.Core
  {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : a ≍ b
• Quotient.recOnSubsingleton 📋 Init.Core
  {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} [h : ∀ (a : α), Subsingleton (motive ⟦a⟧)] (q : Quotient s) (f : (a : α) → motive ⟦a⟧) : motive q
• recSubsingleton 📋 Init.Core
  {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] : Subsingleton (Decidable.casesOn h h₂ h₁)
• Quot.recOnSubsingleton 📋 Init.Core
  {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) : motive q
• Relation.TransGen.below.single 📋 Init.Core
  {α : Sort u} {r : α → α → Prop} {a : α} {motive✝ : (a_1 : α) → Relation.TransGen r a a_1 → Prop} {b : α} (a✝ : r a b) : ⋯.below
• LawfulSingleton.insert_empty_eq 📋 Init.Core
  {α : Type u} {β : Type v} {inst✝ : EmptyCollection β} {inst✝¹ : Insert α β} {inst✝² : Singleton α β} [self : LawfulSingleton α β] (x : α) : insert x ∅ = {x}
• LawfulSingleton.insert_emptyc_eq 📋 Init.Core
  {β : Type u_1} {α : Type u_2} [EmptyCollection β] [Insert α β] [Singleton α β] [LawfulSingleton α β] (x : α) : insert x ∅ = {x}
• LawfulSingleton.mk 📋 Init.Core
  {α : Type u} {β : Type v} [EmptyCollection β] [Insert α β] [Singleton α β] (insert_empty_eq : ∀ (x : α), insert x ∅ = {x}) : LawfulSingleton α β
• Quotient.recOnSubsingleton₂ 📋 Init.Core
  {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Sort uC} [s : ∀ (a : α) (b : β), Subsingleton (motive ⟦a⟧ ⟦b⟧)] (q₁ : Quotient s₁) (q₂ : Quotient s₂) (g : (a : α) → (b : β) → motive ⟦a⟧ ⟦b⟧) : motive q₁ q₂
• instSubsingletonStateM 📋 Init.Control.State
  {σ α : Type u_1} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ α)
• Lean.Meta.Simp.Config.singlePass 📋 Init.MetaTypes
  (self : Lean.Meta.Simp.Config) : Bool
• tacticDecreasing_tactic 📋 Init.WFTactics
  : Lean.ParserDescr
• tacticDecreasing_trivial 📋 Init.WFTactics
  : Lean.ParserDescr
• tacticDecreasing_trivial_pre_omega 📋 Init.WFTactics
  : Lean.ParserDescr
• tacticDecreasing_with_ 📋 Init.WFTactics
  : Lean.ParserDescr
• List.singleton 📋 Init.Data.List.Basic
  {α : Type u} (a : α) : List α
• List.IsInfix 📋 Init.Data.List.Basic
  {α : Type u} (l₁ l₂ : List α) : Prop
• List.dropLast_single 📋 Init.Data.List.Basic
  {α✝ : Type u_1} {x : α✝} : [x].dropLast = []
• List.dropLast_singleton 📋 Init.Data.List.Basic
  {α✝ : Type u_1} {x : α✝} : [x].dropLast = []
• List.length_singleton 📋 Init.Data.List.Basic
  {α : Type u} {a : α} : [a].length = 1
• List.intersperse_single 📋 Init.Data.List.Basic
  {α : Type u} {x sep : α} : List.intersperse sep [x] = [x]
• String.singleton 📋 Init.Data.String.Basic
  (c : Char) : String
• String.length_singleton 📋 Init.Data.String.Basic
  (c : Char) : (String.singleton c).length = 1
• String.singleton_eq 📋 Init.Data.String.Basic
  (c : Char) : String.singleton c = { data := [c] }
• String.data_singleton 📋 Init.Data.String.Basic
  (c : Char) : (String.singleton c).data = [c]
• String.isInt 📋 Init.Data.ToString.Basic
  (s : String) : Bool
• Array.singleton 📋 Init.Data.Array.Basic
  {α : Type u} (v : α) : Array α
• Lean.Name.isInaccessibleUserName 📋 Init.Meta
  : Lean.Name → Bool
• Lean.Syntax.isInterpolatedStrLit? 📋 Init.Meta
  (stx : Lean.Syntax) : Option String
• Lean.Syntax.SepArray.ofElemsUsingRef 📋 Init.Meta
  {m : Type → Type} [Monad m] [Lean.MonadRef m] {sep : String} (elems : Array Lean.Syntax) : m (Lean.Syntax.SepArray sep)
• Lean.Parser.Tactic.Conv.occsIndexed 📋 Init.Conv
  : Lean.ParserDescr
• Lean.singletonUnexpander 📋 Init.NotationExtra
  : Lean.PrettyPrinter.Unexpander
• Classical.epsilon_singleton 📋 Init.Classical
  {α : Sort u} (x : α) : (Classical.epsilon fun y => y = x) = x
• List.mem_singleton_self 📋 Init.Data.List.Lemmas
  {α : Type u_1} (a : α) : a ∈ [a]
• List.getLast?_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} : [a].getLast? = some a
• List.head?_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} : [a].head? = some a
• List.head_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} : [a].head ⋯ = a
• List.flatten_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} : [l].flatten = l
• List.flatMap_singleton' 📋 Init.Data.List.Lemmas
  {α : Type u_1} (l : List α) : List.flatMap (fun x => [x]) l = l
• List.eq_of_mem_singleton 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {b a : α✝} : a ∈ [b] → a = b
• List.flatMap_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} (f : α → List β) (x : α) : List.flatMap f [x] = f x
• List.mem_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a b : α} : a ∈ [b] ↔ a = b
• List.flatten_replicate_singleton 📋 Init.Data.List.Lemmas
  {n : ℕ} {α✝ : Type u_1} {a : α✝} : (List.replicate n [a]).flatten = List.replicate n a
• List.singleton_inj 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a b : α} : [a] = [b] ↔ a = b
• List.forall_mem_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {p : α → Prop} {a : α} : (∀ x ∈ [a], p x) ↔ p a
• List.getLast_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} (h : [a] ≠ []) : [a].getLast h = a
• List.map_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} : List.map f [a] = [f a]
• List.singleton_append 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {x : α✝} {l : List α✝} : [x] ++ l = x :: l
• List.getElem_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {i : ℕ} (h : i < 1) : [a][i] = a
• List.map_eq_singleton_iff 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {b : β} : List.map f l = [b] ↔ ∃ a, l = [a] ∧ f a = b
• List.replace_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} [BEq α] {a b c : α} : [a].replace b c = [if (b == a) = true then c else a]
• List.getElem?_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {i : ℕ} : [a][i]? = if i = 0 then some a else none
• List.append_eq_singleton_iff 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {a b : List α✝} {x : α✝} : a ++ b = [x] ↔ a = [] ∧ b = [x] ∨ a = [x] ∧ b = []
• List.singleton_eq_append_iff 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {x : α✝} {a b : List α✝} : [x] = a ++ b ↔ a = [] ∧ b = [x] ∨ a = [x] ∧ b = []
• List.flatten_eq_singleton_iff 📋 Init.Data.List.Lemmas
  {α : Type u_1} {xs : List (List α)} {y : α} : xs.flatten = [y] ↔ ∃ as bs, xs = as ++ [y] :: bs ∧ (∀ l ∈ as, l = []) ∧ ∀ l ∈ bs, l = []
• List.singleton_eq_flatten_iff 📋 Init.Data.List.Lemmas
  {α : Type u_1} {xs : List (List α)} {y : α} : [y] = xs.flatten ↔ ∃ as bs, xs = as ++ [y] :: bs ∧ (∀ l ∈ as, l = []) ∧ ∀ l ∈ bs, l = []
• BitVec.instSubsingletonOfNatNat 📋 Init.Data.BitVec.Basic
  : Subsingleton (BitVec 0)
• Fin.subsingleton_one 📋 Init.Data.Fin.Lemmas
  : Subsingleton (Fin 1)
• Fin.subsingleton_zero 📋 Init.Data.Fin.Lemmas
  : Subsingleton (Fin 0)
• Fin.subsingleton_iff_le_one 📋 Init.Data.Fin.Lemmas
  {n : ℕ} : Subsingleton (Fin n) ↔ n ≤ 1
• List.IsInfix.sublist 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+: l₂ → l₁.Sublist l₂
• List.IsPrefix.isInfix 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <+: l₂ → l₁ <:+: l₂
• List.IsSuffix.isInfix 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+ l₂ → l₁ <:+: l₂
• List.IsInfix.subset 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} (hl : l₁ <:+: l₂) : l₁ ⊆ l₂
• List.IsInfix.reverse 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+: l₂ → l₁.reverse <:+: l₂.reverse
• List.IsInfix.length_le 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+: l₂) : l₁.length ≤ l₂.length
• List.IsInfix.trans 📋 Init.Data.List.Sublist
  {α : Type u_1} {l₁ l₂ l₃ : List α} : l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃
• List.singleton_sublist 📋 Init.Data.List.Sublist
  {α : Type u_1} {a : α} {l : List α} : [a].Sublist l ↔ a ∈ l
• List.IsInfix.filter 📋 Init.Data.List.Sublist
  {α : Type u_1} (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : List.filter p l₁ <:+: List.filter p l₂
• List.IsInfix.ne_nil 📋 Init.Data.List.Sublist
  {α : Type u_1} {xs ys : List α} (h : xs <:+: ys) (hx : xs ≠ []) : ys ≠ []
• List.IsInfix.eq_of_length 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+: l₂) : l₁.length = l₂.length → l₁ = l₂
• List.IsInfix.eq_of_length_le 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+: l₂) : l₂.length ≤ l₁.length → l₁ = l₂
• List.IsInfix.map 📋 Init.Data.List.Sublist
  {α : Type u_1} {β : Type u_2} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : List.map f l₁ <:+: List.map f l₂
• List.IsInfix.filterMap 📋 Init.Data.List.Sublist
  {α : Type u_1} {β : Type u_2} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : List.filterMap f l₁ <:+: List.filterMap f l₂
• List.IsInfix.mem 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ : List α✝} {a : α✝} {l₂ : List α✝} (hx : a ∈ l₁) (hl : l₁ <:+: l₂) : a ∈ l₂
• List.isInfix_replicate_iff 📋 Init.Data.List.Sublist
  {α : Type u_1} {n : ℕ} {a : α} {l : List α} : l <:+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a
• List.isInfix_filter_iff 📋 Init.Data.List.Sublist
  {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} : l₂ <:+: List.filter p l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = List.filter p l
• List.isInfix_map_iff 📋 Init.Data.List.Sublist
  {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : List α} {l₂ : List β} : l₂ <:+: List.map f l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = List.map f l
• List.isInfix_filterMap_iff 📋 Init.Data.List.Sublist
  {α : Type u_1} {β : Type u_2} {f : α → Option β} {l₁ : List α} {l₂ : List β} : l₂ <:+: List.filterMap f l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = List.filterMap f l
• List.IsInfix.eq_1 📋 Init.Data.List.Sublist
  {α : Type u} (l₁ l₂ : List α) : (l₁ <:+: l₂) = ∃ s t, s ++ l₁ ++ t = l₂
• List.IsInfix.countP_le 📋 Init.Data.List.Count
  {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (s : l₁ <:+: l₂) : List.countP p l₁ ≤ List.countP p l₂
• List.count_singleton_self 📋 Init.Data.List.Count
  {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} : List.count a [a] = 1
• List.IsInfix.count_le 📋 Init.Data.List.Count
  {α : Type u_1} [BEq α] {l₁ l₂ : List α} (a : α) (h : l₁ <:+: l₂) : List.count a l₁ ≤ List.count a l₂
• List.countP_singleton 📋 Init.Data.List.Count
  {α : Type u_1} {p : α → Bool} {a : α} : List.countP p [a] = if p a = true then 1 else 0
• List.count_singleton 📋 Init.Data.List.Count
  {α : Type u_1} [BEq α] {a b : α} : List.count a [b] = if (b == a) = true then 1 else 0
• List.pairwise_singleton 📋 Init.Data.List.Pairwise
  {α : Type u_1} (R : α → α → Prop) (a : α) : List.Pairwise R [a]
• List.findSome?_singleton 📋 Init.Data.List.Impl
  {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {a : α} : List.findSome? f [a] = f a
• List.find?_singleton 📋 Init.Data.List.Impl
  {α : Type u_1} {p : α → Bool} {a : α} : List.find? p [a] = if p a = true then some a else none
• List.IsInfix.find?_eq_none 📋 Init.Data.List.Find
  {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+: l₂) : List.find? p l₂ = none → List.find? p l₁ = none
• List.IsInfix.findIdx?_eq_none 📋 Init.Data.List.Find
  {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+: l₂) : List.findIdx? p l₂ = none → List.findIdx? p l₁ = none
• List.IsInfix.findSome?_eq_none 📋 Init.Data.List.Find
  {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <:+: l₂) : List.findSome? f l₂ = none → List.findSome? f l₁ = none
• List.findIdx_singleton 📋 Init.Data.List.Find
  {α : Type u_1} {a : α} {p : α → Bool} : List.findIdx p [a] = if p a = true then 0 else 1
• List.findIdx?_singleton 📋 Init.Data.List.Find
  {α : Type u_1} {a : α} {p : α → Bool} : List.findIdx? p [a] = if p a = true then some 0 else none
• List.idxOf?_singleton 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] {a b : α} : List.idxOf? b [a] = if (a == b) = true then some 0 else none
• List.IsInfix.lookup_eq_none 📋 Init.Data.List.Find
  {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)} (h : l₁ <:+: l₂) : List.lookup k l₂ = none → List.lookup k l₁ = none
• List.lookup_singleton 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] [LawfulBEq α] {c a b : α} : List.lookup c [(a, b)] = if (c == a) = true then some b else none
• List.findFinIdx?_singleton 📋 Init.Data.List.Find
  {α : Type u_1} {a : α} {p : α → Bool} : List.findFinIdx? p [a] = if p a = true then some ⟨0, List.findFinIdx?_singleton._proof_1⟩ else none
• Std.Iterators.IterM.IsPlausibleIndirectSuccessorOf.single 📋 Init.Data.Iterators.Basic
  {α β : Type w} {m : Type w → Type w'} [Std.Iterators.Iterator α m β] {it' it : Std.IterM m β} (h : it'.IsPlausibleSuccessorOf it) : it'.IsPlausibleIndirectSuccessorOf it
• List.toArray_singleton 📋 Init.Data.List.ToArray
  {α : Type u_1} (a : α) : (List.singleton a).toArray = Array.singleton a
• Array.singleton_def 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {v : α} : Array.singleton v = #[v]
• Array.mem_singleton_self 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (a : α) : a ∈ #[a]
• Array.back_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {a : α} : #[a].back ⋯ = a
• Array.flatMap_singleton' 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (xs : Array α) : Array.flatMap (fun x => #[x]) xs = xs
• Array.flatten_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xs : Array α} : #[xs].flatten = xs
• Array.singleton_eq_toArray_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {a : α} : #[a] = #[a]
• Array.eq_of_mem_singleton 📋 Init.Data.Array.Lemmas
  {α✝ : Type u_1} {b a : α✝} (h : a ∈ #[b]) : a = b
• Array.flatMap_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → Array β} {x : α} : Array.flatMap f #[x] = f x
• Array.mem_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {a b : α} : a ∈ #[b] ↔ a = b
• Array.flatten_mkArray_singleton 📋 Init.Data.Array.Lemmas
  {n : ℕ} {α✝ : Type u_1} {a : α✝} : (Array.replicate n #[a]).flatten = Array.replicate n a
• Array.flatten_replicate_singleton 📋 Init.Data.Array.Lemmas
  {n : ℕ} {α✝ : Type u_1} {a : α✝} : (Array.replicate n #[a]).flatten = Array.replicate n a
• Array.forall_mem_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {p : α → Prop} {a : α} : (∀ x ∈ #[a], p x) ↔ p a
• Array.singleton_inj 📋 Init.Data.Array.Lemmas
  {α✝ : Type u_1} {a b : α✝} : #[a] = #[b] ↔ a = b
• Array.map_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} : Array.map f #[a] = #[f a]
• Array.append_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {a : α} {as : Array α} : as ++ #[a] = as.push a
• Array.push_eq_append_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {as : Array α} {x : α} : as.push x = as ++ #[x]
• Array.getElem_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {a : α} {i : ℕ} (h : i < 1) : #[a][i] = a
• Array.map_eq_singleton_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {b : β} : Array.map f xs = #[b] ↔ ∃ a, xs = #[a] ∧ f a = b
• Array.replace_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} [BEq α] {a b c : α} : #[a].replace b c = #[if (a == b) = true then c else a]
• Array.getElem?_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {a : α} {i : ℕ} : #[a][i]? = if i = 0 then some a else none
• Array.append_singleton_assoc 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {a : α} {xs ys : Array α} : xs ++ (#[a] ++ ys) = xs.push a ++ ys
• Array.append_eq_singleton_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xs ys : Array α} {x : α} : xs ++ ys = #[x] ↔ xs = #[] ∧ ys = #[x] ∨ xs = #[x] ∧ ys = #[]
• Array.singleton_eq_append_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xs ys : Array α} {x : α} : #[x] = xs ++ ys ↔ xs = #[] ∧ ys = #[x] ∨ xs = #[x] ∧ ys = #[]
• List.IsInfix.le_countP 📋 Init.Data.List.Nat.Count
  {α✝ : Type u_1} {l₁ l₂ : List α✝} {p : α✝ → Bool} (s : l₁ <:+: l₂) : List.countP p l₂ - (l₂.length - l₁.length) ≤ List.countP p l₁
• List.IsInfix.le_count 📋 Init.Data.List.Nat.Count
  {α : Type u_1} [BEq α] {l₁ l₂ : List α} (s : l₁ <:+: l₂) (a : α) : List.count a l₂ - (l₂.length - l₁.length) ≤ List.count a l₁
• Array.count_singleton_self 📋 Init.Data.Array.Count
  {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} : Array.count a #[a] = 1
• Array.countP_singleton 📋 Init.Data.Array.Count
  {α : Type u_1} {p : α → Bool} {a : α} : Array.countP p #[a] = if p a = true then 1 else 0
• Array.count_singleton 📋 Init.Data.Array.Count
  {α : Type u_1} [BEq α] {a b : α} : Array.count a #[b] = if (b == a) = true then 1 else 0
• List.zipIdx_singleton 📋 Init.Data.List.Nat.Range
  {α : Type u_1} {x : α} {k : ℕ} : [x].zipIdx k = [(x, k)]
• List.range'_eq_singleton_iff 📋 Init.Data.List.Nat.Range
  {s n a : ℕ} : List.range' s n = [a] ↔ s = a ∧ n = 1
• Option.toList_eq_singleton_iff 📋 Init.Data.Option.List
  {α : Type u_1} {a : α} {o : Option α} : o.toList = [a] ↔ o = some a
• Option.toArray_eq_singleton_iff 📋 Init.Data.Option.Array
  {α : Type u_1} {a : α} {o : Option α} : o.toArray = #[a] ↔ o = some a
• Option.instSubsingletonSubtypeEqSome 📋 Init.Data.Option.Attach
  {α : Type u_1} {o : Option α} : Subsingleton { x // o = some x }
• List.mapIdx_singleton 📋 Init.Data.List.MapIdx
  {α : Type u_1} {α✝ : Type u_2} {f : ℕ → α → α✝} {a : α} : List.mapIdx f [a] = [f 0 a]
• List.mapFinIdx_singleton 📋 Init.Data.List.MapIdx
  {α : Type u_1} {β : Type u_2} {a : α} {f : (i : ℕ) → α → i < 1 → β} : [a].mapFinIdx f = [f 0 a List.mapFinIdx_singleton._proof_1]
• List.mapIdx_eq_singleton_iff 📋 Init.Data.List.MapIdx
  {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β} {b : β} : List.mapIdx f l = [b] ↔ ∃ a, l = [a] ∧ f 0 a = b
• List.mapFinIdx_eq_singleton_iff 📋 Init.Data.List.MapIdx
  {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : ℕ) → α → i < l.length → β} {b : β} : l.mapFinIdx f = [b] ↔ ∃ a, ∃ (w : l = [a]), f 0 a ⋯ = b
• Array.mapIdx_singleton 📋 Init.Data.Array.MapIdx
  {α : Type u_1} {α✝ : Type u_2} {f : ℕ → α → α✝} {a : α} : Array.mapIdx f #[a] = #[f 0 a]
• Array.mapFinIdx_singleton 📋 Init.Data.Array.MapIdx
  {α : Type u_1} {β : Type u_2} {a : α} {f : (i : ℕ) → α → i < 1 → β} : #[a].mapFinIdx f = #[f 0 a Array.mapFinIdx_singleton._proof_1]
• Array.mapIdx_eq_singleton_iff 📋 Init.Data.Array.MapIdx
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β} {b : β} : Array.mapIdx f xs = #[b] ↔ ∃ a, xs = #[a] ∧ f 0 a = b
• Array.mapFinIdx_eq_singleton_iff 📋 Init.Data.Array.MapIdx
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β} {b : β} : xs.mapFinIdx f = #[b] ↔ ∃ a, ∃ (w : xs = #[a]), f 0 a ⋯ = b
• Array.range'_eq_singleton_iff 📋 Init.Data.Array.Range
  {s n a : ℕ} : Array.range' s n = #[a] ↔ s = a ∧ n = 1
• Array.zipIdx_singleton 📋 Init.Data.Array.Range
  {α : Type u_1} {x : α} {k : ℕ} : #[x].zipIdx k = #[(x, k)]
• Vector.singleton 📋 Init.Data.Vector.Basic
  {α : Type u_1} (v : α) : Vector α 1
• List.isInfix_iff 📋 Init.Data.List.Nat.Sublist
  {α : Type u_1} {l₁ l₂ : List α} : l₁ <:+: l₂ ↔ ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ (i : ℕ) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
• List.singleton_perm_singleton 📋 Init.Data.List.Perm
  {α : Type u_1} {a b : α} : [a].Perm [b] ↔ a = b
• List.Perm.eq_singleton 📋 Init.Data.List.Perm
  {α✝ : Type u_1} {l : List α✝} {a : α✝} (h : l.Perm [a]) : l = [a]
• List.Perm.singleton_eq 📋 Init.Data.List.Perm
  {α✝ : Type u_1} {a : α✝} {l : List α✝} (h : [a].Perm l) : [a] = l
• List.perm_singleton 📋 Init.Data.List.Perm
  {α : Type u_1} {a : α} {l : List α} : l.Perm [a] ↔ l = [a]
• List.singleton_perm 📋 Init.Data.List.Perm
  {α : Type u_1} {a : α} {l : List α} : [a].Perm l ↔ [a] = l
• List.perm_append_singleton 📋 Init.Data.List.Perm
  {α : Type u_1} (a : α) (l : List α) : (l ++ [a]).Perm (a :: l)
• List.mergeSort_singleton 📋 Init.Data.List.Sort.Lemmas
  {α : Type u_1} {r : α → α → Bool} (a : α) : [a].mergeSort r = [a]
• Lean.Grind.IntInterval.sint 📋 Init.Grind.ToInt
  (n : ℕ) : Lean.Grind.IntInterval
• Lean.Grind.instToIntISizeSintNumBits 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
• Lean.Grind.instAddISizeSintNumBits 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.Add ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
• Lean.Grind.instLEISizeSintNumBits 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.LE ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
• Lean.Grind.instLTISizeSintNumBits 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.LT ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
• Lean.Grind.instMulISizeSintNumBits 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.Mul ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
• Lean.Grind.instOfNatISizeSintNumBits 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.OfNat ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
• Lean.Grind.instToIntInt16SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt Int16 (Lean.Grind.IntInterval.sint 16)
• Lean.Grind.instToIntInt32SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt Int32 (Lean.Grind.IntInterval.sint 32)
• Lean.Grind.instToIntInt64SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt Int64 (Lean.Grind.IntInterval.sint 64)
• Lean.Grind.instToIntInt8SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt Int8 (Lean.Grind.IntInterval.sint 8)
• Lean.Grind.instZeroISizeSintNumBits 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.Zero ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
• Lean.Grind.instAddInt16SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.Add Int16 (Lean.Grind.IntInterval.sint 16)
• Lean.Grind.instAddInt32SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.Add Int32 (Lean.Grind.IntInterval.sint 32)
• Lean.Grind.instAddInt64SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.Add Int64 (Lean.Grind.IntInterval.sint 64)
• Lean.Grind.instAddInt8SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.Add Int8 (Lean.Grind.IntInterval.sint 8)
• Lean.Grind.instLEInt16SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.LE Int16 (Lean.Grind.IntInterval.sint 16)
• Lean.Grind.instLEInt32SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.LE Int32 (Lean.Grind.IntInterval.sint 32)
• Lean.Grind.instLEInt64SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.LE Int64 (Lean.Grind.IntInterval.sint 64)
• Lean.Grind.instLEInt8SintOfNatNat 📋 Init.GrindInstances.ToInt
  : Lean.Grind.ToInt.LE Int8 (Lean.Grind.IntInterval.sint 8)

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 06e7f72 serving mathlib revision e128198