Loogle!

Result

Found 203 declarations mentioning Array.map. Of these, only the first 200 are shown.

• Array.map 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β
• Array.map_id 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (xs : Array α) : Array.map id xs = xs
• Array.map_id' 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (xs : Array α) : Array.map (fun a => a) xs = xs
• Array.map_id_fun 📋 Init.Data.Array.Lemmas
  {α : Type u_1} : Array.map id = id
• Array.map_id_fun' 📋 Init.Data.Array.Lemmas
  {α : Type u_1} : (Array.map fun a => a) = id
• Array.size_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} : (Array.map f xs).size = xs.size
• Array.map_empty 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} : Array.map f #[] = #[]
• Array.map_const' 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {b : β} : Array.map (fun x => b) xs = Array.replicate xs.size b
• Array.map_id'' 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {f : α → α} (h : ∀ (x : α), f x = x) (xs : Array α) : Array.map f xs = xs
• Array.map_const 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {b : β} : Array.map (Function.const α b) xs = Array.replicate xs.size b
• Array.map_mkArray 📋 Init.Data.Array.Lemmas
  {n : ℕ} {α✝ : Type u_1} {a : α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Array.map f (Array.replicate n a) = Array.replicate n (f a)
• Array.map_replicate 📋 Init.Data.Array.Lemmas
  {n : ℕ} {α✝ : Type u_1} {a : α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Array.map f (Array.replicate n a) = Array.replicate n (f a)
• Array.back?_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} : (Array.map f xs).back? = Option.map f xs.back?
• Array.flatMap_def 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} : Array.flatMap f xs = (Array.map f xs).flatten
• Array.map_const_fun 📋 Init.Data.Array.Lemmas
  {β : Type u_1} {α : Type u_2} {x : β} : Array.map (Function.const α x) = fun x_1 => Array.replicate x_1.size x
• Array.map_pop 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} : Array.map f xs.pop = (Array.map f xs).pop
• Array.map_reverse 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} : Array.map f xs.reverse = (Array.map f xs).reverse
• Array.toList_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} : (Array.map f xs).toList = List.map f xs.toList
• List.map_toArray 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : Array.map f l.toArray = (List.map f l).toArray
• Array.map.eq_1 📋 Init.Data.Array.Lemmas
  {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array.map f as = (Array.mapM f as).run
• Array.flatten_flatten 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xss : Array (Array (Array α))} : xss.flatten.flatten = (Array.map Array.flatten xss).flatten
• Array.flatten_map_toArray 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {L : List (List α)} : (Array.map List.toArray L.toArray).flatten = L.flatten.toArray
• Array.flatten_reverse 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xss : Array (Array α)} : xss.reverse.flatten = (Array.map Array.reverse xss).flatten.reverse
• Array.map_inj 📋 Init.Data.Array.Lemmas
  {α✝ : Type u_1} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} : Array.map f = Array.map g ↔ f = g
• Array.reverse_flatten 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xss : Array (Array α)} : xss.flatten.reverse = (Array.map Array.reverse xss).reverse.flatten
• List.flatten_toArray 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {L : List (List α)} : (Array.map List.toArray L.toArray).flatten = L.flatten.toArray
• Array.size_flatten 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xss : Array (Array α)} : xss.flatten.size = (Array.map Array.size xss).sum
• Array.eq_empty_of_map_eq_empty 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} (h : Array.map f xs = #[]) : xs = #[]
• Array.fst_unzip 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array (α × β)} : xs.unzip.1 = Array.map Prod.fst xs
• Array.map_eq_empty_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} : Array.map f xs = #[] ↔ xs = #[]
• Array.map_eq_flatMap 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} : Array.map f xs = Array.flatMap (fun x => #[f x]) xs
• Array.map_push 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {as : Array α} {x : α} : Array.map f (as.push x) = (Array.map f as).push (f x)
• Array.map_singleton 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} : Array.map f #[a] = #[f a]
• Array.snd_unzip 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array (α × β)} : xs.unzip.2 = Array.map Prod.snd xs
• Array.mem_map_of_mem 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {l : Array α} {a : α} {f : α → β} (h : a ∈ l) : f a ∈ Array.map f l
• Array.map_flatten 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xss : Array (Array α)} : Array.map f xss.flatten = (Array.map (Array.map f) xss).flatten
• Array.flatMap_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → Array γ} {xs : Array α} : Array.flatMap g (Array.map f xs) = Array.flatMap (fun a => g (f a)) xs
• Array.map_setIfInBounds 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {i : ℕ} {a : α} : Array.map f (xs.setIfInBounds i a) = (Array.map f xs).setIfInBounds i (f a)
• Array.map_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {as : Array α} : Array.map g (Array.map f as) = Array.map (g ∘ f) as
• Array.size_flatMap 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} : (Array.flatMap f xs).size = (Array.map (fun a => (f a).size) xs).sum
• Array.map_flatMap 📋 Init.Data.Array.Lemmas
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {g : α → Array β} {xs : Array α} : Array.map f (Array.flatMap g xs) = Array.flatMap (fun a => Array.map f (g a)) xs
• Array.exists_of_mem_map 📋 Init.Data.Array.Lemmas
  {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {l : Array α✝} {b : α✝¹} (h : b ∈ Array.map f l) : ∃ a ∈ l, f a = b
• Array.filterMap_eq_map' 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {stop : ℕ} {as : Array α} {f : α → β} (w : stop = as.size) : Array.filterMap (fun x => some (f x)) as 0 stop = Array.map f as
• Array.forall_mem_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {P : β → Prop} : (∀ i ∈ Array.map f xs, P i) ↔ ∀ j ∈ xs, P (f j)
• Array.map_congr_left 📋 Init.Data.Array.Lemmas
  {α✝ : Type u_1} {xs : Array α✝} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} (h : ∀ a ∈ xs, f a = g a) : Array.map f xs = Array.map g xs
