Loogle!

Result

Found 1690 declarations mentioning List.map. Of these, only the first 200 are shown.

• List.map 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) (l : List α) : List β
• List.map_eq_mapTR 📋 Init.Data.List.Basic
  : @List.map = @List.mapTR
• List.map_nil 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} {f : α → β} : List.map f [] = []
• List.map.eq_1 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) : List.map f [] = []
• List.flatMap.eq_1 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (b : α → List β) (as : List α) : List.flatMap b as = (List.map b as).flatten
• List.map_cons 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} {f : α → β} {a : α} {l : List α} : List.map f (a :: l) = f a :: List.map f l
• List.map.eq_2 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) (a : α) (as : List α) : List.map f (a :: as) = f a :: List.map f as
• List.nil_zipWithAll 📋 Init.Data.List.Basic
  {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : Option α✝ → Option α✝¹ → α✝²} {bs : List α✝¹} : List.zipWithAll f [] bs = List.map (fun b => f none (some b)) bs
• List.zipWithAll_nil 📋 Init.Data.List.Basic
  {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : Option α✝ → Option α✝¹ → α✝²} {as : List α✝} : List.zipWithAll f as [] = List.map (fun a => f (some a) none) as
• List.mapTR_loop_eq 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} {f : α → β} {as : List α} {bs : List β} : List.mapTR.loop f as bs = bs.reverse ++ List.map f as
• List.map_id 📋 Init.Data.List.Lemmas
  {α : Type u_1} (l : List α) : List.map id l = l
• List.map_id' 📋 Init.Data.List.Lemmas
  {α : Type u_1} (l : List α) : List.map (fun a => a) l = l
• List.map_id_fun 📋 Init.Data.List.Lemmas
  {α : Type u_1} : List.map id = id
• List.map_id_fun' 📋 Init.Data.List.Lemmas
  {α : Type u_1} : (List.map fun a => a) = id
• List.isEmpty_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} : (List.map f l).isEmpty = l.isEmpty
• List.length_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {as : List α} (f : α → β) : (List.map f as).length = as.length
• List.map_const' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {b : β} : List.map (fun x => b) l = List.replicate l.length b
• List.map_id'' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {f : α → α} (h : ∀ (x : α), f x = x) (l : List α) : List.map f l = l
• List.filterMap_eq_map' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} : (List.filterMap fun x => some (f x)) = List.map f
• List.eq_nil_of_map_eq_nil 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} (h : List.map f l = []) : l = []
• List.map_const 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {b : β} : List.map (Function.const α b) l = List.replicate l.length b
• List.map_replicate 📋 Init.Data.List.Lemmas
  {n : ℕ} {α✝ : Type u_1} {a : α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : List.map f (List.replicate n a) = List.replicate n (f a)
• List.bind_def 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : List.flatMap f l = (List.map f l).flatten
• List.flatMap_def 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : List.flatMap f l = (List.map f l).flatten
• List.getLast?_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : (List.map f l).getLast? = Option.map f l.getLast?
• List.getLastD_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {a : α} : (List.map f l).getLastD (f a) = f (l.getLastD a)
• List.head?_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : (List.map f l).head? = Option.map f l.head?
• List.headD_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {a : α} : (List.map f l).headD (f a) = f (l.headD a)
• List.map_const_fun 📋 Init.Data.List.Lemmas
  {β : Type u_1} {α : Type u_2} {x : β} : List.map (Function.const α x) = fun x_1 => List.replicate x_1.length x
• List.map_dropLast 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l.dropLast = (List.map f l).dropLast
• List.map_eq_nil 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l = [] ↔ l = []
• List.map_eq_nil_iff 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l = [] ↔ l = []
• List.map_reverse 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l.reverse = (List.map f l).reverse
• List.map_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} : List.map f [a] = [f a]
• List.map_tail 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l.tail = (List.map f l).tail
• List.filterMap_eq_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} : List.filterMap (some ∘ f) = List.map f
• List.flatten_flatten 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List (List α))} : L.flatten.flatten = (List.map List.flatten L).flatten
• List.flatten_reverse 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List α)} : L.reverse.flatten = (List.map List.reverse L).flatten.reverse
• List.join_join 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List (List α))} : L.flatten.flatten = (List.map List.flatten L).flatten
• List.join_reverse 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List α)} : L.reverse.flatten = (List.map List.reverse L).flatten.reverse
• List.length_flatten 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List α)} : L.flatten.length = (List.map List.length L).sum
• List.length_join 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List α)} : L.flatten.length = (List.map List.length L).sum
• List.map_eq_bind 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l = List.flatMap (fun x => [f x]) l
• List.map_eq_flatMap 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l = List.flatMap (fun x => [f x]) l
• List.map_inj 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} : List.map f = List.map g ↔ f = g
• List.reverse_flatten 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List α)} : L.flatten.reverse = (List.map List.reverse L).reverse.flatten
• List.reverse_join 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List α)} : L.flatten.reverse = (List.map List.reverse L).reverse.flatten
• List.filter_flatten 📋 Init.Data.List.Lemmas
  {α : Type u_1} {p : α → Bool} {L : List (List α)} : List.filter p L.flatten = (List.map (List.filter p) L).flatten
