Loogle!

Result

Found 293 declarations mentioning List and Fin. Of these, only the first 200 are shown.

• List.get 📋 Init.Prelude
  {α : Type u} (as : List α) : Fin as.length → α
• List.findFinIdx? 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (l : List α) : Option (Fin l.length)
• List.finIdxOf? 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (a : α) (l : List α) : Option (Fin l.length)
• List.findFinIdx?.go 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (l l' : List α) (i : ℕ) (h : l'.length + i = l.length) : Option (Fin l.length)
• List.sizeOf_get 📋 Init.Data.List.BasicAux
  {α : Type u_1} [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as
• List.get_mem 📋 Init.Data.List.Lemmas
  {α : Type u_1} (l : List α) (n : Fin l.length) : l.get n ∈ l
• List.get_cons_succ' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {as : List α} {i : Fin as.length} : (a :: as).get i.succ = as.get i
• List.get_of_mem 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {l : List α} (h : a ∈ l) : ∃ n, l.get n = a
• List.mem_iff_get 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ n, l.get n = a
• List.get_eq_getElem 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} {i : Fin l.length} : l.get i = l[↑i]
• List.get_of_eq 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l l' : List α} (h : l = l') (i : Fin l.length) : l.get i = l'.get ⟨↑i, ⋯⟩
• List.get_cons_zero 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {a : α✝} {l : List α✝} : (a :: l).get 0 = a
• List.ofFn 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} (f : Fin n → α) : List α
• List.ofFnM 📋 Init.Data.List.OfFn
  {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [Monad m] (f : Fin n → m α) : m (List α)
• List.ofFn_zero 📋 Init.Data.List.OfFn
  {α : Type u_1} {f : Fin 0 → α} : List.ofFn f = []
• List.ofFn_eq_nil_iff 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {f : Fin n → α} : List.ofFn f = [] ↔ n = 0
• List.idRun_ofFnM 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {f : Fin n → Id α} : (List.ofFnM f).run = List.ofFn fun i => (f i).run
• List.mem_ofFn 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} {f : Fin n → α} {a : α} : a ∈ List.ofFn f ↔ ∃ i, f i = a
• List.map_ofFn 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {β : Type u_2} {f : Fin n → α} {g : α → β} : List.map g (List.ofFn f) = List.ofFn (g ∘ f)
• Fin.foldr_cons_eq_append 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {f : Fin n → α} {xs : List α} : Fin.foldr n (fun i xs => f i :: xs) xs = List.ofFn f ++ xs
• List.ofFnM_zero 📋 Init.Data.List.OfFn
  {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin 0 → m α} : List.ofFnM f = pure []
• Fin.foldl_cons_eq_append 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {f : Fin n → α} {xs : List α} : Fin.foldl n (fun xs i => f i :: xs) xs = (List.ofFn f).reverse ++ xs
• List.ofFn_getElem 📋 Init.Data.List.OfFn
  {α : Type u_1} {xs : List α} : (List.ofFn fun i => xs[↑i]) = xs
• List.ofFnM_pure 📋 Init.Data.List.OfFn
  {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {n : ℕ} {f : Fin n → α} : (List.ofFnM fun i => pure (f i)) = pure (List.ofFn f)
• List.ofFnM_pure_comp 📋 Init.Data.List.OfFn
  {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {n : ℕ} {f : Fin n → α} : List.ofFnM (pure ∘ f) = pure (List.ofFn f)
• List.getElem_ofFn 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {i : ℕ} {f : Fin n → α} (h : i < (List.ofFn f).length) : (List.ofFn f)[i] = f ⟨i, ⋯⟩
• List.getElem?_ofFn 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {i : ℕ} {f : Fin n → α} : (List.ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none
• List.ofFn_succ_last 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} {f : Fin (n + 1) → α} : List.ofFn f = (List.ofFn fun i => f i.castSucc) ++ [f (Fin.last n)]
• List.ofFn_add 📋 Init.Data.List.OfFn
  {α : Type u_1} {n m : ℕ} {f : Fin (n + m) → α} : List.ofFn f = (List.ofFn fun i => f (Fin.castLE ⋯ i)) ++ List.ofFn fun i => f (Fin.natAdd n i)
• List.head_ofFn 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} {f : Fin n → α} (h : List.ofFn f ≠ []) : (List.ofFn f).head h = f ⟨0, ⋯⟩
• List.getLast_ofFn 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} {f : Fin n → α} (h : List.ofFn f ≠ []) : (List.ofFn f).getLast h = f ⟨n - 1, ⋯⟩
• List.ofFn_succ 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} {f : Fin (n + 1) → α} : List.ofFn f = f 0 :: List.ofFn fun i => f i.succ
• List.ofFnM_succ_last 📋 Init.Data.List.OfFn
  {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} : List.ofFnM f = do let as ← List.ofFnM fun i => f i.castSucc let a ← f (Fin.last n) pure (as ++ [a])