• Array.map_eq_mkArray_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} {b : β} : Array.map f xs = Array.replicate xs.size b ↔ ∀ x ∈ xs, f x = b
• Array.map_eq_replicate_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} {b : β} : Array.map f xs = Array.replicate xs.size b ↔ ∀ x ∈ xs, f x = b
• Array.map_eq_map_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f g : α → β} {xs : Array α} : Array.map f xs = Array.map g xs ↔ ∀ a ∈ xs, f a = g a
• Array.map_inj_left 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f g : α → β} : Array.map f xs = Array.map g xs ↔ ∀ a ∈ xs, f a = g a
• Array.mem_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {xs : Array α} : b ∈ Array.map f xs ↔ ∃ a ∈ xs, f a = b
• Array.contains_map 📋 Init.Data.Array.Lemmas
  {β : Type u_1} {α : Type u_2} [BEq β] {xs : Array α} {x : β} {f : α → β} : (Array.map f xs).contains x = xs.any fun a => x == f a
• Array.filterMap_eq_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {stop : ℕ} {as : Array α} {f : α → β} (w : stop = as.size) : Array.filterMap (some ∘ f) as 0 stop = Array.map f as
• Array.map_eq_foldl 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} : Array.map f xs = Array.foldl (fun bs a => bs.push (f a)) #[] xs
• Array.map_inj_right 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs ys : Array α} {f : α → β} (w : ∀ (x y : α), f x = f y → x = y) : Array.map f xs = Array.map f ys ↔ xs = ys
• Array.eq_iff_flatten_eq 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xss₁ xss₂ : Array (Array α)} : xss₁ = xss₂ ↔ xss₁.flatten = xss₂.flatten ∧ Array.map Array.size xss₁ = Array.map Array.size xss₂
• Array.map_eq_singleton_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {b : β} : Array.map f xs = #[b] ↔ ∃ a, xs = #[a] ∧ f a = b
• Array.map_filterMap_of_inv 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → Option β} {g : β → α} (H : ∀ (x : α), Option.map g (f x) = some x) {xs : Array α} : Array.map g (Array.filterMap f xs) = xs
• Array.all_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {p : β → Bool} : (Array.map f xs).all p = xs.all (p ∘ f)
• Array.any_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {p : β → Bool} : (Array.map f xs).any p = xs.any (p ∘ f)
• Array.all_map' 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {stop : ℕ} {f : α → β} {xs : Array α} {p : β → Bool} (w : stop = xs.size) : (Array.map f xs).all p 0 stop = xs.all (p ∘ f)
• Array.any_map' 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {stop : ℕ} {f : α → β} {xs : Array α} {p : β → Bool} (w : stop = xs.size) : (Array.map f xs).any p 0 stop = xs.any (p ∘ f)
• Array.map_filterMap 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {xs : Array α} : Array.map g (Array.filterMap f xs) = Array.filterMap (fun x => Option.map g (f x)) xs
• Array.map_append 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs ys : Array α} : Array.map f (xs ++ ys) = Array.map f xs ++ Array.map f ys
• Array.filter_flatten 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {p : α → Bool} {xss : Array (Array α)} {stop : ℕ} (w : stop = xss.flatten.size) : Array.filter p xss.flatten 0 stop = (Array.map (fun as => Array.filter p as) xss).flatten
• Array.filter_map 📋 Init.Data.Array.Lemmas
  {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {xs : Array β} : Array.filter p (Array.map f xs) = Array.map f (Array.filter (p ∘ f) xs)
• Array.filterMap_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → Option γ} {xs : Array α} : Array.filterMap g (Array.map f xs) = Array.filterMap (g ∘ f) xs
• Array.foldl_map 📋 Init.Data.Array.Lemmas
  {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {f : β₁ → β₂} {g : α → β₂ → α} {xs : Array β₁} {init : α} : Array.foldl g init (Array.map f xs) = Array.foldl (fun x y => g x (f y)) init xs
• Array.foldr_map 📋 Init.Data.Array.Lemmas
  {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {f : α₁ → α₂} {g : α₂ → β → β} {xs : Array α₁} {init : β} : Array.foldr g init (Array.map f xs) = Array.foldr (fun x y => g (f x) y) init xs
• Array.map_eq_push_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {ys : Array β} {b : β} : Array.map f xs = ys.push b ↔ ∃ zs a, xs = zs.push a ∧ Array.map f zs = ys ∧ f a = b
• Array.foldl_map' 📋 Init.Data.Array.Lemmas
  {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {f : β₁ → β₂} {g : α → β₂ → α} {xs : Array β₁} {init : α} {stop : ℕ} (w : stop = xs.size) : Array.foldl g init (Array.map f xs) 0 stop = Array.foldl (fun x y => g x (f y)) init xs
• Array.foldr_map' 📋 Init.Data.Array.Lemmas
  {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {f : α₁ → α₂} {g : α₂ → β → β} {xs : Array α₁} {init : β} {start : ℕ} (w : start = xs.size) : Array.foldr g init (Array.map f xs) start = Array.foldr (fun x y => g (f x) y) init xs
• Array.filterMap_flatten 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → Option β} {xss : Array (Array α)} {stop : ℕ} (w : stop = xss.flatten.size) : Array.filterMap f xss.flatten 0 stop = (Array.map (fun as => Array.filterMap f as) xss).flatten
• Array.foldl_push_eq_append 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {stop : ℕ} {as : Array α} {bs : Array β} {f : α → β} (w : stop = as.size) : Array.foldl (fun acc a => acc.push (f a)) bs as 0 stop = bs ++ Array.map f as
• Array.getElem?_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {i : ℕ} : (Array.map f xs)[i]? = Option.map f xs[i]?
• Array.foldr_cons_eq_append 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {start : ℕ} {as : Array α} {bs : List β} {f : α → β} (w : start = as.size) : Array.foldr (fun a acc => f a :: acc) bs as start = (Array.map f as).toList ++ bs
• Array.foldr_flip_push_eq_append 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {start : ℕ} {as : Array α} {bs : Array β} {f : α → β} (w : start = as.size) : Array.foldr (fun a xs => xs.push (f a)) bs as start = bs ++ (Array.map f as).reverse
• Array.foldr_push_eq_append 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {start : ℕ} {as : Array α} {bs : Array β} {f : α → β} (w : start = as.size) : Array.foldr (fun a xs => xs.push (f a)) bs as start = bs ++ (Array.map f as).reverse
• Array.map_filterMap_some_eq_filterMap_isSome 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} : Array.map some (Array.filterMap f xs) = Array.filter (fun b => b.isSome) (Array.map f xs)
• Array.map_filter_eq_foldl 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {p : α → Bool} {xs : Array α} : Array.map f (Array.filter p xs) = Array.foldl (fun acc x => bif p x then acc.push (f x) else acc) #[] xs
• Array.foldl_cons_eq_append 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {stop : ℕ} {as : Array α} {bs : List β} {f : α → β} (w : stop = as.size) : Array.foldl (fun acc a => f a :: acc) bs as 0 stop = (Array.map f as).reverse.toList ++ bs
• Array.map_eq_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {ys : Array β} : Array.map f xs = ys ↔ ∀ (i : ℕ), ys[i]? = Option.map f xs[i]?
• Array.foldl_append_eq_append 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {ys : Array β} : Array.foldl (fun x1 x2 => x1 ++ f x2) ys xs = ys ++ (Array.map f xs).flatten
• Array.foldr_append_eq_append 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {ys : Array β} : Array.foldr (fun x1 x2 => f x1 ++ x2) ys xs = (Array.map f xs).flatten ++ ys
• Array.foldl_map_hom 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Array α} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : Array.foldl f' (g a) (Array.map g xs) = g (Array.foldl f a xs)
• Array.foldr_map_hom 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Array α} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : Array.foldr f' (g a) (Array.map g xs) = g (Array.foldr f a xs)
• Array.foldl_map_hom' 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Array α} {stop : ℕ} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) (w : stop = xs.size) : Array.foldl f' (g a) (Array.map g xs) 0 stop = g (Array.foldl f a xs)
• Array.foldr_map_hom' 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Array α} {start : ℕ} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) (w : start = xs.size) : Array.foldr f' (g a) (Array.map g xs) start = g (Array.foldr f a xs)
• Array.foldl_flip_append_eq_append 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {ys : Array β} : Array.foldl (fun acc y => f y ++ acc) ys xs = (Array.map f xs).reverse.flatten ++ ys
• Array.foldr_flip_append_eq_append 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {ys : Array β} : Array.foldr (fun x acc => acc ++ f x) ys xs = ys ++ (Array.map f xs).reverse.flatten
• Array.append_eq_map_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs ys : Array β} {zs : Array α} {f : α → β} : xs ++ ys = Array.map f zs ↔ ∃ as bs, zs = as ++ bs ∧ Array.map f as = xs ∧ Array.map f bs = ys
• Array.map_eq_append_iff 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array α} {ys zs : Array β} {f : α → β} : Array.map f xs = ys ++ zs ↔ ∃ as bs, xs = as ++ bs ∧ Array.map f as = ys ∧ Array.map f bs = zs
• Array.map_set 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {i : ℕ} {h : i < xs.size} {a : α} : Array.map f (xs.set i a h) = (Array.map f xs).set i (f a) ⋯
• Array.getElem_map 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} (f : α → β) {xs : Array α} {i : ℕ} (hi : i < (Array.map f xs).size) : (Array.map f xs)[i] = f xs[i]
• Array.map_spec 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → β) (p : Fin xs.size → β → Prop) (hs : ∀ (i : Fin xs.size), p i (f xs[i])) : ∃ (eq : (Array.map f xs).size = xs.size), ∀ (i : ℕ) (h : i < xs.size), p ⟨i, h⟩ (Array.map f xs)[i]
• Array.map_induction 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → β) (motive : ℕ → Prop) (h0 : motive 0) (p : Fin xs.size → β → Prop) (hs : ∀ (i : Fin xs.size), motive ↑i → p i (f xs[i]) ∧ motive (↑i + 1)) : motive xs.size ∧ ∃ (eq : (Array.map f xs).size = xs.size), ∀ (i : ℕ) (h : i < xs.size), p ⟨i, h⟩ (Array.map f xs)[i]
• Array.countP_map 📋 Init.Data.Array.Count
  {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → β} {xs : Array α} : Array.countP p (Array.map f xs) = Array.countP (p ∘ f) xs