• List.filter_join 📋 Init.Data.List.Lemmas
  {α : Type u_1} {p : α → Bool} {L : List (List α)} : List.filter p L.flatten = (List.map (List.filter p) L).flatten
• List.all_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {p : β → Bool} : (List.map f l).all p = l.all (p ∘ f)
• List.any_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {p : β → Bool} : (List.map f l).any p = l.any (p ∘ f)
• List.map_concat 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {l : List α} : List.map f (l.concat a) = (List.map f l).concat (f a)
• List.mem_map_of_mem 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {a : α} {f : α → β} (h : a ∈ l) : f a ∈ List.map f l
• List.map_eq_foldr 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l = List.foldr (fun a bs => f a :: bs) [] l
• List.map_flatten 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {L : List (List α)} : List.map f L.flatten = (List.map (List.map f) L).flatten
• List.map_join 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {L : List (List α)} : List.map f L.flatten = (List.map (List.map f) L).flatten
• List.map_tail? 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : Option.map (List.map f) l.tail? = (List.map f l).tail?
• List.bind_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → List γ) (l : List α) : List.flatMap g (List.map f l) = List.flatMap (fun a => g (f a)) l
• List.contains_map 📋 Init.Data.List.Lemmas
  {β : Type u_1} {α : Type u_2} [BEq β] {l : List α} {x : β} {f : α → β} : (List.map f l).contains x = l.any fun a => x == f a