• List.ofFnM_add 📋 Init.Data.List.OfFn
  {k : ℕ} {α : Type u_1} {n : ℕ} {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} : List.ofFnM f = do let as ← List.ofFnM fun i => f (Fin.castLE ⋯ i) let bs ← List.ofFnM fun i => f (Fin.natAdd n i) pure (as ++ bs)
• List.finRange 📋 Init.Data.List.FinRange
  (n : ℕ) : List (Fin n)
• List.mem_finRange 📋 Init.Data.List.FinRange
  {n : ℕ} (x : Fin n) : x ∈ List.finRange n
• List.finRange_reverse 📋 Init.Data.List.FinRange
  {n : ℕ} : (List.finRange n).reverse = List.map Fin.rev (List.finRange n)
• List.finRange_zero 📋 Init.Data.List.FinRange
  : List.finRange 0 = []
• List.getElem_finRange 📋 Init.Data.List.FinRange
  {n i : ℕ} (h : i < (List.finRange n).length) : (List.finRange n)[i] = Fin.cast ⋯ ⟨i, h⟩
• List.finRange_succ 📋 Init.Data.List.FinRange
  {n : ℕ} : List.finRange (n + 1) = 0 :: List.map Fin.succ (List.finRange n)
• List.ofFnM_succ 📋 Init.Data.List.FinRange
  {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} : List.ofFnM f = do let a ← f 0 let as ← List.ofFnM fun i => f i.succ pure (a :: as)
• List.finRange_succ_last 📋 Init.Data.List.FinRange
  {n : ℕ} : List.finRange (n + 1) = List.map Fin.castSucc (List.finRange n) ++ [Fin.last n]
• List.isSome_findFinIdx? 📋 Init.Data.List.Find
  {α : Type u_1} {l : List α} {p : α → Bool} : (List.findFinIdx? p l).isSome = l.any p
• List.isSome_finIdxOf? 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] [PartialEquivBEq α] {l : List α} {a : α} : (List.finIdxOf? a l).isSome = l.contains a
• List.isNone_finIdxOf? 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] [PartialEquivBEq α] {l : List α} {a : α} : (List.finIdxOf? a l).isNone = !l.contains a
• List.findIdx?_eq_map_findFinIdx?_val 📋 Init.Data.List.Find
  {α : Type u_1} {xs : List α} {p : α → Bool} : List.findIdx? p xs = Option.map (fun x => ↑x) (List.findFinIdx? p xs)
• List.idxOf?_eq_map_finIdxOf?_val 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] {xs : List α} {a : α} : List.idxOf? a xs = Option.map (fun x => ↑x) (List.finIdxOf? a xs)
• List.finIdxOf?_eq_none_iff 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : List.finIdxOf? a l = none ↔ a ∉ l
• List.findFinIdx?_eq_bind_find?_finIdxOf? 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {p : α → Bool} : List.findFinIdx? p xs = (List.find? p xs).bind fun a => List.finIdxOf? a xs
• List.findFinIdx?_eq_none_iff 📋 Init.Data.List.Find
  {α : Type u_1} {l : List α} {p : α → Bool} : List.findFinIdx? p l = none ↔ ∀ x ∈ l, ¬p x = true
• List.isNone_findFinIdx? 📋 Init.Data.List.Find
  {α : Type u_1} {l : List α} {p : α → Bool} : (List.findFinIdx? p l).isNone = l.all fun x => decide ¬p x = true
• List.findIdx?_go_eq_map_findFinIdx?_go_val 📋 Init.Data.List.Find
  {α : Type u_1} {l xs : List α} {p : α → Bool} {i : ℕ} {h : xs.length + i = l.length} : List.findIdx?.go p xs i = Option.map (fun x => ↑x) (List.findFinIdx?.go p l xs i h)
