Loogle!

Result

Found 585 declarations mentioning Option.map. Of these, only the first 200 are shown.

• Option.map 📋 Init.Prelude
  {α : Type u_1} {β : Type u_2} (f : α → β) : Option α → Option β
• Option.map_id 📋 Init.Data.Option.Basic
  {α : Type u_1} : Option.map id = id
• Option.map_none 📋 Init.Data.Option.Basic
  {α : Type u_1} {β : Type u_2} (f : α → β) : Option.map f none = none
• Option.map_some 📋 Init.Data.Option.Basic
  {α : Type u_1} {β : Type u_2} (a : α) (f : α → β) : Option.map f (some a) = some (f a)
• Array.findIdx?_eq_map_findFinIdx?_val 📋 Init.Data.Array.Basic
  {α : Type u} {xs : Array α} {p : α → Bool} : Array.findIdx? p xs = Option.map (fun x => ↑x) (Array.findFinIdx? p xs)
• Array.findIdx?_loop_eq_map_findFinIdx?_loop_val 📋 Init.Data.Array.Basic
  {α : Type u} {xs : Array α} {p : α → Bool} {j : ℕ} : Array.findIdx?.loop p xs j = Option.map (fun x => ↑x) (Array.findFinIdx?.loop p xs j)
• Option.map_id' 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {x : Option α} : Option.map (fun a => a) x = x
• Option.map_id_fun 📋 Init.Data.Option.Lemmas
  {α : Type u} : Option.map id = id
• Option.map_id_fun' 📋 Init.Data.Option.Lemmas
  {α : Type u} : (Option.map fun a => a) = id
• Option.map_none' 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} (f : α → β) : Option.map f none = none
• Option.isNone_map 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} : (Option.map f x).isNone = x.isNone
• Option.isSome_map 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} : (Option.map f x).isSome = x.isSome
• Option.isSome_map' 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} : (Option.map f x).isSome = x.isSome
• Option.map_eq_map 📋 Init.Data.Option.Lemmas
  {α✝ α✝¹ : Type u_1} {f : α✝ → α✝¹} : Functor.map f = Option.map f
• Option.map_some' 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} (a : α) (f : α → β) : Option.map f (some a) = some (f a)
• Option.getD_map 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) (o : Option α) : (Option.map f o).getD (f x) = f (o.getD x)
• Option.map_eq_none 📋 Init.Data.Option.Lemmas
  {α✝ : Type u_1} {x : Option α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Option.map f x = none ↔ x = none
• Option.map_eq_none' 📋 Init.Data.Option.Lemmas
  {α✝ : Type u_1} {x : Option α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Option.map f x = none ↔ x = none
• Option.map_eq_none_iff 📋 Init.Data.Option.Lemmas
  {α✝ : Type u_1} {x : Option α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Option.map f x = none ↔ x = none
• Option.any_map 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → β} {p : β → Bool} : Option.any p (Option.map f x) = Option.any (fun a => p (f a)) x
• Option.join_join 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {x : Option (Option (Option α))} : x.join.join = (Option.map Option.join x).join
• Option.map_eq_bind 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} : Option.map f x = x.bind (some ∘ f)
• Option.mem_map_of_mem 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {x : Option α} {a : α} (g : α → β) (h : a ∈ x) : g a ∈ Option.map g x
• Option.join_map_eq_map_join 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {x : Option (Option α)} : (Option.map (Option.map f) x).join = Option.map f x.join
• Option.comp_map 📋 Init.Data.Option.Lemmas
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} (h : β → γ) (g : α → β) (x : Option α) : Option.map (h ∘ g) x = Option.map h (Option.map g x)
• Option.map_map 📋 Init.Data.Option.Lemmas
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} (h : β → γ) (g : α → β) (x : Option α) : Option.map h (Option.map g x) = Option.map (h ∘ g) x
• Option.map_or 📋 Init.Data.Option.Lemmas
  {α✝ : Type u_1} {o o' : Option α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Option.map f (o.or o') = (Option.map f o).or (Option.map f o')
• Option.map_or' 📋 Init.Data.Option.Lemmas
  {α✝ : Type u_1} {o o' : Option α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Option.map f (o.or o') = (Option.map f o).or (Option.map f o')
• Option.bind_map 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → Option γ} {x : Option α} : (Option.map f x).bind g = x.bind (g ∘ f)
• Option.guard_eq_map 📋 Init.Data.Option.Lemmas
  {α : Type u_1} (p : α → Bool) : Option.guard p = fun x => Option.map (fun x_1 => x) (if p x = true then some x else none)
• Option.map_orElse 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} {y : Unit → Option α} : Option.map f (x.orElse y) = (Option.map f x).orElse fun x => Option.map f (y ())
• Option.map_congr 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {α✝ : Type u_2} {f g : α → α✝} {x : Option α} (h : ∀ (a : α), x = some a → f a = g a) : Option.map f x = Option.map g x
• Option.map_eq_some 📋 Init.Data.Option.Lemmas
  {α✝ : Type u_1} {b : α✝} {α✝¹ : Type u_2} {x : Option α✝¹} {f : α✝¹ → α✝} : Option.map f x = some b ↔ ∃ a, x = some a ∧ f a = b