• List.filterMap_flatten 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → Option β} {L : List (List α)} : List.filterMap f L.flatten = (List.map (List.filterMap f) L).flatten
• List.filterMap_join 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → Option β} {L : List (List α)} : List.filterMap f L.flatten = (List.map (List.filterMap f) L).flatten
• List.flatMap_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → List γ) (l : List α) : List.flatMap g (List.map f l) = List.flatMap (fun a => g (f a)) l
• List.map_set 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : ℕ} {a : α} : List.map f (l.set i a) = (List.map f l).set i (f a)
• List.set_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : ℕ} {a : α} : (List.map f l).set i (f a) = List.map f (l.set i a)
• List.map_map 📋 Init.Data.List.Lemmas
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {g : β → γ} {f : α → β} {l : List α} : List.map g (List.map f l) = List.map (g ∘ f) l
• List.tailD_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l l' : List α} : (List.map f l).tailD (List.map f l') = List.map f (l.tailD l')
• List.filter_map 📋 Init.Data.List.Lemmas
  {β : Type u_1} {α : Type u_2} {f : β → α} {p : α → Bool} {l : List β} : List.filter p (List.map f l) = List.map f (List.filter (p ∘ f) l)
• List.length_flatMap 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : (List.flatMap f l).length = (List.map (fun a => (f a).length) l).sum
• List.filterMap_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → Option γ} {l : List α} : List.filterMap g (List.map f l) = List.filterMap (g ∘ f) l
• List.map_bind 📋 Init.Data.List.Lemmas
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {g : α → List β} {l : List α} : List.map f (List.flatMap g l) = List.flatMap (fun a => List.map f (g a)) l
• List.map_filterMap 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {l : List α} : List.map g (List.filterMap f l) = List.filterMap (fun x => Option.map g (f x)) l
• List.map_flatMap 📋 Init.Data.List.Lemmas
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {g : α → List β} {l : List α} : List.map f (List.flatMap g l) = List.flatMap (fun a => List.map f (g a)) l
• List.foldl_map 📋 Init.Data.List.Lemmas
  {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {f : β₁ → β₂} {g : α → β₂ → α} {l : List β₁} {init : α} : List.foldl g init (List.map f l) = List.foldl (fun x y => g x (f y)) init l
• List.foldr_map 📋 Init.Data.List.Lemmas
  {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {f : α₁ → α₂} {g : α₂ → β → β} {l : List α₁} {init : β} : List.foldr g init (List.map f l) = List.foldr (fun x y => g (f x) y) init l
• List.map_filterMap_of_inv 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → Option β} {g : β → α} (H : ∀ (x : α), Option.map g (f x) = some x) {l : List α} : List.map g (List.filterMap f l) = l
• List.exists_of_mem_map 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {l : List α✝} {b : α✝¹} (h : b ∈ List.map f l) : ∃ a ∈ l, f a = b
• List.forall_mem_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {P : β → Prop} : (∀ i ∈ List.map f l, P i) ↔ ∀ j ∈ l, P (f j)
• List.map_congr_left 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {l : List α✝} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} (h : ∀ a ∈ l, f a = g a) : List.map f l = List.map g l
• List.map_eq_replicate_iff 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {b : β} : List.map f l = List.replicate l.length b ↔ ∀ x ∈ l, f x = b
• List.map_filterMap_some_eq_filter_map_isSome 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} : List.map some (List.filterMap f l) = List.filter (fun b => b.isSome) (List.map f l)
• List.map_eq_map_iff 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {l : List α✝} {g : α✝ → α✝¹} : List.map f l = List.map g l ↔ ∀ a ∈ l, f a = g a
• List.map_inj_left 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f g : α → β} : List.map f l = List.map g l ↔ ∀ a ∈ l, f a = g a
• List.mem_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {l : List α} : b ∈ List.map f l ↔ ∃ a ∈ l, f a = b
• 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.map_inj_right 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l l' : List α} {f : α → β} (w : ∀ (x y : α), f x = f y → x = y) : List.map f l = List.map f l' ↔ l = l'
• List.map_filter_eq_foldr 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {p : α → Bool} {as : List α} : List.map f (List.filter p as) = List.foldr (fun a bs => bif p a then f a :: bs else bs) [] as
• List.eq_iff_flatten_eq 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L L' : List (List α)} : L = L' ↔ L.flatten = L'.flatten ∧ List.map List.length L = List.map List.length L'
• List.eq_iff_join_eq 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L L' : List (List α)} : L = L' ↔ L.flatten = L'.flatten ∧ List.map List.length L = List.map List.length L'
• List.foldr_cons_eq_append 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {l' : List β} : List.foldr (fun x ys => f x :: ys) l' l = List.map f l ++ l'
• List.foldl_flip_cons_eq_append 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {l' : List β} : List.foldl (fun xs y => f y :: xs) l' l = (List.map f l).reverse ++ l'
• List.foldl_map' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {l : List α} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : List.foldl f' (g a) (List.map g l) = g (List.foldl f a l)
• List.foldl_map_hom 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {l : List α} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : List.foldl f' (g a) (List.map g l) = g (List.foldl f a l)
• List.foldr_map' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {l : List α} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : List.foldr f' (g a) (List.map g l) = g (List.foldr f a l)
• List.foldr_map_hom 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {l : List α} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : List.foldr f' (g a) (List.map g l) = g (List.foldr f a l)
• List.map_append 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ l₂ : List α} : List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂
• List.map_eq_cons 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α} : List.map f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f a = b ∧ List.map f l₁ = l₂
• List.map_eq_cons_iff 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α} : List.map f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f a = b ∧ List.map f l₁ = l₂
• List.getElem?_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : ℕ} : (List.map f l)[i]? = Option.map f l[i]?
• List.map_eq_cons' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α} : List.map f l = b :: l₂ ↔ Option.map f l.head? = some b ∧ Option.map (List.map f) l.tail? = some l₂
• List.map_eq_cons_iff' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α} : List.map f l = b :: l₂ ↔ Option.map f l.head? = some b ∧ Option.map (List.map f) l.tail? = some l₂
• List.foldl_append_eq_append 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β} : List.foldl (fun x1 x2 => x1 ++ f x2) l' l = l' ++ (List.map f l).flatten
• List.foldr_append_eq_append 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β} : List.foldr (fun x1 x2 => f x1 ++ x2) l' l = (List.map f l).flatten ++ l'
• List.foldl_flip_append_eq_append 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β} : List.foldl (fun xs y => f y ++ xs) l' l = (List.map f l).reverse.flatten ++ l'
• List.foldr_flip_append_eq_append 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β} : List.foldr (fun x ys => ys ++ f x) l' l = l' ++ (List.map f l).reverse.flatten
• List.map_eq_iff 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {l : List α✝} {l' : List α✝¹} : List.map f l = l' ↔ ∀ (i : ℕ), l'[i]? = Option.map f l[i]?
• List.append_eq_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {L₁ L₂ : List β} {l : List α} {f : α → β} : L₁ ++ L₂ = List.map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.map f l₁ = L₁ ∧ List.map f l₂ = L₂
• List.append_eq_map_iff 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {L₁ L₂ : List β} {l : List α} {f : α → β} : L₁ ++ L₂ = List.map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.map f l₁ = L₁ ∧ List.map f l₂ = L₂
• List.getLast_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} (h : List.map f l ≠ []) : (List.map f l).getLast h = f (l.getLast ⋯)
• List.head_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} (w : List.map f l ≠ []) : (List.map f l).head w = f (l.head ⋯)
• List.map_eq_append 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {L₁ L₂ : List β} {f : α → β} : List.map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.map f l₁ = L₁ ∧ List.map f l₂ = L₂
• List.map_eq_append_iff 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} {l : List α} {L₁ L₂ : List β} {f : α → β} : List.map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.map f l₁ = L₁ ∧ List.map f l₂ = L₂
• List.getElem_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} {i : ℕ} {h : i < (List.map f l).length} : (List.map f l)[i] = f l[i]
• List.map_drop 📋 Init.Data.List.TakeDrop
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : ℕ} : List.map f (List.drop i l) = List.drop i (List.map f l)
• List.map_take 📋 Init.Data.List.TakeDrop
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : ℕ} : List.map f (List.take i l) = List.take i (List.map f l)
• List.dropWhile_map 📋 Init.Data.List.TakeDrop
  {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Bool} {l : List α} : List.dropWhile p (List.map f l) = List.map f (List.dropWhile (p ∘ f) l)