• List.find?_eq_map_findFinIdx?_getElem 📋 Init.Data.List.Find
  {α : Type u_1} {xs : List α} {p : α → Bool} : List.find? p xs = Option.map (fun x => xs[x]) (List.findFinIdx? p xs)
• List.findFinIdx?_subtype 📋 Init.Data.List.Find
  {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : List.findFinIdx? f l = Option.map (fun i => Fin.cast ⋯ i) (List.findFinIdx? g l.unattach)
• List.finIdxOf?_cons 📋 Init.Data.List.Find
  {α : Type u_1} {b : α} [BEq α] {a : α} {xs : List α} : List.finIdxOf? b (a :: xs) = if (a == b) = true then some ⟨0, ⋯⟩ else Option.map (fun x => x.succ) (List.finIdxOf? b xs)
• List.findFinIdx?_cons 📋 Init.Data.List.Find
  {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} : List.findFinIdx? p (x :: xs) = if p x = true then some 0 else Option.map Fin.succ (List.findFinIdx? p xs)
• List.finIdxOf?_eq_some_iff 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Fin l.length} : List.finIdxOf? a l = some i ↔ l[i] = a ∧ ∀ j < i, ¬l[j] = a
• List.findFinIdx?_eq_some_iff 📋 Init.Data.List.Find
  {α : Type u_1} {xs : List α} {p : α → Bool} {i : Fin xs.length} : List.findFinIdx? p xs = some i ↔ p xs[i] = true ∧ ∀ (j : Fin xs.length) (hji : j < i), ¬p xs[j] = true
• List.finIdxOf?_eq_pmap_idxOf? 📋 Init.Data.List.Find
  {α : Type u_1} {l : List α} {a : α} [BEq α] [LawfulBEq α] : List.finIdxOf? a l = Option.pmap (fun i h => ⟨i, ⋯⟩) (List.idxOf? a l) ⋯
• List.findFinIdx?_append 📋 Init.Data.List.Find
  {α : Type u_1} {xs ys : List α} {p : α → Bool} : List.findFinIdx? p (xs ++ ys) = (Option.map (Fin.castLE ⋯) (List.findFinIdx? p xs)).or (Option.map (Fin.cast ⋯) (Option.map (Fin.natAdd xs.length) (List.findFinIdx? p ys)))
• List.findFinIdx?_eq_pmap_findIdx? 📋 Init.Data.List.Find
  {α : Type u_1} {xs : List α} {p : α → Bool} : List.findFinIdx? p xs = Option.pmap (fun i m => ⟨i, ⋯⟩) (List.findIdx? p xs) ⋯
• List.findFinIdx?_toArray 📋 Init.Data.List.ToArray
  {α : Type u_1} (p : α → Bool) (l : List α) : Array.findFinIdx? p l.toArray = List.findFinIdx? p l
• List.finIdxOf?_toArray 📋 Init.Data.List.ToArray
  {α : Type u_1} [BEq α] (a : α) (l : List α) : l.toArray.finIdxOf? a = List.finIdxOf? a l
• Array.getElem_fin_eq_getElem_toList 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xs : Array α} {i : Fin xs.size} : xs[i] = xs.toList[i]
• List.mapFinIdx_eq_ofFn 📋 Init.Data.List.MapIdx
  {α : Type u_1} {β : Type u_2} {as : List α} {f : (i : ℕ) → α → i < as.length → β} : as.mapFinIdx f = List.ofFn fun i => f (↑i) as[i] ⋯
• Array.toList_ofFn 📋 Init.Data.Array.OfFn
  {n : ℕ} {α : Type u_1} {f : Fin n → α} : (Array.ofFn f).toList = List.ofFn f
• Array.toList_ofFnM 📋 Init.Data.Array.OfFn
  {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin n → m α} : Array.toList <$> Array.ofFnM f = List.ofFnM f
• Vector.toList_ofFn 📋 Init.Data.Vector.Lemmas
  {n : ℕ} {α : Type u_1} {f : Fin n → α} : (Vector.ofFn f).toList = List.ofFn f
• List.map_getElem_sublist 📋 Init.Data.List.Nat.Pairwise
  {α : Type u_1} {l : List α} {is : List (Fin l.length)} (h : List.Pairwise (fun x1 x2 => x1 < x2) is) : (List.map (fun x => l[x]) is).Sublist l
