Loogle!

Result

Found 1722 declarations mentioning HAppend.hAppend. Of these, 69 have a name containing "concat".

• List.concat_eq_append 📋 Init.Data.List.Basic
  {α : Type u} {as : List α} {a : α} : as.concat a = as ++ [a]
• List.concat_ne_nil 📋 Init.Data.List.Lemmas
  {α : Type u_1} (a : α) (l : List α) : l ++ [a] ≠ []
• List.dropLast_concat 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {l₁ : List α✝} {b : α✝} : (l₁ ++ [b]).dropLast = l₁
• List.getLastD_concat 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a b : α} {l : List α} : (l ++ [b]).getLastD a = b
• List.mem_concat_self 📋 Init.Data.List.Lemmas
  {α : Type u_1} {xs : List α} {a : α} : a ∈ xs ++ [a]
• List.getLast?_concat 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} {a : α} : (l ++ [a]).getLast? = some a
• List.getLast_concat 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {l : List α} : (l ++ [a]).getLast ⋯ = a
• List.reverse_concat 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse
• List.head?_concat 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} {a : α} : (l ++ [a]).head? = some (l.head?.getD a)
• List.dropLast_concat_getLast 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} (h : l ≠ []) : l.dropLast ++ [l.getLast h] = l
• List.reverse_eq_concat 📋 Init.Data.List.Lemmas
  {α : Type u_1} {xs ys : List α} {a : α} : xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse
• List.append_concat 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {l₁ l₂ : List α} : l₁ ++ l₂.concat a = (l₁ ++ l₂).concat a
• List.concat_append 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {l₁ l₂ : List α} : l₁.concat a ++ l₂ = l₁ ++ a :: l₂
• List.getElem?_concat_length 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} {a : α} : (l ++ [a])[l.length]? = some a
• List.head?_concat_concat 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {l : List α✝} {a b : α✝} : (l ++ [a, b]).head? = (l ++ [a]).head?
• List.flatten_concat 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List α)} {l : List α} : (L ++ [l]).flatten = L.flatten ++ l
• List.concat_beq_concat 📋 Init.Data.List.Lemmas
  {α : Type u_1} [BEq α] {a b : α} {l₁ l₂ : List α} : (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b)
• List.getElem_concat_length 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} {a : α} {i : ℕ} (h : i = l.length) (w : i < (l ++ [a]).length) : (l ++ [a])[i] = a
• List.infix_concat_iff 📋 Init.Data.List.Sublist
  {α : Type u_1} {l₁ l₂ : List α} {a : α} : l₁ <:+: l₂ ++ [a] ↔ l₁ <:+ l₂ ++ [a] ∨ l₁ <:+: l₂
• List.prefix_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₂
• BitVec.shiftLeft_eq_concat_of_lt 📋 Init.Data.BitVec.Lemmas
  {w : ℕ} {x : BitVec w} {n : ℕ} (hn : n < w) : x <<< n = BitVec.cast ⋯ (BitVec.extractLsb' 0 (w - n) x ++ 0#n)
• List.range'_1_concat 📋 Init.Data.List.Range
  {s n : ℕ} : List.range' s (n + 1) = List.range' s n ++ [s + n]
• List.range'_concat 📋 Init.Data.List.Range
  {step s n : ℕ} : List.range' s (n + 1) step = List.range' s n step ++ [s + step * n]
• List.mapIdx_concat 📋 Init.Data.List.MapIdx
  {α : Type u_1} {α✝ : Type u_2} {f : ℕ → α → α✝} {l : List α} {e : α} : List.mapIdx f (l ++ [e]) = List.mapIdx f l ++ [f l.length e]
• List.mapFinIdx_concat 📋 Init.Data.List.MapIdx
  {α : Type u_1} {β : Type u_2} {l : List α} {e : α} {f : (i : ℕ) → α → i < (l ++ [e]).length → β} : (l ++ [e]).mapFinIdx f = (l.mapFinIdx fun i a h => f i a ⋯) ++ [f l.length e ⋯]
• List.scanrM_concat 📋 Init.Data.List.Scan.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {xs : List α} {x : α} [Monad m] [LawfulMonad m] {f : α → β → m β} : List.scanrM f init (xs ++ [x]) = do let __do_lift ← f x init let __do_lift ← List.scanrM f __do_lift xs pure (__do_lift ++ [init])
• Array.range'_1_concat 📋 Init.Data.Array.Range
  {s n : ℕ} : Array.range' s (n + 1) = Array.range' s n ++ #[s + n]
• Array.range'_concat 📋 Init.Data.Array.Range
  {step s n : ℕ} : Array.range' s (n + 1) step = Array.range' s n step ++ #[s + step * n]
• Vector.range'_1_concat 📋 Init.Data.Vector.Range
  {s n : ℕ} : Vector.range' s (n + 1) = Vector.range' s n ++ #v[s + n]
• Vector.range'_concat 📋 Init.Data.Vector.Range
  {step s n : ℕ} : Vector.range' s (n + 1) step = Vector.range' s n step ++ #v[s + step * n]
• List.take_concat_get' 📋 Mathlib.Data.List.TakeDrop
  {α : Type u} (l : List α) (i : ℕ) (h : i < l.length) : List.take i l ++ [l[i]] = List.take (i + 1) l
• List.reverse_concat' 📋 Mathlib.Data.List.Basic
  {α : Type u} (l : List α) (a : α) : (l ++ [a]).reverse = a :: l.reverse
• List.eq_nil_or_concat' 📋 Mathlib.Data.List.Basic
  {α : Type u} (l : List α) : l = [] ∨ ∃ L b, l = L ++ [b]
• List.foldl_concat 📋 Mathlib.Data.List.Basic
  {α : Type u} {β : Type v} (f : β → α → β) (b : β) (x : α) (xs : List α) : List.foldl f b (xs ++ [x]) = f (List.foldl f b xs) x
• List.foldr_concat 📋 Mathlib.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β → β) (b : β) (x : α) (xs : List α) : List.foldr f b (xs ++ [x]) = List.foldr f (f x b) xs
• List.reverseRecOn_concat 📋 Mathlib.Data.List.Induction
  {α : Type u_1} {motive : List α → Sort u_2} (x : α) (xs : List α) (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) : List.reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (List.reverseRecOn xs nil append_singleton)