• List.takeWhile_map 📋 Init.Data.List.TakeDrop
  {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Bool} {l : List α} : List.takeWhile p (List.map f l) = List.map f (List.takeWhile (p ∘ f) l)
• List.zipWith_same 📋 Init.Data.List.Zip
  {α : Type u_1} {δ : Type u_2} {f : α → α → δ} {l : List α} : List.zipWith f l l = List.map (fun a => f a a) l
• List.zipWith_self 📋 Init.Data.List.Zip
  {α : Type u_1} {δ : Type u_2} {f : α → α → δ} {l : List α} : List.zipWith f l l = List.map (fun a => f a a) l
• List.unzip_fst 📋 Init.Data.List.Zip
  {α✝ : Type u_1} {β✝ : Type u_2} {l : List (α✝ × β✝)} : l.unzip.1 = List.map Prod.fst l
• List.unzip_snd 📋 Init.Data.List.Zip
  {α✝ : Type u_1} {β✝ : Type u_2} {l : List (α✝ × β✝)} : l.unzip.2 = List.map Prod.snd l
• List.map_fst_zip 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} : l₁.length ≤ l₂.length → List.map Prod.fst (l₁.zip l₂) = l₁
• List.map_snd_zip 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} : l₂.length ≤ l₁.length → List.map Prod.snd (l₁.zip l₂) = l₂
• List.map_prod_left_eq_zip 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} : List.map (fun x => (x, f x)) l = l.zip (List.map f l)
• List.map_prod_right_eq_zip 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} : List.map (fun x => (f x, x)) l = (List.map f l).zip l
• List.map_uncurry_zip_eq_zipWith 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l : List α} {l' : List β} : List.map (Function.uncurry f) (l.zip l') = List.zipWith f l l'
• List.map_zip_eq_zipWith 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {l : List α} {l' : List β} : List.map f (l.zip l') = List.zipWith (Function.curry f) l l'
• List.map_zipWith 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : γ → δ → α} {l : List γ} {l' : List δ} : List.map f (List.zipWith g l l') = List.zipWith (fun x y => f (g x y)) l l'
• List.unzip_eq_map 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {l : List (α × β)} : l.unzip = (List.map Prod.fst l, List.map Prod.snd l)
• List.zipWith_map_left 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} {l₁ : List α} {l₂ : List β} {f : α → α'} {g : α' → β → γ} : List.zipWith g (List.map f l₁) l₂ = List.zipWith (fun a b => g (f a) b) l₁ l₂
• List.zipWith_map_right 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} {l₁ : List α} {l₂ : List β} {f : β → β'} {g : α → β' → γ} : List.zipWith g l₁ (List.map f l₂) = List.zipWith (fun a b => g a (f b)) l₁ l₂
• List.zip_map' 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {l : List α} : (List.map f l).zip (List.map g l) = List.map (fun a => (f a, g a)) l
• List.map_zipWithAll 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : Option γ → Option δ → α} {l : List γ} {l' : List δ} : List.map f (List.zipWithAll g l l') = List.zipWithAll (fun x y => f (g x y)) l l'
• List.zip_map_left 📋 Init.Data.List.Zip
  {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : α → γ} {l₁ : List α} {l₂ : List β} : (List.map f l₁).zip l₂ = List.map (Prod.map f id) (l₁.zip l₂)