• Option.map_eq_some' 📋 Init.Data.Option.Lemmas
  {α✝ : Type u_1} {b : α✝} {α✝¹ : Type u_2} {x : Option α✝¹} {f : α✝¹ → α✝} : Option.map f x = some b ↔ ∃ a, x = some a ∧ f a = b
• Option.map_eq_some_iff 📋 Init.Data.Option.Lemmas
  {α✝ : Type u_1} {b : α✝} {α✝¹ : Type u_2} {x : Option α✝¹} {f : α✝¹ → α✝} : Option.map f x = some b ↔ ∃ a, x = some a ∧ f a = b
• Option.bind_map_comm 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {x : Option (Option α)} {f : α → β} : x.bind (Option.map f) = (Option.map (Option.map f) x).bind id
• Option.map_comp_map 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) : Option.map g ∘ Option.map f = Option.map (g ∘ f)
• Option.map_if 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {c : Prop} {a : α} {f : α → β} {x✝ : Decidable c} : Option.map f (if c then some a else none) = if c then some (f a) else none
• Option.guard_comp 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : β → α} : Option.guard p ∘ f = Option.map f ∘ Option.guard (p ∘ f)
• Option.map_bind 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {x : Option α} : Option.map g (x.bind f) = x.bind (Option.map g ∘ f)
• Option.pmap_eq_map 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : α → β) (o : Option α) (H : ∀ (a : α), o = some a → p a) : Option.pmap (fun a x => f a) o H = Option.map f o
• Option.map_inj_right 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {o o' : Option α} (w : ∀ (x y : α), f x = f y → x = y) : Option.map f o = Option.map f o' ↔ o = o'
• Option.map_dif 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {c : Prop} {f : α → β} {x✝ : Decidable c} {a : c → α} : Option.map f (if h : c then some (a h) else none) = if h : c then some (f (a h)) else none
• Option.map_pbind 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {o : Option α} {f : (a : α) → o = some a → Option β} {g : β → γ} : Option.map g (o.pbind f) = o.pbind fun a h => Option.map g (f a h)
• Option.map_pmap 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (o : Option α) (H : ∀ (a : α), o = some a → p a) : Option.map g (Option.pmap f o H) = Option.pmap (fun a h => g (f a h)) o H
• Option.get_map 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {o : Option α} {h : (Option.map f o).isSome = true} : (Option.map f o).get h = f (o.get ⋯)
• Option.pbind_map 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (o : Option α) (f : α → β) (g : (x : β) → Option.map f o = some x → Option γ) : (Option.map f o).pbind g = o.pbind fun x h => g (f x) ⋯
• Option.pmap_map 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (o : Option α) (f : α → β) {p : β → Prop} (g : (b : β) → p b → γ) (H : ∀ (a : β), Option.map f o = some a → p a) : Option.pmap g (Option.map f o) H = Option.pmap (fun a h => g (f a) h) o ⋯
• 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.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.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.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_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.tail?_append 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l l' : List α} : (l ++ l').tail? = (Option.map (fun x => x ++ l') l.tail?).or l'.tail?
• 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.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.getElem?_zipWith' 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {f : α → β → γ} {i : ℕ} : (List.zipWith f l₁ l₂)[i]? = (Option.map f l₁[i]?).bind fun g => Option.map g l₂[i]?
• Lean.Omega.Constraint.map.eq_1 📋 Init.Omega.Constraint
  (c : Lean.Omega.Constraint) (f : ℤ → ℤ) : c.map f = { lowerBound := Option.map f c.lowerBound, upperBound := Option.map f c.upperBound }
• Lean.Omega.Constraint.add.eq_1 📋 Init.Omega.Constraint
  (x y : Lean.Omega.Constraint) : x.add y = { lowerBound := Option.bind x.lowerBound fun a => Option.map (fun b => a + b) y.lowerBound, upperBound := Option.bind x.upperBound fun a => Option.map (fun b => a + b) y.upperBound }
• Lean.Omega.Constraint.div.eq_1 📋 Init.Omega.Constraint
  (c : Lean.Omega.Constraint) (k : ℕ) : c.div k = { lowerBound := Option.map (fun x => -(-x / ↑k)) c.lowerBound, upperBound := Option.map (fun y => y / ↑k) c.upperBound }
• List.countP_filterMap 📋 Init.Data.List.Count
  {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → Option β} {l : List α} : List.countP p (List.filterMap f l) = List.countP (fun a => (Option.map p (f a)).getD false) l
• List.find?_subtype 📋 Init.Data.List.Attach
  {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : Option.map Subtype.val (List.find? f l) = List.find? g l.unattach
• List.getElem?_unattach 📋 Init.Data.List.Attach
  {α : Type u_1} {p : α → Prop} {l : List { x // p x }} (i : ℕ) : l.unattach[i]? = Option.map Subtype.val l[i]?
• List.getLast?_pmap 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs, P a) : (List.pmap f xs H).getLast? = Option.map (fun x => match x with | ⟨a, m⟩ => f a ⋯) xs.attach.getLast?
• List.head?_pmap 📋 Init.Data.List.Attach
  {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs, P a) : (List.pmap f xs H).head? = Option.map (fun x => match x with | ⟨a, m⟩ => f a ⋯) xs.attach.head?
• List.getElem?_enumFrom 📋 Init.Data.List.Range
  {α : Type u_1} (i : ℕ) (l : List α) (j : ℕ) : (List.enumFrom i l)[j]? = Option.map (fun a => (i + j, a)) l[j]?
• List.getElem?_zipIdx 📋 Init.Data.List.Range
  {α : Type u_1} {l : List α} {i j : ℕ} : (l.zipIdx i)[j]? = Option.map (fun a => (a, i + j)) l[j]?
• List.findIdx?_eq_map_findFinIdx?_val 📋 Init.Data.List.Find
  {α : Type u_1} {xs : List α} {p : α → Bool} : List.findIdx? p xs = Option.map (fun x => ↑x) (List.findFinIdx? p xs)
• List.find?_map 📋 Init.Data.List.Find
  {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {l : List β} : List.find? p (List.map f l) = Option.map f (List.find? (p ∘ f) l)
• List.idxOf?_eq_map_finIdxOf?_val 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] {xs : List α} {a : α} : List.idxOf? a xs = Option.map (fun x => ↑x) (List.finIdxOf? a xs)
• List.map_findSome? 📋 Init.Data.List.Find
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {l : List α} : Option.map g (List.findSome? f l) = List.findSome? (Option.map g ∘ f) l
• List.findIdx?_eq_fst_find?_zipIdx 📋 Init.Data.List.Find
  {α : Type u_1} {xs : List α} {p : α → Bool} : List.findIdx? p xs = Option.map (fun x => x.2) (List.find? (fun x => match x with | (x, snd) => p x) xs.zipIdx)
• List.findIdx?_append 📋 Init.Data.List.Find
  {α : Type u_1} {xs ys : List α} {p : α → Bool} : List.findIdx? p (xs ++ ys) = (List.findIdx? p xs).or (Option.map (fun i => i + xs.length) (List.findIdx? p ys))
• List.findIdx?_go_eq_map_findFinIdx?_go_val 📋 Init.Data.List.Find
  {α : Type u_1} {l xs : List α} {p : α → Bool} {i : ℕ} {h : xs.length + i = l.length} : List.findIdx?.go p xs i = Option.map (fun x => ↑x) (List.findFinIdx?.go p l xs i h)
• List.findIdx?_cons 📋 Init.Data.List.Find
  {α✝ : Type u_1} {x : α✝} {xs : List α✝} {p : α✝ → Bool} : List.findIdx? p (x :: xs) = if p x = true then some 0 else Option.map (fun i => i + 1) (List.findIdx? p xs)
• List.idxOf?_cons 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] {a : α} {xs : List α} {b : α} : List.idxOf? b (a :: xs) = if (a == b) = true then some 0 else Option.map (fun x => x + 1) (List.idxOf? b xs)
• List.findIdx?_flatten 📋 Init.Data.List.Find
  {α : Type u_1} {l : List (List α)} {p : α → Bool} : List.findIdx? p l.flatten = Option.map (fun i => (List.map List.length (List.take i l)).sum + (Option.map (fun xs => List.findIdx p xs) l[i]?).getD 0) (List.findIdx? (fun x => x.any p) l)
• List.findIdx?_join 📋 Init.Data.List.Find
  {α : Type u_1} {l : List (List α)} {p : α → Bool} : List.findIdx? p l.flatten = Option.map (fun i => (List.map List.length (List.take i l)).sum + (Option.map (fun xs => List.findIdx p xs) l[i]?).getD 0) (List.findIdx? (fun x => x.any p) l)
• List.findFinIdx?_cons 📋 Init.Data.List.Find
  {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} : List.findFinIdx? p (x :: xs) = if p x = true then some 0 else Option.map Fin.succ (List.findFinIdx? p xs)
• List.finIdxOf?_cons 📋 Init.Data.List.Find
  {α : Type u_1} {b : α} [BEq α] {a : α} {xs : List α} : List.finIdxOf? b (a :: xs) = if (a == b) = true then some ⟨0, ⋯⟩ else Option.map (fun x => x.succ) (List.finIdxOf? b xs)
• List.find?_pmap 📋 Init.Data.List.Find
  {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs, P a) {p : β → Bool} : List.find? p (List.pmap f xs H) = Option.map (fun x => match x with | ⟨a, m⟩ => f a ⋯) (List.find? (fun x => match x with | ⟨a, m⟩ => p (f a ⋯)) xs.attach)
• List.findFinIdx?_subtype 📋 Init.Data.List.Find
  {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : List.findFinIdx? f l = Option.map (fun i => Fin.cast ⋯ i) (List.findFinIdx? g l.unattach)
• List.findFinIdx?_append 📋 Init.Data.List.Find
  {α : Type u_1} {xs ys : List α} {p : α → Bool} : List.findFinIdx? p (xs ++ ys) = (Option.map (Fin.castLE ⋯) (List.findFinIdx? p xs)).or (Option.map (Fin.cast ⋯) (Option.map (Fin.natAdd xs.length) (List.findFinIdx? p ys)))
• Option.map.eq_2 📋 Init.Data.List.Nat.Modify
  {α : Type u_1} {β : Type u_2} (f : α → β) : Option.map f none = none
• Option.map.eq_1 📋 Init.Data.List.Nat.Modify
  {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) : Option.map f (some x) = some (f x)
• List.head?_modifyHead 📋 Init.Data.List.Nat.Modify
  {α : Type u_1} {l : List α} {f : α → α} : (List.modifyHead f l).head? = Option.map f l.head?
• List.getElem?_modifyHead_zero 📋 Init.Data.List.Nat.Modify
  {α : Type u_1} {l : List α} {f : α → α} : (List.modifyHead f l)[0]? = Option.map f l[0]?
• List.getElem?_modifyHead 📋 Init.Data.List.Nat.Modify
  {α : Type u_1} {l : List α} {f : α → α} {i : ℕ} : (List.modifyHead f l)[i]? = if i = 0 then Option.map f l[i]? else l[i]?
• Array.idxOf?.eq_1 📋 Init.Data.List.ToArray
  {α : Type u} [BEq α] (xs : Array α) (v : α) : xs.idxOf? v = Option.map (fun x => ↑x) (xs.finIdxOf? v)
• 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.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.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.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.findFinIdx?_toList 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {p : α → Bool} {xs : Array α} : List.findFinIdx? p xs.toList = Option.map (Fin.cast ⋯) (Array.findFinIdx? p xs)
• Array.finIdxOf?_toList 📋 Init.Data.Array.Lemmas
  {α : Type u_1} [BEq α] {a : α} {xs : Array α} : List.finIdxOf? a xs.toList = Option.map (Fin.cast ⋯) (xs.finIdxOf? a)
• 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.getElem?_modify 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {xs : Array α} {i : ℕ} {f : α → α} {j : ℕ} : (xs.modify i f)[j]? = if i = j then Option.map f xs[j]? else xs[j]?
• Array.countP_filterMap 📋 Init.Data.Array.Count
  {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → Option β} {xs : Array α} : Array.countP p (Array.filterMap f xs) = Array.countP (fun a => (Option.map p (f a)).getD false) xs
• Array.find?_subtype 📋 Init.Data.Array.Attach
  {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : Option.map Subtype.val (Array.find? f xs) = Array.find? g xs.unattach
• Array.getElem?_unattach 📋 Init.Data.Array.Attach
  {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} (i : ℕ) : xs.unattach[i]? = Option.map Subtype.val xs[i]?
• Array.back?_pmap 📋 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).back? = Option.map (fun x => match x with | ⟨a, m⟩ => f a ⋯) xs.attach.back?
• List.head?_enumFrom 📋 Init.Data.List.Nat.Range
  {α : Type u_1} (n : ℕ) (l : List α) : (List.enumFrom n l).head? = Option.map (fun a => (n, a)) l.head?
• List.head?_zipIdx 📋 Init.Data.List.Nat.Range
  {α : Type u_1} {l : List α} {k : ℕ} : (l.zipIdx k).head? = Option.map (fun a => (a, k)) l.head?
• List.head?_enum 📋 Init.Data.List.Nat.Range
  {α : Type u_1} (l : List α) : l.enum.head? = Option.map (fun a => (0, a)) l.head?
• List.getLast?_enum 📋 Init.Data.List.Nat.Range
  {α : Type u_1} (l : List α) : l.enum.getLast? = Option.map (fun a => (l.length - 1, a)) l.getLast?
• List.getLast?_enumFrom 📋 Init.Data.List.Nat.Range
  {α : Type u_1} (n : ℕ) (l : List α) : (List.enumFrom n l).getLast? = Option.map (fun a => (n + l.length - 1, a)) l.getLast?
• List.getLast?_zipIdx 📋 Init.Data.List.Nat.Range
  {α : Type u_1} {l : List α} {k : ℕ} : (l.zipIdx k).getLast? = Option.map (fun a => (a, k + l.length - 1)) l.getLast?
• List.getElem?_enum 📋 Init.Data.List.Nat.Range
  {α : Type u_1} (l : List α) (i : ℕ) : l.enum[i]? = Option.map (fun a => (i, a)) l[i]?
• Option.attach_map_subtype_val 📋 Init.Data.Option.Attach
  {α : Type u_1} (o : Option α) : Option.map Subtype.val o.attach = o
• Option.unattach.eq_1 📋 Init.Data.Option.Attach
  {α : Type u_1} {p : α → Prop} (o : Option { x // p x }) : o.unattach = Option.map (fun x => ↑x) o
• Option.attachWith_map_subtype_val 📋 Init.Data.Option.Attach
  {α : Type u_1} {p : α → Prop} (o : Option α) (H : ∀ (a : α), o = some a → p a) : Option.map Subtype.val (o.attachWith p H) = o
• Option.attachWith_map_coe 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ (a : α), o = some a → p a) : Option.map (fun i => f ↑i) (o.attachWith p H) = Option.map f o
• Option.attachWith_map_val 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ (a : α), o = some a → p a) : Option.map (fun i => f ↑i) (o.attachWith p H) = Option.map f o
• Option.attach_map_coe 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → β) : Option.map (fun i => f ↑i) o.attach = Option.map f o
• Option.attach_map_val 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → β) : Option.map (fun i => f ↑i) o.attach = Option.map f o
• Option.map_subtype 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {o : Option { x // p x }} {f : { x // p x } → β} {g : α → β} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : Option.map f o = Option.map g o.unattach
• Option.map_attach 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} {o : Option α} (f : { x // o = some x } → β) : Option.map f o.attach = Option.pmap (fun a h => f ⟨a, h⟩) o ⋯
• Option.map_attach_eq_pmap 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} {o : Option α} (f : { x // o = some x } → β) : Option.map f o.attach = Option.pmap (fun a h => f ⟨a, h⟩) o ⋯
• Option.map_attach_eq_attachWith 📋 Init.Data.Option.Attach
  {α : Type u_1} {o : Option α} {p : α → Prop} (f : ∀ (a : α), o = some a → p a) : Option.map (fun x => ⟨↑x, ⋯⟩) o.attach = o.attachWith p f
• Option.map_attachWith 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} {l : Option α} {P : α → Prop} {H : ∀ (a : α), l = some a → P a} (f : { x // P x } → β) : Option.map f (l.attachWith P H) = Option.map (fun x => match x with | ⟨x, h⟩ => f ⟨x, ⋯⟩) l.attach
• Option.map_attachWith_eq_pmap 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} {o : Option α} {P : α → Prop} {H : ∀ (a : α), o = some a → P a} (f : { x // P x } → β) : Option.map f (o.attachWith P H) = Option.pmap (fun a h => f ⟨a, ⋯⟩) o ⋯
• Option.attach_congr 📋 Init.Data.Option.Attach
  {α : Type u_1} {o₁ o₂ : Option α} (h : o₁ = o₂) : o₁.attach = Option.map (fun x => ⟨↑x, ⋯⟩) o₂.attach
• Option.attach_toList 📋 Init.Data.Option.Attach
  {α : Type u_1} (o : Option α) : o.toList.attach = (Option.map (fun x => match x with | ⟨a, h⟩ => ⟨a, ⋯⟩) o.attach).toList
• Option.attach_map 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} {o : Option α} (f : α → β) : (Option.map f o).attach = Option.map (fun x => match x with | ⟨x, h⟩ => ⟨f x, ⋯⟩) o.attach
• Option.attachWith_map 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), Option.map f o = some b → P b} : (Option.map f o).attachWith P H = Option.map (fun x => match x with | ⟨x, h⟩ => ⟨f x, h⟩) (o.attachWith (P ∘ f) ⋯)
• Option.attach_bind 📋 Init.Data.Option.Attach
  {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β} : (o.bind f).attach = o.attach.bind fun x => match x with | ⟨x, h⟩ => Option.map (fun x_1 => match x_1 with | ⟨y, h'⟩ => ⟨y, ⋯⟩) (f x).attach
• List.head?_mapIdx 📋 Init.Data.List.MapIdx
  {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β} : (List.mapIdx f l).head? = Option.map (f 0) l.head?
• List.getLast?_mapIdx 📋 Init.Data.List.MapIdx
  {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β} : (List.mapIdx f l).getLast? = Option.map (f (l.length - 1)) l.getLast?
• List.getElem?_mapIdx 📋 Init.Data.List.MapIdx
  {α : Type u_1} {α✝ : Type u_2} {f : ℕ → α → α✝} {l : List α} {i : ℕ} : (List.mapIdx f l)[i]? = Option.map (f i) l[i]?
• List.mapIdx_eq_iff 📋 Init.Data.List.MapIdx
  {α : Type u_1} {α✝ : Type u_2} {f : ℕ → α → α✝} {l' : List α✝} {l : List α} : List.mapIdx f l = l' ↔ ∀ (i : ℕ), l'[i]? = Option.map (f i) l[i]?
• List.mapIdx_eq_cons_iff' 📋 Init.Data.List.MapIdx
  {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {l₂ : List β} {l : List α} {b : β} : List.mapIdx f l = b :: l₂ ↔ Option.map (f 0) l.head? = some b ∧ Option.map (List.mapIdx fun i => f (i + 1)) l.tail? = some l₂
• List.getElem?_mapIdx_go 📋 Init.Data.List.MapIdx
  {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {l : List α} {acc : Array β} {i : ℕ} : (List.mapIdx.go f l acc)[i]? = if h : i < acc.size then some acc[i] else Option.map (f i) l[i - acc.size]?
• List.mapFinIdx_eq_cons_iff' 📋 Init.Data.List.MapIdx
  {α : Type u_1} {β : Type u_2} {l₂ : List β} {l : List α} {b : β} {f : (i : ℕ) → α → i < l.length → β} : l.mapFinIdx f = b :: l₂ ↔ (l.head?.pbind fun x m => some (f 0 x ⋯)) = some b ∧ Option.map (fun x => match x with | ⟨t, m⟩ => t.mapFinIdx fun i a h => f (i + 1) a ⋯) l.tail?.attach = some l₂
• Array.back?_mapIdx 📋 Init.Data.Array.MapIdx
  {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β} : (Array.mapIdx f xs).back? = Option.map (f (xs.size - 1)) xs.back?
• Array.getElem?_mapIdx 📋 Init.Data.Array.MapIdx
  {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {xs : Array α} {i : ℕ} : (Array.mapIdx f xs)[i]? = Option.map (f i) xs[i]?
• Array.mapIdx_eq_iff 📋 Init.Data.Array.MapIdx
  {α : Type u_1} {α✝ : Type u_2} {f : ℕ → α → α✝} {ys : Array α✝} {xs : Array α} : Array.mapIdx f xs = ys ↔ ∀ (i : ℕ), ys[i]? = Option.map (f i) xs[i]?
• Array.getElem?_zipWith' 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁ : Array α} {l₂ : Array β} {f : α → β → γ} {i : ℕ} : (Array.zipWith f l₁ l₂)[i]? = (Option.map f l₁[i]?).bind fun g => Option.map g l₂[i]?
• Array.getElem?_zipIdx 📋 Init.Data.Array.Range
  {α : Type u_1} {xs : Array α} {i j : ℕ} : (xs.zipIdx i)[j]? = Option.map (fun a => (a, i + j)) xs[j]?
• 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.idxOf?_eq_map_finIdxOf?_val 📋 Init.Data.Array.Find
  {α : Type u_1} [BEq α] {xs : Array α} {a : α} : xs.idxOf? a = Option.map (fun x => ↑x) (xs.finIdxOf? a)
• Array.map_findSome? 📋 Init.Data.Array.Find
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {xs : Array α} : Option.map g (Array.findSome? f xs) = Array.findSome? (Option.map g ∘ f) xs
• Array.findIdx?_eq_fst_find?_zipIdx 📋 Init.Data.Array.Find
  {α : Type u_1} {xs : Array α} {p : α → Bool} : Array.findIdx? p xs = Option.map (fun x => x.2) (Array.find? (fun x => match x with | (x, snd) => p x) xs.zipIdx)
• Array.findIdx?_append 📋 Init.Data.Array.Find
  {α : Type u_1} {xs ys : Array α} {p : α → Bool} : Array.findIdx? p (xs ++ ys) = (Array.findIdx? p xs).or (Option.map (fun i => i + xs.size) (Array.findIdx? p ys))
• Array.findFinIdx?_congr 📋 Init.Data.Array.Find
  {α : Type u_1} {p : α → Bool} {xs ys : Array α} (w : xs = ys) : Array.findFinIdx? p xs = Option.map (fun i => Fin.cast ⋯ i) (Array.findFinIdx? p ys)
• 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.find?_pmap 📋 Init.Data.Array.Find
  {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α} (H : ∀ a ∈ xs, P a) {p : β → Bool} : Array.find? p (Array.pmap f xs H) = Option.map (fun x => match x with | ⟨a, m⟩ => f a ⋯) (Array.find? (fun x => match x with | ⟨a, m⟩ => p (f a ⋯)) xs.attach)
• Array.findFinIdx?_subtype 📋 Init.Data.Array.Find
  {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : Array.findFinIdx? f xs = Option.map (fun i => Fin.cast ⋯ i) (Array.findFinIdx? g xs.unattach)
• Array.findFinIdx?_push 📋 Init.Data.Array.Find
  {α : Type u_1} {xs : Array α} {a : α} {p : α → Bool} : Array.findFinIdx? p (xs.push a) = (Option.map (Fin.castLE ⋯) (Array.findFinIdx? p xs)).or (if p a = true then some ⟨xs.size, ⋯⟩ else none)
• Array.findFinIdx?_append 📋 Init.Data.Array.Find
  {α : Type u_1} {xs ys : Array α} {p : α → Bool} : Array.findFinIdx? p (xs ++ ys) = (Option.map (Fin.castLE ⋯) (Array.findFinIdx? p xs)).or (Option.map (Fin.cast ⋯) (Option.map (Fin.natAdd xs.size) (Array.findFinIdx? p ys)))
• Option.forM_map 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : β → m PUnit.{u_1 + 1}) : (Option.map g o).forM f = o.forM fun a => f (g a)
• Option.forIn_map 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : β → γ → m (ForInStep γ)) : forIn (Option.map g o) init f = forIn o init fun a y => f (g a) y
• Option.forIn'_map 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : (b : β) → b ∈ Option.map g o → γ → m (ForInStep γ)) : forIn' (Option.map g o) init f = forIn' o init fun a h y => f (g a) ⋯ y
• Sum.getLeft?_map 📋 Init.Data.Sum.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ) : (Sum.map f g x).getLeft? = Option.map f x.getLeft?
• Sum.getRight?_map 📋 Init.Data.Sum.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ) : (Sum.map f g x).getRight? = Option.map g x.getRight?
• Vector.back?_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} : (Vector.map f xs).back? = Option.map f xs.back?
• Vector.findFinIdx?_mk 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n) (f : α → Bool) : Vector.findFinIdx? f { toArray := xs, size_toArray := h } = Option.map (Fin.cast h) (Array.findFinIdx? f xs)
• Vector.finIdxOf?_mk 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} [BEq α] {xs : Array α} (h : xs.size = n) (x : α) : { toArray := xs, size_toArray := h }.finIdxOf? x = Option.map (Fin.cast h) (xs.finIdxOf? x)
• Vector.indexOf?_mk 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} [BEq α] {xs : Array α} (h : xs.size = n) (x : α) : { toArray := xs, size_toArray := h }.finIdxOf? x = Option.map (Fin.cast h) (xs.finIdxOf? x)
• Vector.findFinIdx?_toArray 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n} : Array.findFinIdx? p xs.toArray = Option.map (Fin.cast ⋯) (Vector.findFinIdx? p xs)
• Vector.finIdxOf?_toArray 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} [BEq α] {a : α} {xs : Vector α n} : xs.finIdxOf? a = Option.map (Fin.cast ⋯) (xs.finIdxOf? a)
• Vector.findFinIdx?_toList 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n} : List.findFinIdx? p xs.toList = Option.map (Fin.cast ⋯) (Vector.findFinIdx? p xs)
• Vector.finIdxOf?_toList 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} [BEq α] {a : α} {xs : Vector α n} : List.finIdxOf? a xs.toList = Option.map (Fin.cast ⋯) (xs.finIdxOf? a)
• Vector.getElem?_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {i : ℕ} : (Vector.map f xs)[i]? = Option.map f xs[i]?
• Vector.find?_subtype 📋 Init.Data.Vector.Attach
  {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : Option.map Subtype.val (Array.find? f xs) = Array.find? g xs.unattach
• Vector.back?_pmap 📋 Init.Data.Vector.Attach
  {α : Type u_1} {β : Type u_2} {n : ℕ} {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n} (H : ∀ a ∈ xs, P a) : (Vector.pmap f xs H).back? = Option.map (fun x => match x with | ⟨a, m⟩ => f a ⋯) xs.attach.back?
• Vector.getElem?_unattach 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n} (i : ℕ) : xs.unattach[i]? = Option.map Subtype.val xs[i]?
• Vector.back?_mapIdx 📋 Init.Data.Vector.MapIdx
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : ℕ → α → β} : (Vector.mapIdx f xs).back? = Option.map (f (xs.size - 1)) xs.back?
• Vector.getElem?_mapIdx 📋 Init.Data.Vector.MapIdx
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : ℕ → α → β} {xs : Vector α n} {i : ℕ} : (Vector.mapIdx f xs)[i]? = Option.map (f i) xs[i]?
• Vector.getElem?_zipWith' 📋 Init.Data.Vector.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n✝ : ℕ} {as : Vector α n✝} {bs : Vector β n✝} {f : α → β → γ} {i : ℕ} : (Vector.zipWith f as bs)[i]? = (Option.map f as[i]?).bind fun g => Option.map g bs[i]?
• Vector.getElem?_zipIdx 📋 Init.Data.Vector.Range
  {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} : (xs.zipIdx i)[j]? = Option.map (fun a => (a, i + j)) xs[j]?
