Loogle!

Result

Found 69 definitions mentioning List.IsSuffix.

• List.IsSuffix 📋 Init.Data.List.Basic
  {α : Type u} (l₁ l₂ : List α) : Prop
• List.leftpad_suffix 📋 Init.Data.List.Lemmas
  {α : Type u_1} (n : ℕ) (a : α) (l : List α) : l <:+ List.leftpad n a l
• List.IsSuffix.eq_1 📋 Init.Data.List.Lemmas
  {α : Type u} (l₁ l₂ : List α) : (l₁ <:+ l₂) = ∃ t, t ++ l₁ = l₂
• List.suffix_refl 📋 Init.Data.List.Sublist
  {α : Type u_1} (l : List α) : l <:+ l
• List.suffix_rfl 📋 Init.Data.List.Sublist
  {α : Type u_1} {l : List α} : l <:+ l
• List.nil_suffix 📋 Init.Data.List.Sublist
  {α : Type u_1} {l : List α} : [] <:+ l
• List.tail_suffix 📋 Init.Data.List.Sublist
  {α : Type u_1} (l : List α) : l.tail <:+ l
• List.drop_suffix 📋 Init.Data.List.Sublist
  {α : Type u_1} (i : ℕ) (l : List α) : List.drop i l <:+ l
• List.suffix_cons 📋 Init.Data.List.Sublist
  {α : Type u_1} (a : α) (l : List α) : l <:+ a :: l
• List.dropWhile_suffix 📋 Init.Data.List.Sublist
  {α : Type u_1} {l : List α} (p : α → Bool) : List.dropWhile p l <:+ l
• List.instDecidableIsSuffixOfDecidableEq 📋 Init.Data.List.Sublist
  {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <:+ l₂)
• List.IsSuffix.isInfix 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+ l₂ → l₁ <:+: l₂
• List.IsSuffix.sublist 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+ l₂) : l₁.Sublist l₂
• List.eq_nil_of_suffix_nil 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l : List α✝} (h : l <:+ []) : l = []
• List.suffix_nil 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l : List α✝} : l <:+ [] ↔ l = []
• List.IsSuffix.subset 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} (hl : l₁ <:+ l₂) : l₁ ⊆ l₂
• List.IsPrefix.reverse 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <+: l₂ → l₁.reverse <:+ l₂.reverse
• List.IsSuffix.reverse 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+ l₂ → l₁.reverse <+: l₂.reverse
• List.reverse_prefix 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁.reverse <+: l₂.reverse ↔ l₁ <:+ l₂
• List.reverse_suffix 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁.reverse <:+ l₂.reverse ↔ l₁ <+: l₂
• List.IsSuffix.length_le 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length
• List.IsSuffix.trans 📋 Init.Data.List.Sublist
  {α : Type u_1} {l₁ l₂ l₃ : List α} : l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃
• List.drop_suffix_drop_left 📋 Init.Data.List.Sublist
  {α : Type u_1} (l : List α) {i j : ℕ} (h : i ≤ j) : List.drop j l <:+ List.drop i l
• List.IsSuffix.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.IsSuffix.ne_nil 📋 Init.Data.List.Sublist
  {α : Type u_1} {xs ys : List α} (h : xs <:+ ys) (hx : xs ≠ []) : ys ≠ []
• List.suffix_append 📋 Init.Data.List.Sublist
  {α : Type u_1} (l₁ l₂ : List α) : l₂ <:+ l₁ ++ l₂
• List.IsSuffix.eq_of_length 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+ l₂) : l₁.length = l₂.length → l₁ = l₂
• List.isSuffixOf_iff_suffix 📋 Init.Data.List.Sublist
  {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : l₁.isSuffixOf l₂ = true ↔ l₁ <:+ l₂
• List.IsSuffix.eq_of_length_le 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+ l₂) : l₂.length ≤ l₁.length → l₁ = l₂
• List.infix_iff_prefix_suffix 📋 Init.Data.List.Sublist
  {α : Type u_1} {l₁ l₂ : List α} : l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂
• List.infix_iff_suffix_prefix 📋 Init.Data.List.Sublist
  {α : Type u_1} {l₁ l₂ : List α} : l₁ <:+: l₂ ↔ ∃ t, l₁ <:+ t ∧ t <+: l₂
• List.suffix_or_suffix_of_suffix 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₃ l₂ : List α✝} (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) : l₁ <:+ l₂ ∨ l₂ <:+ l₁
• List.IsSuffix.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.IsSuffix.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.IsSuffix.mem 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ : List α✝} {a : α✝} {l₂ : List α✝} (hx : a ∈ l₁) (hl : l₁ <:+ l₂) : a ∈ l₂
• List.suffix_cons_iff 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ : List α✝} {a : α✝} {l₂ : List α✝} : l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂
• List.suffix_of_suffix_length_le 📋 Init.Data.List.Sublist
  {α✝ : Type u_1} {l₁ l₃ l₂ : List α✝} (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : l₁.length ≤ l₂.length) : l₁ <:+ l₂
• List.IsSuffix.getLast 📋 Init.Data.List.Sublist
  {α : Type u_1} {l₁ l₂ : List α} (h : l₁ <:+ l₂) (hx : l₁ ≠ []) : l₁.getLast hx = l₂.getLast ⋯