• Array.countP_flatten 📋 Init.Data.Array.Count
  {α : Type u_1} {p : α → Bool} {xss : Array (Array α)} : Array.countP p xss.flatten = (Array.map (Array.countP p) xss).sum
• Array.count_flatten 📋 Init.Data.Array.Count
  {α : Type u_1} [BEq α] {a : α} {xss : Array (Array α)} : Array.count a xss.flatten = (Array.map (Array.count a) xss).sum
• Array.count_le_count_map 📋 Init.Data.Array.Count
  {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} [BEq β] [LawfulBEq β] {xs : Array α} {f : α → β} {x : α} : Array.count x xs ≤ Array.count (f x) (Array.map f xs)
• Array.countP_flatMap 📋 Init.Data.Array.Count
  {α : Type u_2} {β : Type u_1} {p : β → Bool} {xs : Array α} {f : α → Array β} : Array.countP p (Array.flatMap f xs) = (Array.map (Array.countP p ∘ f) xs).sum
• Array.count_flatMap 📋 Init.Data.Array.Count
  {β : Type u_1} {α : Type u_2} [BEq β] {xs : Array α} {f : α → Array β} {x : β} : Array.count x (Array.flatMap f xs) = (Array.map (Array.count x ∘ f) xs).sum
• Array.map_wfParam 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} : Array.map f (wfParam xs) = Array.map f xs.attach.unattach
• Array.attach_map_subtype_val 📋 Init.Data.Array.Attach
  {α : Type u_1} (xs : Array α) : Array.map Subtype.val xs.attach = xs