• Vector.find?_map 📋 Init.Data.Vector.Find
  {β α : Type} {n : ℕ} {p : α → Bool} {f : β → α} {xs : Vector β n} : Vector.find? p (Vector.map f xs) = Option.map f (Vector.find? (p ∘ f) xs)
• Vector.map_findSome? 📋 Init.Data.Vector.Find
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → Option β} {g : β → γ} {xs : Vector α n} : Option.map g (Vector.findSome? f xs) = Vector.findSome? (Option.map g ∘ f) xs
• Vector.find?_pmap 📋 Init.Data.Vector.Find
  {α β : Type} {n : ℕ} {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n} (H : ∀ a ∈ xs, P a) {p : β → Bool} : Vector.find? p (Vector.pmap f xs H) = Option.map (fun x => match x with | ⟨a, m⟩ => f a ⋯) (Vector.find? (fun x => match x with | ⟨a, m⟩ => p (f a ⋯)) xs.attach)
• Vector.findFinIdx?_push 📋 Init.Data.Vector.Find
  {α : Type u_1} {n : ℕ} {xs : Vector α n} {a : α} {p : α → Bool} : Vector.findFinIdx? p (xs.push a) = (Option.map Fin.castSucc (Vector.findFinIdx? p xs)).or (if p a = true then some ⟨n, ⋯⟩ else none)