• List.sublist_eq_map_getElem 📋 Init.Data.List.Nat.Pairwise
  {α : Type u_1} {l l' : List α} (h : l'.Sublist l) : ∃ is, l' = List.map (fun x => l[x]) is ∧ List.Pairwise (fun x1 x2 => x1 < x2) is
• Vector.toList_ofFnM 📋 Init.Data.Vector.OfFn
  {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin n → m α} : Vector.toList <$> Vector.ofFnM f = List.ofFnM f
• Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.existsRatHint_of_ratHintsExhaustive 📋 Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
  {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRatAdd : f.ReadyForRatAdd) (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (ℕ × Array ℕ)) (ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true) (c' : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (c'_in_f : c' ∈ f.toList) (negPivot_in_c' : pivot.negate ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c') : ∃ i, f.clauses[ratHints[i].1]! = some c'
• Batteries.Linter.UnnecessarySeqFocus.getPath 📋 Batteries.Linter.UnnecessarySeqFocus
  : Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List ((n : ℕ) × Fin n) → Option Lean.Elab.Info
• List.map_coe_finRange_eq_range 📋 Batteries.Data.List.Lemmas
  {n : ℕ} : List.map (fun x => ↑x) (List.finRange n) = List.range n
• List.finRange_eq_nil_iff 📋 Batteries.Data.List.Lemmas
  {n : ℕ} : List.finRange n = [] ↔ n = 0
• List.map_get_finRange 📋 Batteries.Data.List.Lemmas
  {α : Type u_1} (l : List α) : List.map l.get (List.finRange l.length) = l
• List.finRange_eq_pmap_range 📋 Batteries.Data.List.Lemmas
  {n : ℕ} : List.finRange n = List.pmap Fin.mk (List.range n) ⋯
• List.map_getElem_finRange 📋 Batteries.Data.List.Lemmas
  {α : Type u_1} (l : List α) : List.map (fun x => l[↑x]) (List.finRange l.length) = l
• List.sigmaCountToIdx 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] (xs : List α) (xc : (x : α) × Fin (List.count x xs)) : Fin xs.length
• List.idxToSigmaCount 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [ReflBEq α] (xs : List α) (i : Fin xs.length) : (x : α) × Fin (List.count x xs)
• List.injective_sigmaCountToIdx 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} : Function.Injective xs.sigmaCountToIdx
• List.surjective_sigmaCountToIdx 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} : Function.Surjective xs.sigmaCountToIdx
• List.injective_idxToSigmaCount 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} : Function.Injective xs.idxToSigmaCount
• List.sigmaCountToIdx_idxToSigmaCount 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} {i : Fin xs.length} : xs.sigmaCountToIdx (xs.idxToSigmaCount i) = i
• List.leftInverse_sigmaCountToIdx_idxToSigmaCount 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} : Function.LeftInverse xs.sigmaCountToIdx xs.idxToSigmaCount
• List.rightInverse_idxToSigmaCount_sigmaCountToIdx 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} : Function.RightInverse xs.idxToSigmaCount xs.sigmaCountToIdx
• List.surjective_idxToSigmaCount 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} : Function.Surjective xs.idxToSigmaCount
• List.leftInverse_idxToSigmaCount_sigmaCountToIdx 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} : Function.LeftInverse xs.idxToSigmaCount xs.sigmaCountToIdx
• List.rightInverse_sigmaCountToIdx_idxToSigmaCount 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} : Function.RightInverse xs.sigmaCountToIdx xs.idxToSigmaCount
• List.idxToSigmaCount_sigmaCountToIdx 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {xc : (x : α) × Fin (List.count x xs)} : xs.idxToSigmaCount (xs.sigmaCountToIdx xc) = xc
• List.fst_idxToSigmaCount 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} {i : Fin xs.length} : (xs.idxToSigmaCount i).fst = xs[↑i]
• List.coe_sigmaCountToIdx 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] {xs : List α} {xc : (x : α) × Fin (List.count x xs)} : ↑(xs.sigmaCountToIdx xc) = List.idxOfNth xc.fst xs ↑xc.snd
• List.coe_snd_idxToSigmaCount 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} {i : Fin xs.length} : ↑(xs.idxToSigmaCount i).snd = List.countBefore xs[↑i] xs ↑i
• List.snd_idxToSigmaCount 📋 Batteries.Data.List.Count
  {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} {i : Fin xs.length} : (xs.idxToSigmaCount i).snd = ⟨List.countBefore xs[↑i] xs ↑i, ⋯⟩