• Array.unattach.eq_1 📋 Init.Data.Array.Attach
  {α : Type u_1} {p : α → Prop} (xs : Array { x // p x }) : xs.unattach = Array.map (fun x => ↑x) xs
• Array.attachWith_map_subtype_val 📋 Init.Data.Array.Attach
  {α : Type u_1} {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) : Array.map Subtype.val (xs.attachWith p H) = xs
• Array.pmap_eq_map 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : α → β} {xs : Array α} (H : ∀ a ∈ xs, p a) : Array.pmap (fun a x => f a) xs H = Array.map f xs
• Array.unattach_flatten 📋 Init.Data.Array.Attach
  {α : Type u_1} {p : α → Prop} {xs : Array (Array { x // p x })} : xs.flatten.unattach = (Array.map Array.unattach xs).flatten
• Array.attachWith_map_coe 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : α → β} {xs : Array α} (H : ∀ a ∈ xs, p a) : Array.map (fun i => f ↑i) (xs.attachWith p H) = Array.map f xs
• Array.attachWith_map_val 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : α → β} {xs : Array α} (H : ∀ a ∈ xs, p a) : Array.map (fun i => f ↑i) (xs.attachWith p H) = Array.map f xs
• Array.map_pmap 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} {g : β → γ} {f : (a : α) → p a → β} {xs : Array α} (H : ∀ a ∈ xs, p a) : Array.map g (Array.pmap f xs H) = Array.pmap (fun a h => g (f a h)) xs H
• Array.map_subtype 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → β} {g : α → β} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : Array.map f xs = Array.map g xs.unattach
• Array.attach_map_coe 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → β) : Array.map (fun i => f ↑i) xs.attach = Array.map f xs
• Array.attach_map_val 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → β) : Array.map (fun i => f ↑i) xs.attach = Array.map f xs
• Array.map_unattach 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : Array (Subtype P)} {f : α → β} : Array.map f xs.unattach = Array.map (fun x => match x with | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x)))) xs
• Array.pmap_map 📋 Init.Data.Array.Attach
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {p : β → Prop} {g : (b : β) → p b → γ} {f : α → β} {xs : Array α} (H : ∀ a ∈ Array.map f xs, p a) : Array.pmap g (Array.map f xs) H = Array.pmap (fun a h => g (f a) h) xs ⋯
• Array.map_attach 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : { x // x ∈ xs } → β} : Array.map f xs.attach = Array.pmap (fun a h => f ⟨a, h⟩) xs ⋯
• Array.map_attach_eq_pmap 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : { x // x ∈ xs } → β} : Array.map f xs.attach = Array.pmap (fun a h => f ⟨a, h⟩) xs ⋯
• Array.pmap_eq_map_attach 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {xs : Array α} (H : ∀ a ∈ xs, p a) : Array.pmap f xs H = Array.map (fun x => f ↑x ⋯) xs.attach
• Array.map_attachWith 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a} {f : { x // P x } → β} : Array.map f (xs.attachWith P H) = Array.map (fun x => match x with | ⟨x, h⟩ => f ⟨x, ⋯⟩) xs.attach
• Array.map_attachWith_eq_pmap 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a} {f : { x // P x } → β} : Array.map f (xs.attachWith P H) = Array.pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯
• Array.attachWith_map 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} {P : β → Prop} (H : ∀ b ∈ Array.map f xs, P b) : (Array.map f xs).attachWith P H = Array.map (fun x => match x with | ⟨x, h⟩ => ⟨f x, h⟩) (xs.attachWith (P ∘ f) ⋯)
• Array.attach_map 📋 Init.Data.Array.Attach
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} : (Array.map f xs).attach = Array.map (fun x => match x with | ⟨x, h⟩ => ⟨f x, ⋯⟩) xs.attach
• Array.attach_congr 📋 Init.Data.Array.Attach
  {α : Type u_1} {xs ys : Array α} (h : xs = ys) : xs.attach = Array.map (fun x => ⟨↑x, ⋯⟩) ys.attach
• Array.reverse_attach 📋 Init.Data.Array.Attach
  {α : Type u_1} {xs : Array α} : xs.attach.reverse = Array.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.reverse.attach
• Array.attach_reverse 📋 Init.Data.Array.Attach
  {α : Type u_1} {xs : Array α} : xs.reverse.attach = Array.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach.reverse
• Array.filter_attachWith 📋 Init.Data.Array.Attach
  {α : Type u_1} {stop : ℕ} {q : α → Prop} {xs : Array α} {p : { x // q x } → Bool} (H : ∀ x ∈ xs, q x) (w : stop = (xs.attachWith q H).size) : Array.filter p (xs.attachWith q H) 0 stop = Array.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) (Array.filter (fun x => match x with | ⟨x, h⟩ => p ⟨x, ⋯⟩) xs.attach)
• Array.attach_push 📋 Init.Data.Array.Attach
  {α : Type u_1} {a : α} {xs : Array α} : (xs.push a).attach = (Array.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach).push ⟨a, ⋯⟩
• Array.attach_append 📋 Init.Data.Array.Attach
  {α : Type u_1} {xs ys : Array α} : (xs ++ ys).attach = Array.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach ++ Array.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) ys.attach
• Array.mapIdx_eq_zipIdx_map 📋 Init.Data.Array.MapIdx
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β} : Array.mapIdx f xs = Array.map (fun x => match x with | (a, i) => f i a) xs.zipIdx
• Array.mapIdx_eq_zipWithIndex_map 📋 Init.Data.Array.MapIdx
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β} : Array.mapIdx f xs = Array.map (fun x => match x with | (a, i) => f i a) xs.zipIdx
• Array.mapFinIdx_eq_zipIdx_map 📋 Init.Data.Array.MapIdx
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β} : xs.mapFinIdx f = Array.map (fun x => match x with | ⟨(x, i), m⟩ => f i x ⋯) xs.zipIdx.attach
• Array.mapFinIdx_eq_zipWithIndex_map 📋 Init.Data.Array.MapIdx
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β} : xs.mapFinIdx f = Array.map (fun x => match x with | ⟨(x, i), m⟩ => f i x ⋯) xs.zipIdx.attach
• Array.zipWith_self 📋 Init.Data.Array.Zip
  {α : Type u_1} {δ : Type u_2} {f : α → α → δ} {xs : Array α} : Array.zipWith f xs xs = Array.map (fun a => f a a) xs