• List.reverseRec_concat 📋 Mathlib.Data.List.Induction
  {α : Type u_1} {motive : List α → Sort u_2} (x : α) (xs : List α) (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) : List.reverseRec nil append_singleton (xs ++ [x]) = append_singleton xs x (List.reverseRec nil append_singleton xs)
• List.concat_get_prefix 📋 Mathlib.Data.List.Infix
  {α : Type u_1} {x y : List α} (h : x <+: y) (hl : x.length < y.length) : x ++ [y.get ⟨x.length, hl⟩] <+: y
• List.IsChain.backwards_concat_induction 📋 Mathlib.Data.List.Chain
  {α : Type u} {r : α → α → Prop} {b : α} (p : α → Prop) (l : List α) (h : List.IsChain r (l ++ [b])) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) (i : α) : i ∈ l → p i
• List.IsChain.concat_induction_head 📋 Mathlib.Data.List.Chain
  {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : List.IsChain r (l ++ [b])) (hb : (l ++ [b]).head ⋯ = a) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) : p b
• List.IsChain.concat_induction 📋 Mathlib.Data.List.Chain
  {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : List.IsChain r (l ++ [b])) (hb : (l ++ [b]).head ⋯ = a) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) (i : α) : i ∈ l ++ [b] → p i
• List.isRotated_concat 📋 Mathlib.Data.List.Rotate
  {α : Type u} (hd : α) (tl : List α) : tl ++ [hd] ~r hd :: tl
• List.sublists_concat 📋 Mathlib.Data.List.Sublists
  {α : Type u} (l : List α) (a : α) : (l ++ [a]).sublists = l.sublists ++ List.map (fun x => x ++ [a]) l.sublists
• List.maximum_concat 📋 Mathlib.Data.List.MinMax
  {α : Type u_1} [LinearOrder α] (a : α) (l : List α) : (l ++ [a]).maximum = max l.maximum ↑a
• List.minimum_concat 📋 Mathlib.Data.List.MinMax
  {α : Type u_1} [LinearOrder α] (a : α) (l : List α) : (l ++ [a]).minimum = min l.minimum ↑a
• List.argmax_concat 📋 Mathlib.Data.List.MinMax
  {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] (f : α → β) (a : α) (l : List α) : List.argmax f (l ++ [a]) = Option.casesOn (List.argmax f l) (some a) fun c => if f c < f a then some a else some c
• List.argmin_concat 📋 Mathlib.Data.List.MinMax
  {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] (f : α → β) (a : α) (l : List α) : List.argmin f (l ++ [a]) = Option.casesOn (List.argmin f l) (some a) fun c => if f a < f c then some a else some c
• List.nextOr_concat 📋 Mathlib.Data.List.Cycle
  {α : Type u_1} [DecidableEq α] {xs : List α} {x : α} (d : α) (h : x ∉ xs) : (xs ++ [x]).nextOr x d = d
• List.next_cons_concat 📋 Mathlib.Data.List.Cycle
  {α : Type u_1} [DecidableEq α] (l : List α) (x y : α) (hy : x ≠ y) (hx : x ∉ l) (h : x ∈ y :: l ++ [x] := ⋯) : (y :: l ++ [x]).next x h = y