• List.isSuffix_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.isSuffix_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.isSuffix_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.isSuffix_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.infix_concat_iff 📋 Init.Data.List.Sublist
  {α : Type u_1} {l₁ l₂ : List α} {a : α} : l₁ <:+: l₂ ++ [a] ↔ l₁ <:+ l₂ ++ [a] ∨ l₁ <:+: l₂
• List.suffix_concat_iff 📋 Init.Data.List.Sublist
  {α : Type u_1} {l₁ l₂ : List α} {a : α} : l₁ <:+ l₂ ++ [a] ↔ l₁ = [] ∨ ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂
• List.IsSuffix.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.IsSuffix.count_le 📋 Init.Data.List.Count
  {α : Type u_1} [BEq α] {l₁ l₂ : List α} (h : l₁ <:+ l₂) (a : α) : List.count a l₁ ≤ List.count a l₂
• List.IsSuffix.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.IsSuffix.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.IsSuffix.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.IsSuffix.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.suffix_iff_eq_drop 📋 Init.Data.List.Nat.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+ l₂ ↔ l₁ = List.drop (l₂.length - l₁.length) l₂
• List.suffix_iff_eq_append 📋 Init.Data.List.Nat.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+ l₂ ↔ List.take (l₂.length - l₁.length) l₂ ++ l₁ = l₂
• List.isSuffix_iff 📋 Init.Data.List.Nat.Sublist
  {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+ l₂ ↔ l₁.length ≤ l₂.length ∧ ∀ (i : ℕ) (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i]
• List.IsSuffix.getElem 📋 Init.Data.List.Nat.Sublist
  {α : Type u_1} {xs ys : List α} (h : xs <:+ ys) {i : ℕ} (hn : i < xs.length) : xs[i] = ys[ys.length - xs.length + i]
• List.IsSuffix.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.IsSuffix.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₁
• String.utf8Len_le_of_suffix 📋 Batteries.Data.String.Lemmas
  {cs₁ cs₂ : List Char} (h : cs₁ <:+ cs₂) : String.utf8Len cs₁ ≤ String.utf8Len cs₂
• List.suffix_union_right 📋 Mathlib.Data.List.Lattice
  {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : l₂ <:+ l₁ ∪ l₂
• List.instIsPartialOrderIsSuffix 📋 Mathlib.Data.List.Infix
  {α : Type u_1} : IsPartialOrder (List α) fun x1 x2 => x1 <:+ x2
• List.suffix_insert 📋 Mathlib.Data.List.Infix
  {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : l <:+ List.insert a l
• List.IsSuffix.flatten 📋 Mathlib.Data.List.Infix
  {α : Type u_1} {l₁ l₂ : List (List α)} (h : l₁ <:+ l₂) : l₁.flatten <:+ l₂.flatten
• List.mem_tails 📋 Mathlib.Data.List.Infix
  {α : Type u_1} (s t : List α) : s ∈ t.tails ↔ s <:+ t
• List.IsSuffix.flatMap 📋 Mathlib.Data.List.Infix
  {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (h : l₁ <:+ l₂) (f : α → List β) : List.flatMap f l₁ <:+ List.flatMap f l₂
• List.Chain'.suffix 📋 Mathlib.Data.List.Chain
  {α : Type u} {R : α → α → Prop} {l l₁ : List α} (h : List.Chain' R l) (h' : l₁ <:+ l) : List.Chain' R l₁
• DyckWord.le_of_suffix 📋 Mathlib.Combinatorics.Enumerative.DyckWord
  {p q : DyckWord} (h : ↑p <:+ ↑q) : p ≤ q
• List.rtakeWhile_suffix 📋 Mathlib.Data.List.DropRight
  {α : Type u_1} (p : α → Bool) (l : List α) : List.rtakeWhile p l <:+ l
• le_levenshtein_cons 📋 Mathlib.Data.List.EditDistance.Bounds
  {α : Type u_1} {β : Type u_2} {δ : Type u_3} {C : Levenshtein.Cost α β δ} [LinearOrderedAddCommMonoid δ] [CanonicallyOrderedAdd δ] (xs : List α) (y : β) (ys : List β) : ∃ xs', xs' <:+ xs ∧ levenshtein C xs' ys ≤ levenshtein C xs (y :: ys)
• le_levenshtein_append 📋 Mathlib.Data.List.EditDistance.Bounds
  {α : Type u_1} {β : Type u_2} {δ : Type u_3} {C : Levenshtein.Cost α β δ} [LinearOrderedAddCommMonoid δ] [CanonicallyOrderedAdd δ] (xs : List α) (ys₁ ys₂ : List β) : ∃ xs', xs' <:+ xs ∧ levenshtein C xs' ys₂ ≤ levenshtein C xs (ys₁ ++ ys₂)
• String.IsSuffix.eq_1 📋 Mathlib.Data.String.Lemmas
  (d1 d2 : List Char) : { data := d1 }.IsSuffix { data := d2 } = (d1 <:+ d2)

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, _ * _, _ ^ _, |- _ < _ → _
woould 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 d56dbe9 serving mathlib revision 3d845f2