• List.zip_map_right 📋 Init.Data.List.Zip
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {l₁ : List α} {l₂ : List β} : l₁.zip (List.map f l₂) = List.map (Prod.map id f) (l₁.zip l₂)
• List.zipWith_map 📋 Init.Data.List.Zip
  {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {μ : Type u_5} {f : γ → δ → μ} {g : α → γ} {h : β → δ} {l₁ : List α} {l₂ : List β} : List.zipWith f (List.map g l₁) (List.map h l₂) = List.zipWith (fun a b => f (g a) (h b)) l₁ l₂
• List.zip_of_prod 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {l : List α} {l' : List β} {xs : List (α × β)} (hl : List.map Prod.fst xs = l) (hr : List.map Prod.snd xs = l') : xs = l.zip l'
• List.zipWithAll_map_left 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {α' : Type u_1} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {f : α → α'} {g : Option α' → Option β → γ} : List.zipWithAll g (List.map f l₁) l₂ = List.zipWithAll (fun a b => g (f <$> a) b) l₁ l₂
• List.zipWithAll_map_right 📋 Init.Data.List.Zip
  {α : Type u_1} {β β' : Type u_2} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {f : β → β'} {g : Option α → Option β' → γ} : List.zipWithAll g l₁ (List.map f l₂) = List.zipWithAll (fun a b => g a (f <$> b)) l₁ l₂
• List.zip_map 📋 Init.Data.List.Zip
  {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} {l₁ : List α} {l₂ : List β} : (List.map f l₁).zip (List.map g l₂) = List.map (Prod.map f g) (l₁.zip l₂)
• List.zipWithAll_map 📋 Init.Data.List.Zip
  {γ : Type u_1} {δ : Type u_2} {α : Type u_1} {β : Type u_2} {μ : Type u_3} {f : Option γ → Option δ → μ} {g : α → γ} {h : β → δ} {l₁ : List α} {l₂ : List β} : List.zipWithAll f (List.map g l₁) (List.map h l₂) = List.zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂
• Lean.Omega.IntList.neg_def 📋 Init.Omega.IntList
  (xs : Lean.Omega.IntList) : -xs = List.map (fun x => -x) xs
• Lean.Omega.IntList.smul_def 📋 Init.Omega.IntList
  (xs : Lean.Omega.IntList) (i : ℤ) : i * xs = List.map (fun x => i * x) xs
• Lean.Omega.IntList.get_map 📋 Init.Omega.IntList
  {f : ℤ → ℤ} {i : ℕ} {xs : Lean.Omega.IntList} (h : f 0 = 0) : Lean.Omega.IntList.get (List.map f xs) i = f (xs.get i)
• 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.IsPrefix.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.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.Sublist.map 📋 Init.Data.List.Sublist
  {α : Type u_1} {β : Type u_2} (f : α → β) {l₁ l₂ : List α} (s : l₁.Sublist l₂) : (List.map f l₁).Sublist (List.map f l₂)
• List.map_subset 📋 Init.Data.List.Sublist
  {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : List.map f l₁ ⊆ List.map f 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.isPrefix_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_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.sublist_map_iff 📋 Init.Data.List.Sublist
  {β : Type u_1} {α : Type u_2} {l₂ : List α} {l₁ : List β} {f : α → β} : l₁.Sublist (List.map f l₂) ↔ ∃ l', l'.Sublist l₂ ∧ l₁ = List.map f l'
• List.countP_map 📋 Init.Data.List.Count
  {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → β} {l : List α} : List.countP p (List.map f l) = List.countP (p ∘ f) l
• List.countP_flatten 📋 Init.Data.List.Count
  {α : Type u_1} {p : α → Bool} {l : List (List α)} : List.countP p l.flatten = (List.map (List.countP p) l).sum
• List.countP_join 📋 Init.Data.List.Count
  {α : Type u_1} {p : α → Bool} {l : List (List α)} : List.countP p l.flatten = (List.map (List.countP p) l).sum
• List.count_flatten 📋 Init.Data.List.Count
  {α : Type u_1} [BEq α] {a : α} {l : List (List α)} : List.count a l.flatten = (List.map (List.count a) l).sum
• List.count_join 📋 Init.Data.List.Count
  {α : Type u_1} [BEq α] {a : α} {l : List (List α)} : List.count a l.flatten = (List.map (List.count a) l).sum
• List.count_le_count_map 📋 Init.Data.List.Count
  {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} [BEq β] [LawfulBEq β] {l : List α} {f : α → β} {x : α} : List.count x l ≤ List.count (f x) (List.map f l)
• List.countP_flatMap 📋 Init.Data.List.Count
  {α : Type u_2} {β : Type u_1} {p : β → Bool} {l : List α} {f : α → List β} : List.countP p (List.flatMap f l) = (List.map (List.countP p ∘ f) l).sum
• List.count_flatMap 📋 Init.Data.List.Count
  {β : Type u_1} {α : Type u_2} [BEq β] {l : List α} {f : α → List β} {x : β} : List.count x (List.flatMap f l) = (List.map (List.count x ∘ f) l).sum
• List.map_wfParam 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → β} : List.map f (wfParam xs) = List.map f xs.attach.unattach
• List.attach_map_subtype_val 📋 Init.Data.List.Attach
  {α : Type u_1} (l : List α) : List.map Subtype.val l.attach = l
• List.unattach.eq_1 📋 Init.Data.List.Attach
  {α : Type u_1} {p : α → Prop} (l : List { x // p x }) : l.unattach = List.map (fun x => ↑x) l
• List.attachWith_map_subtype_val 📋 Init.Data.List.Attach
  {α : Type u_1} {p : α → Prop} {l : List α} (H : ∀ a ∈ l, p a) : List.map Subtype.val (l.attachWith p H) = l
• List.pmap_eq_map 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : α → β} {l : List α} (H : ∀ a ∈ l, p a) : List.pmap (fun a x => f a) l H = List.map f l
• List.unattach_flatten 📋 Init.Data.List.Attach
  {α : Type u_1} {p : α → Prop} {l : List (List { x // p x })} : l.flatten.unattach = (List.map List.unattach l).flatten
• List.unattach_join 📋 Init.Data.List.Attach
  {α : Type u_1} {p : α → Prop} {l : List (List { x // p x })} : l.flatten.unattach = (List.map List.unattach l).flatten
• List.attachWith_map_coe 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : α → β} {l : List α} (H : ∀ a ∈ l, p a) : List.map (fun i => f ↑i) (l.attachWith p H) = List.map f l
• List.attachWith_map_val 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : α → β} {l : List α} (H : ∀ a ∈ l, p a) : List.map (fun i => f ↑i) (l.attachWith p H) = List.map f l
• List.map_pmap 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} {g : β → γ} {f : (a : α) → p a → β} {l : List α} (H : ∀ a ∈ l, p a) : List.map g (List.pmap f l H) = List.pmap (fun a h => g (f a h)) l H
• List.map_subtype 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → β} {g : α → β} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : List.map f l = List.map g l.unattach
• List.attach_map_coe 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} : List.map (fun i => f ↑i) l.attach = List.map f l
• List.attach_map_val 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} : List.map (fun i => f ↑i) l.attach = List.map f l
• List.map_unattach 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : List (Subtype P)} {f : α → β} : List.map f xs.unattach = List.map (fun x => match x with | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x)))) xs
• List.pmap_map 📋 Init.Data.List.Attach
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {p : β → Prop} {g : (b : β) → p b → γ} {f : α → β} {l : List α} (H : ∀ a ∈ List.map f l, p a) : List.pmap g (List.map f l) H = List.pmap (fun a h => g (f a) h) l ⋯
• List.map_attach 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {l : List α} {f : { x // x ∈ l } → β} : List.map f l.attach = List.pmap (fun a h => f ⟨a, h⟩) l ⋯
• List.map_attach_eq_pmap 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {l : List α} {f : { x // x ∈ l } → β} : List.map f l.attach = List.pmap (fun a h => f ⟨a, h⟩) l ⋯
• List.pmap_eq_map_attach 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} (H : ∀ a ∈ l, p a) : List.pmap f l H = List.map (fun x => f ↑x ⋯) l.attach
• List.map_attachWith 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {l : List α} {P : α → Prop} {H : ∀ a ∈ l, P a} {f : { x // P x } → β} : List.map f (l.attachWith P H) = List.map (fun x => match x with | ⟨x, h⟩ => f ⟨x, ⋯⟩) l.attach
• List.map_attachWith_eq_pmap 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {l : List α} {P : α → Prop} {H : ∀ a ∈ l, P a} {f : { x // P x } → β} : List.map f (l.attachWith P H) = List.pmap (fun a h => f ⟨a, ⋯⟩) l ⋯
• List.attachWith_map 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {P : β → Prop} (H : ∀ b ∈ List.map f l, P b) : (List.map f l).attachWith P H = List.map (fun x => match x with | ⟨x, h⟩ => ⟨f x, h⟩) (l.attachWith (P ∘ f) ⋯)
• List.tail_attach 📋 Init.Data.List.Attach
  {α : Type u_1} {xs : List α} : xs.attach.tail = List.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.tail.attach
• List.attach_map 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} : (List.map f l).attach = List.map (fun x => match x with | ⟨x, h⟩ => ⟨f x, ⋯⟩) l.attach
• List.attach_congr 📋 Init.Data.List.Attach
  {α : Type u_1} {l₁ l₂ : List α} (h : l₁ = l₂) : l₁.attach = List.map (fun x => ⟨↑x, ⋯⟩) l₂.attach
• List.reverse_attach 📋 Init.Data.List.Attach
  {α : Type u_1} {xs : List α} : xs.attach.reverse = List.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.reverse.attach
• List.attach_cons 📋 Init.Data.List.Attach
  {α : Type u_1} {x : α} {xs : List α} : (x :: xs).attach = ⟨x, ⋯⟩ :: List.map (fun x_1 => match x_1 with | ⟨y, h⟩ => ⟨y, ⋯⟩) xs.attach
• List.filter_attachWith 📋 Init.Data.List.Attach
  {α : Type u_1} {q : α → Prop} {l : List α} {p : { x // q x } → Bool} (H : ∀ x ∈ l, q x) : List.filter p (l.attachWith q H) = List.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) (List.filter (fun x => match x with | ⟨x, h⟩ => p ⟨x, ⋯⟩) l.attach)
• List.attach_reverse 📋 Init.Data.List.Attach
  {α : Type u_1} {xs : List α} : xs.reverse.attach = List.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach.reverse
• List.attach_append 📋 Init.Data.List.Attach
  {α : Type u_1} {xs ys : List α} : (xs ++ ys).attach = List.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach ++ List.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) ys.attach
• List.pairwise_map 📋 Init.Data.List.Pairwise
  {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {R : α✝ → α✝ → Prop} {l : List α} : List.Pairwise R (List.map f l) ↔ List.Pairwise (fun a b => R (f a) (f b)) l
• List.Pairwise.map 📋 Init.Data.List.Pairwise
  {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {l : List α} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), R a b → S (f a) (f b)) (p : List.Pairwise R l) : List.Pairwise S (List.map f l)
• List.Pairwise.of_map 📋 Init.Data.List.Pairwise
  {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {l : List α} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), S (f a) (f b) → R a b) (p : List.Pairwise S (List.map f l)) : List.Pairwise R l
• List.enumFrom_map_snd 📋 Init.Data.List.Range
  {α : Type u_1} (n : ℕ) (l : List α) : List.map Prod.snd (List.enumFrom n l) = l
• List.zipIdx_map_fst 📋 Init.Data.List.Range
  {α : Type u_1} (i : ℕ) (l : List α) : List.map Prod.fst (l.zipIdx i) = l
• List.range'_eq_map_range 📋 Init.Data.List.Range
  {s n : ℕ} : List.range' s n = List.map (fun x => s + x) (List.range n)
• List.enumFrom_map_fst 📋 Init.Data.List.Range
  {α : Type u_1} (n : ℕ) (l : List α) : List.map Prod.fst (List.enumFrom n l) = List.range' n l.length
• List.zipIdx_map_snd 📋 Init.Data.List.Range
  {α : Type u_1} (i : ℕ) (l : List α) : List.map Prod.snd (l.zipIdx i) = List.range' i l.length
• List.range_succ_eq_map 📋 Init.Data.List.Range
  {n : ℕ} : List.range (n + 1) = 0 :: List.map Nat.succ (List.range n)
• List.map_add_range' 📋 Init.Data.List.Range
  {a : ℕ} (s n step : ℕ) : List.map (fun x => a + x) (List.range' s n step) = List.range' (a + s) n step
• List.enumFrom_eq_map_enum 📋 Init.Data.List.Range
  {α : Type u_1} (l : List α) (n : ℕ) : List.enumFrom n l = List.map (Prod.map (fun x => x + n) id) l.enum

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 19971e9 serving mathlib revision bce1d65