• Vector.findFinIdx?_append 📋 Init.Data.Vector.Find
  {α : Type u_1} {n₁ n₂ : ℕ} {xs : Vector α n₁} {ys : Vector α n₂} {p : α → Bool} : Vector.findFinIdx? p (xs ++ ys) = (Option.map (Fin.castLE ⋯) (Vector.findFinIdx? p xs)).or (Option.map (Fin.cast ⋯) (Option.map (Fin.natAdd xs.size) (Vector.findFinIdx? p ys)))
• Std.Internal.List.Option.dmap_eq_map 📋 Std.Data.Internal.List.Associative
  {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → β} : (Std.Internal.List.Option.dmap✝ x fun a x => f a) = Option.map f x
• Option.map.eq_def 📋 Std.Data.Internal.List.Associative
  {α : Type u_1} {β : Type u_2} (f : α → β) (x✝ : Option α) : Option.map f x✝ = match x✝ with | some x => some (f x) | none => none
• Std.Internal.List.minKey?.eq_1 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [Ord α] (xs : List ((a : α) × β a)) : Std.Internal.List.minKey? xs = Option.map Sigma.fst (Std.Internal.List.minEntry? xs)
• Std.Internal.List.Const.modifyKey_eq_alterKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] (k : α) (f : β → β) (l : List ((_ : α) × β)) : Std.Internal.List.Const.modifyKey k f l = Std.Internal.List.Const.alterKey k (fun x => Option.map f x) l
• Std.Internal.List.getValue?_eq_getEntry? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} : Std.Internal.List.getValue? a l = Option.map (fun x => x.snd) (Std.Internal.List.getEntry? a l)
• Std.Internal.List.Option.map_dmap 📋 Std.Data.Internal.List.Associative
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : Option α) (f : (a : α) → x = some a → β) (g : β → γ) : Option.map g (Std.Internal.List.Option.dmap✝ x f) = Std.Internal.List.Option.dmap✝ x fun a h => g (f a h)
• Std.Internal.List.getKey?_eq_getEntry? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} {a : α} : Std.Internal.List.getKey? a l = Option.map (fun x => x.fst) (Std.Internal.List.getEntry? a l)
• Std.Internal.List.Const.getValue?_modifyKey_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValue? k (Std.Internal.List.Const.modifyKey k f l) = Option.map f (Std.Internal.List.getValue? k l)
• Std.Internal.List.Const.getValueD_modifyKey_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} {fallback : β} {f : β → β} (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueD k (Std.Internal.List.Const.modifyKey k f l) fallback = (Option.map f (Std.Internal.List.getValue? k l)).getD fallback
• Std.Internal.List.modifyKey_eq_alterKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) (l : List ((a : α) × β a)) : Std.Internal.List.modifyKey k f l = Std.Internal.List.alterKey k (fun x => Option.map f x) l
• Std.Internal.List.Const.getValue!_modifyKey_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k : α} [Inhabited β] {f : β → β} (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValue! k (Std.Internal.List.Const.modifyKey k f l) = (Option.map f (Std.Internal.List.getValue? k l)).get!
• Std.Internal.List.getEntry?_eq_getValueCast? 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} : Std.Internal.List.getEntry? a l = Option.map (fun v => ⟨a, v⟩) (Std.Internal.List.getValueCast? a l)
• Std.Internal.List.getValueCast?_modifyKey_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {f : β k → β k} (l : List ((a : α) × β a)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueCast? k (Std.Internal.List.modifyKey k f l) = Option.map f (Std.Internal.List.getValueCast? k l)
• Std.Internal.List.getValueCastD_modifyKey_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k} (l : List ((a : α) × β a)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueCastD k (Std.Internal.List.modifyKey k f l) fallback = (Option.map f (Std.Internal.List.getValueCast? k l)).getD fallback
• Std.Internal.List.getValueCast!_modifyKey_self 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {k : α} [Inhabited (β k)] {f : β k → β k} (l : List ((a : α) × β a)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueCast! k (Std.Internal.List.modifyKey k f l) = (Option.map f (Std.Internal.List.getValueCast? k l)).get!
• Std.Internal.List.Const.getValue?_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValue? k' (Std.Internal.List.Const.modifyKey k f l) = if (k == k') = true then Option.map f (Std.Internal.List.getValue? k l) else Std.Internal.List.getValue? k' l
• Std.Internal.List.Const.maxKey?_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β} {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) : Std.Internal.List.maxKey? (Std.Internal.List.Const.modifyKey k f l) = Option.map (fun km => if (km == k) = true then k else km) (Std.Internal.List.maxKey? l)
• Std.Internal.List.Const.minKey?_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β} {l : List ((_ : α) × β)} (hd : Std.Internal.List.DistinctKeys l) : Std.Internal.List.minKey? (Std.Internal.List.Const.modifyKey k f l) = Option.map (fun km => if (km == k) = true then k else km) (Std.Internal.List.minKey? l)
• Std.Internal.List.Const.getValueD_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} {fallback : β} {f : β → β} (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueD k' (Std.Internal.List.Const.modifyKey k f l) fallback = if (k == k') = true then (Option.map f (Std.Internal.List.getValue? k l)).getD fallback else Std.Internal.List.getValueD k' l fallback
• Std.Internal.List.Const.getValue!_modifyKey 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {k k' : α} [hi : Inhabited β] {f : β → β} (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValue! k' (Std.Internal.List.Const.modifyKey k f l) = if (k == k') = true then (Option.map f (Std.Internal.List.getValue? k l)).get! else Std.Internal.List.getValue! k' l
• Std.Internal.List.Const.getValue?_map_of_getKey?_eq_some 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {f : α → β → γ} {l : List ((_ : α) × β)} (hl : Std.Internal.List.DistinctKeys l) {k k' : α} (h : Std.Internal.List.getKey? k l = some k') : Std.Internal.List.getValue? k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) = Option.map (f k') (Std.Internal.List.getValue? k l)
• Std.Internal.List.getValueCast?_map 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [LawfulBEq α] {f : (a : α) → β a → γ a} {l : List ((a : α) × β a)} {k : α} (hl : Std.Internal.List.DistinctKeys l) : Std.Internal.List.getValueCast? k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) = Option.map (f k) (Std.Internal.List.getValueCast? k l)
• Std.Internal.List.DistinctKeys.filterMap 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {f : (a : α) → β a → Option (γ a)} : Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision bce1d65