• List.formPerm_cons_concat_apply_last 📋 Mathlib.GroupTheory.Perm.List
  {α : Type u_1} [DecidableEq α] (x y : α) (xs : List α) : (x :: (xs ++ [y])).formPerm y = x
• Stream'.concat_take_get 📋 Mathlib.Data.Stream.Init
  {α : Type u} {n : ℕ} {s : Stream' α} : Stream'.take n s ++ [s.get n] = Stream'.take (n + 1) s
• List.toFinsupp_concat_eq_toFinsupp_add_single 📋 Mathlib.Data.List.ToFinsupp
  {R : Type u_2} [AddZeroClass R] (x : R) (xs : List R) [DecidablePred fun i => (xs ++ [x]).getD i 0 ≠ 0] [DecidablePred fun i => xs.getD i 0 ≠ 0] : (xs ++ [x]).toFinsupp = xs.toFinsupp + fun₀ | xs.length => x
• SimpleGraph.Walk.support_dropLast_concat 📋 Mathlib.Combinatorics.SimpleGraph.Walks.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : ¬p.Nil) : p.dropLast.support ++ [v] = p.support
• DyckWord.cons_tail_dropLast_concat 📋 Mathlib.Combinatorics.Enumerative.DyckWord
  {p : DyckWord} (h : p ≠ 0) : DyckStep.U :: (↑p).dropLast.tail ++ [DyckStep.D] = ↑p
• Primrec.list_concat 📋 Mathlib.Computability.Primrec.List
  {α : Type u_1} [Primcodable α] : Primrec₂ fun l a => l ++ [a]
• Computable.list_concat 📋 Mathlib.Computability.Partrec
  {α : Type u_1} [Primcodable α] : Computable₂ fun l a => l ++ [a]
• List.reduceOption_concat 📋 Mathlib.Data.List.ReduceOption
  {α : Type u_1} (l : List (Option α)) (x : Option α) : (l.concat x).reduceOption = l.reduceOption ++ x.toList
• List.reduceOption_eq_concat_iff 📋 Mathlib.Data.List.ReduceOption
  {α : Type u_1} (l : List (Option α)) (l' : List α) (a : α) : l.reduceOption = l'.concat a ↔ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
• List.rtakeWhile_concat_neg 📋 Mathlib.Data.List.DropRight
  {α : Type u_1} (p : α → Bool) (l : List α) (x : α) (h : ¬p x = true) : List.rtakeWhile p (l ++ [x]) = []
• List.rdropWhile_concat_pos 📋 Mathlib.Data.List.DropRight
  {α : Type u_1} (p : α → Bool) (l : List α) (x : α) (h : p x = true) : List.rdropWhile p (l ++ [x]) = List.rdropWhile p l
• List.rdrop_concat_succ 📋 Mathlib.Data.List.DropRight
  {α : Type u_1} (l : List α) (n : ℕ) (x : α) : (l ++ [x]).rdrop (n + 1) = l.rdrop n
• List.rdropWhile_concat_neg 📋 Mathlib.Data.List.DropRight
  {α : Type u_1} (p : α → Bool) (l : List α) (x : α) (h : ¬p x = true) : List.rdropWhile p (l ++ [x]) = l ++ [x]
• List.rtakeWhile_concat_pos 📋 Mathlib.Data.List.DropRight
  {α : Type u_1} (p : α → Bool) (l : List α) (x : α) (h : p x = true) : List.rtakeWhile p (l ++ [x]) = List.rtakeWhile p l ++ [x]
• List.rtake_concat_succ 📋 Mathlib.Data.List.DropRight
  {α : Type u_1} (l : List α) (n : ℕ) (x : α) : (l ++ [x]).rtake (n + 1) = l.rtake n ++ [x]
• List.rdropWhile_concat 📋 Mathlib.Data.List.DropRight
  {α : Type u_1} (p : α → Bool) (l : List α) (x : α) : List.rdropWhile p (l ++ [x]) = if p x = true then List.rdropWhile p l else l ++ [x]
• List.rtakeWhile_concat 📋 Mathlib.Data.List.DropRight
  {α : Type u_1} (p : α → Bool) (l : List α) (x : α) : List.rtakeWhile p (l ++ [x]) = if p x = true then List.rtakeWhile p l ++ [x] else []
• List.modifyLast_concat 📋 Mathlib.Data.List.ModifyLast
  {α : Type u_1} (f : α → α) (a : α) (l : List α) : List.modifyLast f (l ++ [a]) = l ++ [f a]
• List.Palindrome.cons_concat 📋 Mathlib.Data.List.Palindrome
  {α : Type u_1} (x : α) {l : List α} : l.Palindrome → (x :: (l ++ [x])).Palindrome

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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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 128218b serving mathlib revision 6682a4e