• List.pairwise_iff_get 📋 Batteries.Data.List.Pairwise
  {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} : List.Pairwise R l ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
• List.Perm.idxBij 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Perm ys) : Fin xs.length → Fin ys.length
• List.Subperm.idxInj 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Subperm ys) (i : Fin xs.length) : Fin ys.length
• List.Perm.idxBij_injective 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.Injective h.idxBij
• List.Perm.idxBij_surjective 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.Surjective h.idxBij
• List.Subperm.idxInj_injective 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Subperm ys) : Function.Injective h.idxInj
• List.Perm.subperm_idxBij 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Perm ys) : ⋯.idxInj = h.idxBij
• List.Perm.idxBij_leftInverse_idxBij_symm 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.LeftInverse h.idxBij ⋯.idxBij
• List.Perm.idxBij_rightInverse_idxBij_symm 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.RightInverse h.idxBij ⋯.idxBij
• List.Perm.idxBij_symm_leftInverse_idxBij 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.LeftInverse ⋯.idxBij h.idxBij
• List.Perm.idxBij_symm_rightInverse_idxBij 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.RightInverse ⋯.idxBij h.idxBij
• List.Perm.idxBij_idxBij_symm 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) {i : Fin ys.length} : h.idxBij (⋯.idxBij i) = i
• List.Perm.idxBij_symm_idxBij 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) {i : Fin xs.length} : ⋯.idxBij (h.idxBij i) = i
• List.Subperm.idxInj_inj 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} {h : xs.Subperm ys} (i j : Fin xs.length) : h.idxInj i = h.idxInj j ↔ i = j
• List.Perm.getElem_idxBij_eq_getElem 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (hxy : xs.Perm ys) (i : Fin xs.length) : ys[↑(hxy.idxBij i)] = xs[↑i]
• List.Subperm.getElem_idxInj_eq_getElem 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Subperm ys) {i : Fin xs.length} : ys[↑(h.idxInj i)] = xs[↑i]
• List.Perm.getElem_idxBij_symm_eq_getElem 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (hxy : xs.Perm ys) (i : Fin ys.length) : xs[↑(⋯.idxBij i)] = ys[↑i]
• List.coe_idxInj 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} {h : xs.Subperm ys} {i : Fin xs.length} : ↑(h.idxInj i) = List.idxOfNth xs[i] ys (List.countBefore xs[i] xs ↑i)
• List.Perm.coe_idxBij 📋 Batteries.Data.List.Perm
  {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Perm ys) {i : Fin xs.length} : ↑(h.idxBij i) = List.idxOfNth xs[i] ys (List.countBefore xs[i] xs ↑i)
• List.cons_get_drop_succ 📋 Mathlib.Data.List.TakeDrop
  {α : Type u} {l : List α} {n : Fin l.length} : l.get n :: List.drop (↑n + 1) l = List.drop (↑n) l
• List.get_surjective_iff 📋 Mathlib.Data.List.Basic
  {α : Type u} {l : List α} : Function.Surjective l.get ↔ ∀ (x : α), x ∈ l
• List.forall_mem_iff_get 📋 Mathlib.Data.List.Basic
  {α : Type u} {l : List α} {p : α → Prop} : (∀ x ∈ l, p x) ↔ ∀ (i : Fin l.length), p (l.get i)
• List.exists_mem_iff_get 📋 Mathlib.Data.List.Basic
  {α : Type u} {l : List α} {p : α → Prop} : (∃ x ∈ l, p x) ↔ ∃ i, p (l.get i)
• List.getElem_fin_surjective_iff 📋 Mathlib.Data.List.Basic
  {α : Type u} {l : List α} : (Function.Surjective fun n => l[↑n]) ↔ ∀ (x : α), x ∈ l
• List.get_eq_getElem? 📋 Mathlib.Data.List.Basic
  {α : Type u} (l : List α) (i : Fin l.length) : l.get i = l[i]?.get ⋯