• Array.unzip_fst 📋 Init.Data.Array.Zip
  {α✝ : Type u_1} {β✝ : Type u_2} {l : Array (α✝ × β✝)} : l.unzip.1 = Array.map Prod.fst l
• Array.unzip_snd 📋 Init.Data.Array.Zip
  {α✝ : Type u_1} {β✝ : Type u_2} {l : Array (α✝ × β✝)} : l.unzip.2 = Array.map Prod.snd l
• Array.map_fst_zip 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} (h : as.size ≤ bs.size) : Array.map Prod.fst (as.zip bs) = as
• Array.map_snd_zip 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} (h : bs.size ≤ as.size) : Array.map Prod.snd (as.zip bs) = bs
• Array.map_prod_left_eq_zip 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} : Array.map (fun x => (x, f x)) xs = xs.zip (Array.map f xs)
• Array.map_prod_right_eq_zip 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} : Array.map (fun x => (f x, x)) xs = (Array.map f xs).zip xs
• Array.map_uncurry_zip_eq_zipWith 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : Array α} {bs : Array β} : Array.map (Function.uncurry f) (as.zip bs) = Array.zipWith f as bs
• Array.map_zip_eq_zipWith 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {as : Array α} {bs : Array β} : Array.map f (as.zip bs) = Array.zipWith (Function.curry f) as bs
• Array.map_zipWith 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : γ → δ → α} {cs : Array γ} {ds : Array δ} : Array.map f (Array.zipWith g cs ds) = Array.zipWith (fun x y => f (g x y)) cs ds
• Array.unzip_eq_map 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {xs : Array (α × β)} : xs.unzip = (Array.map Prod.fst xs, Array.map Prod.snd xs)
• Array.zipWith_map_left 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} {as : Array α} {bs : Array β} {f : α → α'} {g : α' → β → γ} : Array.zipWith g (Array.map f as) bs = Array.zipWith (fun a b => g (f a) b) as bs
• Array.zipWith_map_right 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} {as : Array α} {bs : Array β} {f : β → β'} {g : α → β' → γ} : Array.zipWith g as (Array.map f bs) = Array.zipWith (fun a b => g a (f b)) as bs
• Array.zip_map' 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {xs : Array α} : (Array.map f xs).zip (Array.map g xs) = Array.map (fun a => (f a, g a)) xs
• Array.map_zipWithAll 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : Option γ → Option δ → α} {cs : Array γ} {ds : Array δ} : Array.map f (Array.zipWithAll g cs ds) = Array.zipWithAll (fun x y => f (g x y)) cs ds
• Array.zip_map_left 📋 Init.Data.Array.Zip
  {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : α → γ} {as : Array α} {bs : Array β} : (Array.map f as).zip bs = Array.map (Prod.map f id) (as.zip bs)