• List.get_reverse' 📋 Mathlib.Data.List.Basic
  {α : Type u} (l : List α) (n : Fin l.reverse.length) (hn' : l.length - 1 - ↑n < l.length) : l.reverse.get n = l.get ⟨l.length - 1 - ↑n, hn'⟩
• List.get_attach 📋 Mathlib.Data.List.Basic
  {α : Type u} (l : List α) (i : Fin l.attach.length) : ↑(l.attach.get i) = l.get ⟨↑i, ⋯⟩
• Function.Injective.nodup 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} (h : Function.Injective l.get) : l.Nodup
• List.Nodup.injective_get 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} (h : l.Nodup) : Function.Injective l.get
• List.nodup_iff_injective_get 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} : l.Nodup ↔ Function.Injective l.get
• List.get_idxOf 📋 Mathlib.Data.List.Nodup
  {α : Type u} [BEq α] [LawfulBEq α] {l : List α} (H : l.Nodup) (i : Fin l.length) : List.idxOf (l.get i) l = ↑i
• List.get_bijective_iff 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} [BEq α] [LawfulBEq α] : Function.Bijective l.get ↔ ∀ (a : α), List.count a l = 1
• List.not_nodup_of_get_eq_of_ne 📋 Mathlib.Data.List.Nodup
  {α : Type u} (xs : List α) (n m : Fin xs.length) (h : xs.get n = xs.get m) (hne : n ≠ m) : ¬xs.Nodup
• List.Nodup.get_inj_iff 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} (h : l.Nodup) {i j : Fin l.length} : l.get i = l.get j ↔ i = j
• List.Nodup.erase_get 📋 Mathlib.Data.List.Nodup
  {α : Type u} [BEq α] [LawfulBEq α] {l : List α} (hl : l.Nodup) (i : Fin l.length) : l.erase (l.get i) = l.eraseIdx ↑i
• List.nodup_iff_injective_getElem 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} : l.Nodup ↔ Function.Injective fun i => l[↑i]
• List.getElem_bijective_iff 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} [BEq α] [LawfulBEq α] : (Function.Bijective fun n => l[n]) ↔ ∀ (a : α), List.count a l = 1
• Set.range_list_get 📋 Mathlib.Data.Set.List
  {α : Type u_1} (l : List α) : Set.range l.get = {x | x ∈ l}
• List.get_inits 📋 Mathlib.Data.List.Infix
  {α : Type u_1} (l : List α) (n : Fin l.inits.length) : l.inits.get n = List.take (↑n) l
• List.get_tails 📋 Mathlib.Data.List.Infix
  {α : Type u_1} (l : List α) (n : Fin l.tails.length) : l.tails.get n = List.drop (↑n) l
• List.equivSigmaTuple 📋 Mathlib.Data.List.OfFn
  {α : Type u} : List α ≃ (n : ℕ) × (Fin n → α)
• List.ofFn_injective 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} : Function.Injective List.ofFn
• List.ofFn_const 📋 Mathlib.Data.List.OfFn
  {α : Type u} (n : ℕ) (c : α) : (List.ofFn fun x => c) = List.replicate n c
• List.ofFnRec 📋 Mathlib.Data.List.OfFn
  {α : Type u} {C : List α → Sort u_1} (h : (n : ℕ) → (f : Fin n → α) → C (List.ofFn f)) (l : List α) : C l
• List.forall_iff_forall_tuple 📋 Mathlib.Data.List.OfFn
  {α : Type u} {P : List α → Prop} : (∀ (l : List α), P l) ↔ ∀ (n : ℕ) (f : Fin n → α), P (List.ofFn f)
• List.ofFn_inj 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} {f g : Fin n → α} : List.ofFn f = List.ofFn g ↔ f = g
• List.exists_iff_exists_tuple 📋 Mathlib.Data.List.OfFn
  {α : Type u} {P : List α → Prop} : (∃ l, P l) ↔ ∃ n f, P (List.ofFn f)
• List.forall_mem_ofFn_iff 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} {f : Fin n → α} {P : α → Prop} : (∀ i ∈ List.ofFn f, P i) ↔ ∀ (j : Fin n), P (f j)
• List.ofFn_comp' 📋 Mathlib.Data.List.OfFn
  {α : Type u} {β : Type u_1} {n : ℕ} (f : Fin n → α) (g : α → β) : (List.ofFn fun i => g (f i)) = List.map g (List.ofFn f)
• List.ofFn_succ' 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n.succ → α) : List.ofFn f = (List.ofFn fun i => f i.castSucc).concat (f (Fin.last n))
• List.mem_ofFn' 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n → α) (a : α) : a ∈ List.ofFn f ↔ a ∈ Set.range f
• List.ofFn_congr 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m n : ℕ} (h : m = n) (f : Fin m → α) : List.ofFn f = List.ofFn fun i => f (Fin.cast ⋯ i)
• List.ofFnRec_ofFn 📋 Mathlib.Data.List.OfFn
  {α : Type u} {C : List α → Sort u_1} (h : (n : ℕ) → (f : Fin n → α) → C (List.ofFn f)) {n : ℕ} (f : Fin n → α) : List.ofFnRec h (List.ofFn f) = h n f
• List.ofFn_fin_repeat 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m : ℕ} (a : Fin m → α) (n : ℕ) : List.ofFn (Fin.repeat n a) = (List.replicate n (List.ofFn a)).flatten
• List.ofFn_inj' 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m n : ℕ} {f : Fin m → α} {g : Fin n → α} : List.ofFn f = List.ofFn g ↔ ⟨m, f⟩ = ⟨n, g⟩
• List.ofFn_fin_append 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m n : ℕ} (a : Fin m → α) (b : Fin n → α) : List.ofFn (Fin.append a b) = List.ofFn a ++ List.ofFn b
• List.ofFn_cons 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (a : α) (f : Fin n → α) : List.ofFn (Fin.cons a f) = a :: List.ofFn f
• List.ofFn_getElem_eq_map 📋 Mathlib.Data.List.OfFn
  {α : Type u} {β : Type u_1} (l : List α) (f : α → β) : (List.ofFn fun i => f l[↑i]) = List.map f l
• List.equivSigmaTuple_apply_fst 📋 Mathlib.Data.List.OfFn
  {α : Type u} (l : List α) : (List.equivSigmaTuple l).fst = l.length
• List.getLast_ofFn_succ 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n.succ → α) : (List.ofFn f).getLast ⋯ = f (Fin.last n)
• List.equivSigmaTuple_apply_snd 📋 Mathlib.Data.List.OfFn
  {α : Type u} (l : List α) (a✝ : Fin l.length) : (List.equivSigmaTuple l).snd a✝ = l.get a✝
• List.equivSigmaTuple_symm_apply 📋 Mathlib.Data.List.OfFn
  {α : Type u} (f : (n : ℕ) × (Fin n → α)) : List.equivSigmaTuple.symm f = List.ofFn f.snd
• List.ofFn_mul 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m n : ℕ} (f : Fin (m * n) → α) : List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten
• List.ofFn_mul' 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m n : ℕ} (f : Fin (m * n) → α) : List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨m * ↑i + ↑j, ⋯⟩).flatten
• List.ofFn_id 📋 Mathlib.Data.List.FinRange
  (n : ℕ) : List.ofFn id = List.finRange n
• List.map_coe_finRange 📋 Mathlib.Data.List.FinRange
  {n : ℕ} : List.map (fun x => ↑x) (List.finRange n) = List.range n
• List.finRange_eq_nil 📋 Mathlib.Data.List.FinRange
  {n : ℕ} : List.finRange n = [] ↔ n = 0
• List.ofFn_eq_map 📋 Mathlib.Data.List.FinRange
  {α : Type u} {n : ℕ} {f : Fin n → α} : List.ofFn f = List.map f (List.finRange n)
• List.finRange_map_get 📋 Mathlib.Data.List.FinRange
  {α : Type u_1} (l : List α) : List.map l.get (List.finRange l.length) = l
• List.finRange_map_getElem 📋 Mathlib.Data.List.FinRange
  {α : Type u_1} (l : List α) : List.map (fun x => l[↑x]) (List.finRange l.length) = l
• List.ofFn_eq_pmap 📋 Mathlib.Data.List.FinRange
  {α : Type u} {n : ℕ} {f : Fin n → α} : List.ofFn f = List.pmap (fun i hi => f ⟨i, hi⟩) (List.range n) ⋯
• List.finRange_succ_eq_map 📋 Mathlib.Data.List.FinRange
  (n : ℕ) : List.finRange n.succ = 0 :: List.map Fin.succ (List.finRange n)
• Fin.univ_image_get 📋 Mathlib.Data.Fintype.Basic
  {α : Type u_1} [DecidableEq α] (l : List α) : Finset.image l.get Finset.univ = l.toFinset
• Fin.univ_image_get' 📋 Mathlib.Data.Fintype.Basic
  {α : Type u_1} {β : Type u_2} [DecidableEq β] (l : List α) (f : α → β) : Finset.image (fun x => f (l.get x)) Finset.univ = (List.map f l).toFinset