• Array.zip_map_right 📋 Init.Data.Array.Zip
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {as : Array α} {bs : Array β} : as.zip (Array.map f bs) = Array.map (Prod.map id f) (as.zip bs)
• Array.zipWith_map 📋 Init.Data.Array.Zip
  {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {μ : Type u_5} {f : γ → δ → μ} {g : α → γ} {h : β → δ} {as : Array α} {bs : Array β} : Array.zipWith f (Array.map g as) (Array.map h bs) = Array.zipWith (fun a b => f (g a) (h b)) as bs
• Array.zip_of_prod 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} {xs : Array (α × β)} (hl : Array.map Prod.fst xs = as) (hr : Array.map Prod.snd xs = bs) : xs = as.zip bs
• Array.zipWithAll_map_left 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {α' : Type u_1} {γ : Type u_3} {as : Array α} {bs : Array β} {f : α → α'} {g : Option α' → Option β → γ} : Array.zipWithAll g (Array.map f as) bs = Array.zipWithAll (fun a b => g (f <$> a) b) as bs
• Array.zipWithAll_map_right 📋 Init.Data.Array.Zip
  {α : Type u_1} {β β' : Type u_2} {γ : Type u_3} {as : Array α} {bs : Array β} {f : β → β'} {g : Option α → Option β' → γ} : Array.zipWithAll g as (Array.map f bs) = Array.zipWithAll (fun a b => g a (f <$> b)) as bs
• Array.zip_map 📋 Init.Data.Array.Zip
  {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} {as : Array α} {bs : Array β} : (Array.map f as).zip (Array.map g bs) = Array.map (Prod.map f g) (as.zip bs)
• Array.zipWithAll_map 📋 Init.Data.Array.Zip
  {γ : Type u_1} {δ : Type u_2} {α : Type u_1} {β : Type u_2} {μ : Type u_3} {f : Option γ → Option δ → μ} {g : α → γ} {h : β → δ} {as : Array α} {bs : Array β} : Array.zipWithAll f (Array.map g as) (Array.map h bs) = Array.zipWithAll (fun a b => f (g <$> a) (h <$> b)) as bs
• Array.zipIdx_map_fst 📋 Init.Data.Array.Range
  {α : Type u_1} (i : ℕ) (xs : Array α) : Array.map Prod.fst (xs.zipIdx i) = xs
• Array.range'_eq_map_range 📋 Init.Data.Array.Range
  {s n : ℕ} : Array.range' s n = Array.map (fun x => s + x) (Array.range n)
• Array.zipIdx_map_snd 📋 Init.Data.Array.Range
  {α : Type u_1} (i : ℕ) (xs : Array α) : Array.map Prod.snd (xs.zipIdx i) = Array.range' i xs.size
• Array.map_add_range' 📋 Init.Data.Array.Range
  {a : ℕ} (s n step : ℕ) : Array.map (fun x => a + x) (Array.range' s n step) = Array.range' (a + s) n step
• Array.map_zipIdx 📋 Init.Data.Array.Range
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {k : ℕ} : Array.map (Prod.map f id) (xs.zipIdx k) = (Array.map f xs).zipIdx k
• Array.zipIdx_map 📋 Init.Data.Array.Range
  {α : Type u_1} {β : Type u_2} {xs : Array α} {k : ℕ} {f : α → β} : (Array.map f xs).zipIdx k = Array.map (Prod.map f id) (xs.zipIdx k)
• Array.map_sub_range' 📋 Init.Data.Array.Range
  {step a s : ℕ} (h : a ≤ s) (n : ℕ) : Array.map (fun x => x - a) (Array.range' s n step) = Array.range' (s - a) n step
• Array.range'_succ_left 📋 Init.Data.Array.Range
  {s n step : ℕ} : Array.range' (s + 1) n step = Array.map (fun x => x + 1) (Array.range' s n step)
• Array.range_add 📋 Init.Data.Array.Range
  {n m : ℕ} : Array.range (n + m) = Array.range n ++ Array.map (fun x => n + x) (Array.range m)
• Array.range_succ_eq_map 📋 Init.Data.Array.Range
  {n : ℕ} : Array.range (n + 1) = #[0] ++ Array.map Nat.succ (Array.range n)
• Array.map_snd_add_zipIdx_eq_zipIdx 📋 Init.Data.Array.Range
  {α : Type u_1} {xs : Array α} {n k : ℕ} : Array.map (Prod.map id fun x => x + n) (xs.zipIdx k) = xs.zipIdx (n + k)
• Array.reverse_range' 📋 Init.Data.Array.Range
  {s n : ℕ} : (Array.range' s n).reverse = Array.map (fun x => s + n - 1 - x) (Array.range n)
• Array.zipIdx_eq_map_add 📋 Init.Data.Array.Range
  {α : Type u_1} {xs : Array α} {i : ℕ} : xs.zipIdx i = Array.map (fun x => match x with | (a, j) => (a, i + j)) xs.zipIdx
• Array.zipIdx_succ 📋 Init.Data.Array.Range
  {α : Type u_1} {xs : Array α} {i : ℕ} : xs.zipIdx (i + 1) = Array.map (fun x => match x with | (a, j) => (a, j + 1)) (xs.zipIdx i)
• Array.mapM_id 📋 Init.Data.Array.Monadic
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Id β} : Array.mapM f xs = Array.map f xs
• Array.forM_map 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] [LawfulMonad m] {xs : Array α} {g : α → β} {f : β → m PUnit.{u_1 + 1}} : forM (Array.map g xs) f = forM xs fun a => f (g a)
• Array.mapM_pure 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} {f : α → β} : Array.mapM (fun x => pure (f x)) xs = pure (Array.map f xs)
• Array.foldlM_map 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} {stop : ℕ} [Monad m] {f : β₁ → β₂} {g : α → β₂ → m α} {xs : Array β₁} {init : α} {w : stop = xs.size} : Array.foldlM g init (Array.map f xs) 0 stop = Array.foldlM (fun x y => g x (f y)) init xs 0 stop
• Array.foldrM_map 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} {start : ℕ} [Monad m] [LawfulMonad m] {f : β₁ → β₂} {g : β₂ → α → m α} {xs : Array β₁} {init : α} {w : start = xs.size} : Array.foldrM g init (Array.map f xs) start = Array.foldrM (fun x y => g (f x) y) init xs start
• Array.forIn_map 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] {xs : Array α} {g : α → β} {f : β → γ → m (ForInStep γ)} : forIn (Array.map g xs) init f = forIn xs init fun a y => f (g a) y
• Array.forIn'_map 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] {xs : Array α} (g : α → β) (f : (b : β) → b ∈ Array.map g xs → γ → m (ForInStep γ)) : forIn' (Array.map g xs) init f = forIn' xs init fun a h y => f (g a) ⋯ y
• Array.finRange_reverse 📋 Init.Data.Array.FinRange
  {n : ℕ} : (Array.finRange n).reverse = Array.map Fin.rev (Array.finRange n)
• Array.finRange_succ_last 📋 Init.Data.Array.FinRange
  {n : ℕ} : Array.finRange (n + 1) = Array.map Fin.castSucc (Array.finRange n) ++ #[Fin.last n]
• Array.finRange_succ 📋 Init.Data.Array.FinRange
  {n : ℕ} : Array.finRange (n + 1) = #[0] ++ Array.map Fin.succ (Array.finRange n)
• Array.findIdx?_map 📋 Init.Data.Array.Find
  {β : Type u_1} {α : Type u_2} {f : β → α} {xs : Array β} {p : α → Bool} : Array.findIdx? p (Array.map f xs) = Array.findIdx? (p ∘ f) xs
• Array.find?_map 📋 Init.Data.Array.Find
  {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {xs : Array β} : Array.find? p (Array.map f xs) = Option.map f (Array.find? (p ∘ f) xs)
• Array.findSome?_map 📋 Init.Data.Array.Find
  {β : Type u_1} {γ : Type u_2} {α✝ : Type u_3} {p : γ → Option α✝} {f : β → γ} {xs : Array β} : Array.findSome? p (Array.map f xs) = Array.findSome? (p ∘ f) xs
• Array.findIdx?_flatten 📋 Init.Data.Array.Find
  {α : Type u_1} {xss : Array (Array α)} {p : α → Bool} : Array.findIdx? p xss.flatten = Option.map (fun i => (Array.map Array.size (xss.take i)).sum + (Option.map (fun xs => Array.findIdx p xs) xss[i]?).getD 0) (Array.findIdx? (fun x => x.any p) xss)
• Array.map_lt 📋 Init.Data.Array.Lex.Lemmas
  {α : Type u_1} {β : Type u_2} [LT α] [LT β] {xs ys : Array α} {f : α → β} (w : ∀ (x y : α), x < y → f x < f y) (h : xs < ys) : Array.map f xs < Array.map f ys
• Array.map_le 📋 Init.Data.Array.Lex.Lemmas
  {α : Type u_1} {β : Type u_2} [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β] [Std.Irrefl fun x1 x2 => x1 < x2] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Antisymm fun x1 x2 => ¬x1 < x2] [Std.Irrefl fun x1 x2 => x1 < x2] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Antisymm fun x1 x2 => ¬x1 < x2] {xs ys : Array α} {f : α → β} (w : ∀ (x y : α), x < y → f x < f y) (h : xs ≤ ys) : Array.map f xs ≤ Array.map f ys