• Fin.univ_image_getElem' 📋 Mathlib.Data.Fintype.Basic
  {α : Type u_1} {β : Type u_2} [DecidableEq β] (l : List α) (f : α → β) : Finset.image (fun i => f l[↑i]) Finset.univ = (List.map f l).toFinset
• Antitone.sortedGE 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : Antitone l.get → l.SortedGE
• Monotone.sortedLE 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : Monotone l.get → l.SortedLE
• StrictAnti.sortedGT 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : StrictAnti l.get → l.SortedGT
• StrictMono.sortedLT 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : StrictMono l.get → l.SortedLT
• List.SortedGE.antitone_get 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : l.SortedGE → Antitone l.get
• List.SortedGT.strictAnti_get 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : l.SortedGT → StrictAnti l.get
• List.SortedLE.monotone_get 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE → Monotone l.get
• List.SortedLT.strictMono_get 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT → StrictMono l.get
• List.sortedGE_iff_antitone_get 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : l.SortedGE ↔ Antitone l.get
• List.sortedGT_iff_strictAnti_get 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : l.SortedGT ↔ StrictAnti l.get
• List.sortedLE_iff_monotone_get 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE ↔ Monotone l.get
• List.sortedLT_iff_strictMono_get 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT ↔ StrictMono l.get
• List.Nodup.getEquivOfForallMemList 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) : Fin l.length ≃ α
• List.Nodup.getEquiv 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) : Fin l.length ≃ { x // x ∈ l }
• List.getEquivOfForallCountEqOne 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (h : ∀ (x : α), List.count x l = 1) : Fin l.length ≃ α
• List.Sorted.get_mono 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE → Monotone l.get
• List.Sorted.get_strictMono 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT → StrictMono l.get
• List.Nodup.getBijectionOfForallMemList 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) : { f // Function.Bijective f }
• List.Sorted.getIso 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [Preorder α] [DecidableEq α] (l : List α) (H : l.SortedLT) : Fin l.length ≃o { x // x ∈ l }
• List.SortedLT.getIso 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [Preorder α] [DecidableEq α] (l : List α) (H : l.SortedLT) : Fin l.length ≃o { x // x ∈ l }
• List.Nodup.getBijectionOfForallMemList_coe 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (i : Fin l.length) : ↑(List.Nodup.getBijectionOfForallMemList l nd h) i = l.get i
• List.duplicate_iff_exists_distinct_get 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} {l : List α} {x : α} : List.Duplicate x l ↔ ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m
• List.Nodup.getEquivOfForallMemList_apply 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (i : Fin l.length) : (List.Nodup.getEquivOfForallMemList l nd h) i = l.get i
• List.Nodup.getEquivOfForallMemList_symm_apply_val 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (a : α) : ↑((List.Nodup.getEquivOfForallMemList l nd h).symm a) = List.idxOf a l
• List.getEquivOfForallCountEqOne_symm_apply_val 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (h : ∀ (x : α), List.count x l = 1) (a : α) : ↑((l.getEquivOfForallCountEqOne h).symm a) = List.idxOf a l
• List.getEquivOfForallCountEqOne_apply 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (h : ∀ (x : α), List.count x l = 1) (i : Fin l.length) : (l.getEquivOfForallCountEqOne h) i = l[↑i]
• List.sublist_iff_exists_fin_orderEmbedding_get_eq 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} {l l' : List α} : l.Sublist l' ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
• List.Nodup.getEquiv_apply_coe 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) (i : Fin l.length) : ↑((List.Nodup.getEquiv l H) i) = l.get i
• List.Sorted.coe_getIso_apply 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [Preorder α] {l : List α} [DecidableEq α] (H : l.SortedLT) {i : Fin l.length} : ↑((List.SortedLT.getIso l H) i) = l.get i
• List.SortedLT.coe_getIso_apply 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [Preorder α] {l : List α} [DecidableEq α] (H : l.SortedLT) {i : Fin l.length} : ↑((List.SortedLT.getIso l H) i) = l.get i
• List.Nodup.getEquiv_symm_apply_val 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) (x : { x // x ∈ l }) : ↑((List.Nodup.getEquiv l H).symm x) = List.idxOf (↑x) l

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 401c76f serving mathlib revision a3d2529