• Array.eraseP_map 📋 Init.Data.Array.Erase
  {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {xs : Array β} : (Array.map f xs).eraseP p = Array.map f (xs.eraseP (p ∘ f))
• Array.map_extract 📋 Init.Data.Array.Extract
  {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {as : Array α} {i j : ℕ} : Array.map f (as.extract i j) = (Array.map f as).extract i j
• Array.popWhile_map 📋 Init.Data.Array.Extract
  {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Bool} {as : Array α} : Array.popWhile p (Array.map f as) = Array.map f (Array.popWhile (p ∘ f) as)
• Array.takeWhile_map 📋 Init.Data.Array.Extract
  {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Bool} {as : Array α} : Array.takeWhile p (Array.map f as) = Array.map f (Array.takeWhile (p ∘ f) as)
• Vector.toArray_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} : (Vector.map f xs).toArray = Array.map f xs.toArray
• Vector.map.eq_1 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (xs : Vector α n) : Vector.map f xs = { toArray := Array.map f xs.toArray, size_toArray := ⋯ }
• Vector.flatten.eq_1 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n m : ℕ} (xs : Vector (Vector α n) m) : xs.flatten = { toArray := (Array.map Vector.toArray xs.toArray).flatten, size_toArray := ⋯ }
• Vector.map_mk 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Array α} (h : xs.size = n) : Vector.map f { toArray := xs, size_toArray := h } = { toArray := Array.map f xs, size_toArray := ⋯ }
• Vector.unzip_mk 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {xs : Array (α × β)} (h : xs.size = n) : { toArray := xs, size_toArray := h }.unzip = ({ toArray := xs.unzip.1, size_toArray := ⋯ }, { toArray := xs.unzip.2, size_toArray := ⋯ })
• Vector.flatMap_mk 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {m n : ℕ} {f : α → Vector β m} {xs : Array α} (h : xs.size = n) : { toArray := xs, size_toArray := h }.flatMap f = { toArray := Array.flatMap (fun a => (f a).toArray) xs, size_toArray := ⋯ }
• Vector.flatten_mk 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n m : ℕ} {xss : Array (Vector α n)} (h : xss.size = m) : { toArray := xss, size_toArray := h }.flatten = { toArray := (Array.map Vector.toArray xss).flatten, size_toArray := ⋯ }
• Vector.vector₂_induction 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n m : ℕ} (P : Vector (Vector α n) m → Prop) (of : ∀ (xss : Array (Array α)) (h₁ : xss.size = m) (h₂ : ∀ xs ∈ xss, xs.size = n), P { toArray := Array.map (fun x => match x with | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ }) xss.attach, size_toArray := ⋯ }) (xss : Vector (Vector α n) m) : P xss
• Vector.vector₃_induction 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n m k : ℕ} (P : Vector (Vector (Vector α n) m) k → Prop) (of : ∀ (xss : Array (Array (Array α))) (h₁ : xss.size = k) (h₂ : ∀ xs ∈ xss, xs.size = m) (h₃ : ∀ xs ∈ xss, ∀ as ∈ xs, as.size = n), P { toArray := Array.map (fun x => match x with | ⟨xs, m_1⟩ => { toArray := Array.map (fun x => match x with | ⟨as, m'⟩ => { toArray := as, size_toArray := ⋯ }) xs.attach, size_toArray := ⋯ }) xss.attach, size_toArray := ⋯ }) (xss : Vector (Vector (Vector α n) m) k) : P xss
• Std.DHashMap.Internal.updateAllBuckets.eq_1 📋 Std.Data.DHashMap.Internal.Model
  {α : Type u} {β : α → Type v} {δ : α → Type w} (self : Array (Std.DHashMap.Internal.AssocList α β)) (f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α δ) : Std.DHashMap.Internal.updateAllBuckets self f = Array.map f self
• Std.Sat.AIG.relabel.eq_1 📋 Std.Sat.AIG.Relabel
  {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] (r : α → β) (aig : Std.Sat.AIG α) : Std.Sat.AIG.relabel r aig = { decls := Array.map (Std.Sat.AIG.Decl.relabel r) aig.decls, cache := Std.Sat.AIG.Cache.empty, hdag := ⋯, hzero := ⋯, hconst := ⋯ }

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