Loogle!

Result

Found 37687 declarations whose name contains "map". Of these, only the first 200 are shown.

• Option.map 📋 Init.Prelude
  {α : Type u_1} {β : Type u_2} (f : α → β) : Option α → Option β
• Functor.mapConst 📋 Init.Prelude
  {f : Type u → Type v} [self : Functor f] {α β : Type u} : α → f β → f α
• Functor.map 📋 Init.Prelude
  {f : Type u → Type v} [self : Functor f] {α β : Type u} : (α → β) → f α → f β
• EStateM.map 📋 Init.Prelude
  {ε σ α β : Type u} (f : α → β) (x : EStateM ε σ α) : EStateM ε σ β
• MonadFunctorT.monadMap 📋 Init.Prelude
  {m : Type u → Type v} {n : Type u → Type w} [self : MonadFunctorT m n] {α : Type u} : ({β : Type u} → m β → m β) → n α → n α
• MonadFunctor.monadMap 📋 Init.Prelude
  {m : semiOutParam (Type u → Type v)} {n : Type u → Type w} [self : MonadFunctor m n] {α : Type u} : ({β : Type u} → m β → m β) → n α → n α
• Thunk.map 📋 Init.Core
  {α : Type u_1} {β : Type u_2} (f : α → β) (x : Thunk α) : Thunk β
• Prod.map 📋 Init.Core
  {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
• Task.map 📋 Init.Core
  {α : Type u_1} {β : Type u_2} (f : α → β) (x : Task α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : Task β
• Prod.map_fst 📋 Init.Core
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α × γ) : (Prod.map f g x).1 = f x.1
• Prod.map_snd 📋 Init.Core
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α × γ) : (Prod.map f g x).2 = g x.2
• Prod.map_apply 📋 Init.Core
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α) (y : γ) : Prod.map f g (x, y) = (f x, g y)
• Functor.mapRev 📋 Init.Control.Basic
  {f : Type u → Type v} [Functor f] {α β : Type u} : f α → (α → β) → f β
• Except.map 📋 Init.Control.Except
  {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → β) : Except ε α → Except ε β
• Except.mapError 📋 Init.Control.Except
  {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : ε → ε') : Except ε α → Except ε' α
• ExceptT.map 📋 Init.Control.Except
  {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β
• Except.map_id 📋 Init.Control.Except
  {ε : Type u} {α : Type u_1} : Except.map id = id
• Except.map.eq_1 📋 Init.Control.Except
  {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → β) (err : ε) : Except.map f (Except.error err) = Except.error err
• Except.map.eq_2 📋 Init.Control.Except
  {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → β) (v : α) : Except.map f (Except.ok v) = Except.ok (f v)
• StateT.map 📋 Init.Control.State
  {σ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → β) (x : StateT σ m α) : StateT σ m β
• List.map 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) (l : List α) : List β
• List.mapTR 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) (as : List α) : List β
• List.filterMap 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → Option β) : List α → List β
• List.flatMap 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (b : α → List β) (as : List α) : List β
• List.mapTR.loop 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) : List α → 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.filterMap_nil 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} {f : α → Option β} : List.filterMap f [] = []
• List.flatMap_nil 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} {f : α → List β} : List.flatMap f [] = []
• List.nil_flatMap 📋 Init.Data.List.Basic
  {α : Type u_1} {β : Type u_2} {f : α → List β} : List.flatMap f [] = []
• List.mapTR.loop.eq_1 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) (x✝ : List β) : List.mapTR.loop f [] x✝ = x✝.reverse
• List.mapTR.eq_1 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) (as : List α) : List.mapTR f as = List.mapTR.loop f as []
• 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.mapTR.loop.eq_2 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) (x✝ : List β) (a : α) (as : List α) : List.mapTR.loop f (a :: as) x✝ = List.mapTR.loop f as (f a :: x✝)
• 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.cons_flatMap 📋 Init.Data.List.Basic
  {α : Type u_1} {β : Type u_2} {x : α} {xs : List α} {f : α → List β} : List.flatMap f (x :: xs) = f x ++ List.flatMap f xs
• List.flatMap_cons 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} {x : α} {xs : List α} {f : α → List β} : List.flatMap f (x :: xs) = f x ++ List.flatMap f xs
• List.filterMap_cons 📋 Init.Data.List.Basic
  {α : Type u} {β : Type v} {f : α → Option β} {a : α} {l : List α} : List.filterMap f (a :: l) = match f a with | none => List.filterMap f l | some b => b :: List.filterMap f l
• String.map 📋 Init.Data.String.Basic
  (f : Char → Char) (s : String) : String
• String.mapAux 📋 Init.Data.String.Basic
  (f : Char → Char) (i : String.Pos) (s : String) : String
• String.mapAux_lemma 📋 Init.Data.String.Basic
  (s : String) (i : String.Pos) (c : Char) (h : ¬s.atEnd i = true) : (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx < s.endPos.byteIdx - i.byteIdx
• String.mapAux.eq_def 📋 Init.Data.String.Basic
  (f : Char → Char) (i : String.Pos) (s : String) : String.mapAux f i s = if h : s.atEnd i = true then s else let c := f (s.get i); let_fun this := ⋯; let s := s.set i c; String.mapAux f (s.next i) s
• Option.mapA 📋 Init.Data.Option.Basic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative m] (f : α → m β) : Option α → m (Option β)
• Option.mapM 📋 Init.Data.Option.Basic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative m] (f : α → m β) : Option α → m (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.map 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β
• Array.concatMap 📋 Init.Data.Array.Basic
  {α : Type u_1} {β : Type u_2} (f : α → Array β) (as : Array α) : Array β
• Array.flatMap 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type u_1} (f : α → Array β) (as : Array α) : Array β
• Array.mapIdx 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} (f : ℕ → α → β) (as : Array α) : Array β
• Array.mapM 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β)
• Array.mapMUnsafe 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β)
• Array.sequenceMap 📋 Init.Data.Array.Basic
  {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [Monad m] (f : α → m β) (as : Array α) : m (Array β)
• Array.concatMapM 📋 Init.Data.Array.Basic
  {α : Type u_1} {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β)
• Array.flatMapM 📋 Init.Data.Array.Basic
  {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β)
• Array.mapIdxM 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : ℕ → α → m β) (as : Array α) : m (Array β)
• Array.mapFinIdx 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} (as : Array α) (f : (i : ℕ) → α → i < as.size → β) : Array β
• Array.mapMUnsafe.map 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (sz i : USize) (bs : Array NonScalar) : m (Array PNonScalar)
• Array.mapM.map 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) (i : ℕ) (bs : Array β) : m (Array β)
• Array.filterMap 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type u_1} (f : α → Option β) (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : Array β
• Array.mapFinIdxM 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : (i : ℕ) → α → i < as.size → m β) : m (Array β)
• Array.filterMapM 📋 Init.Data.Array.Basic
  {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : α → m (Option β)) (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : m (Array β)
• 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)
• Array.mapFinIdxM.map 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : (i : ℕ) → α → i < as.size → m β) (i j : ℕ) (inv : i + j = as.size) (bs : Array β) : m (Array β)
• Array.mapM.map.eq_def 📋 Init.Data.Array.Basic
  {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) (i : ℕ) (bs : Array β) : Array.mapM.map f as i bs = if hlt : i < as.size then do let __do_lift ← f as[i] Array.mapM.map f as (i + 1) (bs.push __do_lift) else pure bs
• Array.mapSepElems 📋 Init.Meta
  (a : Array Lean.Syntax) (f : Lean.Syntax → Lean.Syntax) : Array Lean.Syntax
• Array.mapSepElemsM 📋 Init.Meta
  {m : Type → Type} [Monad m] (a : Array Lean.Syntax) (f : Lean.Syntax → m Lean.Syntax) : m (Array Lean.Syntax)
• Functor.map_unit 📋 Init.Control.Lawful.Basic
  {f : Type u_1 → Type u_2} [Functor f] [LawfulFunctor f] {a : f PUnit.{u_1 + 1}} : (fun x => PUnit.unit) <$> a = a
• id_map' 📋 Init.Control.Lawful.Basic
  {f : Type u_1 → Type u_2} {α : Type u_1} [Functor f] [LawfulFunctor f] (x : f α) : (fun a => a) <$> x = x
• Id.map_eq 📋 Init.Control.Lawful.Basic
  {α β : Type u_1} (x : Id α) (f : α → β) : f <$> x = f x
• LawfulFunctor.id_map 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Functor f} [self : LawfulFunctor f] {α : Type u} (x : f α) : id <$> x = x
• map_congr 📋 Init.Control.Lawful.Basic
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Functor m] {x : m α} {f g : α → β} (h : ∀ (a : α), f a = g a) : f <$> x = g <$> x
• LawfulFunctor.map_const 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Functor f} [self : LawfulFunctor f] {α β : Type u} : Functor.mapConst = Functor.map ∘ Function.const β
• LawfulApplicative.map_pure 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Applicative f} [self : LawfulApplicative f] {α β : Type u} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• Functor.map_map 📋 Init.Control.Lawful.Basic
  {f : Type u_1 → Type u_2} {α β γ : Type u_1} [Functor f] [LawfulFunctor f] (m : α → β) (g : β → γ) (x : f α) : g <$> m <$> x = (fun a => g (m a)) <$> x
• LawfulFunctor.comp_map 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Functor f} [self : LawfulFunctor f] {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α) : (h ∘ g) <$> x = h <$> g <$> x
• LawfulMonad.map_pure' 📋 Init.Control.Lawful.Basic
  {m : Type u_1 → Type u_2} {α β : Type u_1} {f : α → β} [Monad m] [LawfulMonad m] {a : α} : f <$> pure a = pure (f a)
• map_eq_pure_bind 📋 Init.Control.Lawful.Basic
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = do let a ← x pure (f a)
• seq_eq_bind_map 📋 Init.Control.Lawful.Basic
  {m : Type u → Type u_1} {α β : Type u} [Monad m] [LawfulMonad m] (f : m (α → β)) (x : m α) : f <*> x = do let x_1 ← f x_1 <$> x
• LawfulMonad.bind_map 📋 Init.Control.Lawful.Basic
  {m : Type u → Type v} {inst✝ : Monad m} [self : LawfulMonad m] {α β : Type u} (f : m (α → β)) (x : m α) : (do let x_1 ← f x_1 <$> x) = f <*> x
• bind_map_left 📋 Init.Control.Lawful.Basic
  {m : Type u_1 → Type u_2} {α β γ : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : m α) (g : β → m γ) : (do let b ← f <$> x g b) = do let a ← x g (f a)
• LawfulMonad.map_map 📋 Init.Control.Lawful.Basic
  {α α✝ a✝ : Type u_1} {g : α✝ → a✝} {f : α → α✝} {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {x : m α} : g <$> f <$> x = (fun a => g (f a)) <$> x
• map_bind 📋 Init.Control.Lawful.Basic
  {m : Type u_1 → Type u_2} {β γ α : Type u_1} [Monad m] [LawfulMonad m] (f : β → γ) (x : m α) (g : α → m β) : f <$> (x >>= g) = do let a ← x f <$> g a
• ReaderT.run_mapConst 📋 Init.Control.Lawful.Instances
  {m : Type u_1 → Type u_2} {α ρ β : Type u_1} [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ) : (Functor.mapConst a x).run ctx = Functor.mapConst a (x.run ctx)
• ReaderT.run_map 📋 Init.Control.Lawful.Instances
  {m : Type u_1 → Type u_2} {α β ρ : Type u_1} [Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ) : (f <$> x).run ctx = f <$> x.run ctx
• ReaderT.run_monadMap 📋 Init.Control.Lawful.Instances
  {n : Type u → Type u_1} {m : Type u → Type u_2} {ρ α : Type u} [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ) : (monadMap f x).run ctx = monadMap f (x.run ctx)
• StateT.run_monadMap 📋 Init.Control.Lawful.Instances
  {n : Type u → Type u_1} {m : Type u → Type u_2} {σ α : Type u} [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ) : (monadMap f x).run s = monadMap f (x.run s)
• ExceptT.run_map 📋 Init.Control.Lawful.Instances
  {m : Type u_1 → Type u_2} {α β ε : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α) : (f <$> x).run = Except.map f <$> x.run
• ExceptT.map_throw 📋 Init.Control.Lawful.Instances
  {m : Type u_1 → Type u_2} {ε : Type u_1} [Monad m] [LawfulMonad m] {α β : Type u_1} (f : α → β) (e : ε) : f <$> throw e = throw e
• StateT.map.eq_1 📋 Init.Control.Lawful.Instances
  {σ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → β) (x : StateT σ m α) (s : σ) : StateT.map f x s = do let __discr ← x s match __discr with | (a, s) => pure (f a, s)
• StateT.run_map 📋 Init.Control.Lawful.Instances
  {m : Type u → Type u_1} {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun p => (f p.1, p.2)) <$> x.run s
• ExceptT.map.eq_1 📋 Init.Control.Lawful.Instances
  {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT.map f x = ExceptT.mk do let a ← x match a with | Except.ok a => pure (Except.ok (f a)) | Except.error e => pure (Except.error e)
• map_inj_of_left_inverse 📋 Init.Control.Lawful.Lemmas
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Functor m] [LawfulFunctor m] {f : α → β} (w : ∃ g, ∀ (x : α), g (f x) = x) {x y : m α} : f <$> x = f <$> y ↔ x = y
• map_inj_right_of_nonempty 📋 Init.Control.Lawful.Lemmas
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Functor m] [LawfulFunctor m] [Nonempty α] {f : α → β} (w : ∀ {x y : α}, f x = f y → x = y) {x y : m α} : f <$> x = f <$> y ↔ x = y
• map_inj_right 📋 Init.Control.Lawful.Lemmas
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] {f : α → β} (h : ∀ {x y : α}, f x = f y → x = y) {x y : m α} : f <$> x = f <$> y ↔ x = y
• Prod.map_id 📋 Init.Data.Prod
  {α : Type u_1} {β : Type u_2} : Prod.map id id = id
• Prod.map_id' 📋 Init.Data.Prod
  {α : Type u_1} {β : Type u_2} : (Prod.map (fun a => a) fun b => b) = fun x => x
• Prod.map_map 📋 Init.Data.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) (x : α × γ) : Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x
• Prod.map_comp_swap 📋 Init.Data.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) : Prod.map f g ∘ Prod.swap = Prod.swap ∘ Prod.map g f
• Prod.map_comp_map 📋 Init.Data.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) : Prod.map g g' ∘ Prod.map f f' = Prod.map (g ∘ f) (g' ∘ f')
• Option.pmap 📋 Init.Data.Option.Instances
  {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (o : Option α) : (∀ (a : α), o = some a → p a) → Option β
• 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.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.pmap_none 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), none = some a → p a} : Option.pmap f none h = none
• Option.pmap.eq_1 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (x_2 : ∀ (a : α), none = some a → p a) : Option.pmap f none x_2 = none
• 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.isNone_pmap 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a} : (Option.pmap f o h).isNone = o.isNone
• Option.isSome_pmap 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a} : (Option.pmap f o h).isSome = o.isSome
• 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.pmap_isSome 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a} : (Option.pmap f o h).isSome = o.isSome
• 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.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.pmap_eq_none_iff 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {o : Option α} {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), o = some a → p a} : Option.pmap f o h = none ↔ o = none
• Option.pmap_pred_congr 📋 Init.Data.Option.Lemmas
  {α : Type u} {p p' : α → Prop} (hp : ∀ (x : α), p x ↔ p' x) {o o' : Option α} (ho : o = o') (h : ∀ (x : α), o = some x → p x) (x : α) : o' = some x → p' x
• Option.pmap.eq_2 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (a : α) (H : ∀ (a_1 : α), some a = some a_1 → p a_1) : Option.pmap f (some a) H = some (f a ⋯)
• 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.pmap_some 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {a : α} {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a_1 : α), some a = some a_1 → p a_1} : Option.pmap f (some a) h = some (f a ⋯)
• 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.elim_pmap 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Sort u_3} {p : α → Prop} (f : (a : α) → p a → β) (o : Option α) (H : ∀ (a : α), o = some a → p a) (g : γ) (g' : β → γ) : (Option.pmap f o H).elim g g' = o.pelim g fun a h => g' (f a ⋯)
• Option.pmap_eq_some_iff 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {b : β} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a} : Option.pmap f o h = some b ↔ ∃ a, ∃ (h : p a), o = some a ∧ b = f a 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.pmap_congr 📋 Init.Data.Option.Lemmas
  {α : Type u} {β : Type v} {p p' : α → Prop} (hp : ∀ (x : α), p x ↔ p' x) {f : (x : α) → p x → β} {f' : (x : α) → p' x → β} (hf : ∀ (x : α) (h : p' x), f x ⋯ = f' x h) {o o' : Option α} (ho : o = o') {h : ∀ (x : α), o = some x → p x} : Option.pmap f o h = Option.pmap f' o' ⋯
• 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_or 📋 Init.Data.Option.Lemmas
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o o' : Option α} {h : ∀ (a : α), o.or o' = some a → p a} : Option.pmap f (o.or o') h = match o, h with | none, h => Option.pmap f o' ⋯ | some a, h => some (f a ⋯)
• 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.mapMono 📋 Init.Data.List.BasicAux
  {α : Type u_1} (as : List α) (f : α → α) : List α
• List.mapMonoM 📋 Init.Data.List.BasicAux
  {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (as : List α) (f : α → m α) : m (List α)
• List.partitionMap 📋 Init.Data.List.BasicAux
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β ⊕ γ) (l : List α) : List β × List γ
• List.partitionMap.go 📋 Init.Data.List.BasicAux
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β ⊕ γ) : List α → Array β → Array γ → List β × List γ
• List.mapA 📋 Init.Data.List.Control
  {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
• List.mapM 📋 Init.Data.List.Control
  {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) (as : List α) : m (List β)
• List.filterMapM 📋 Init.Data.List.Control
  {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (as : List α) : m (List β)
• List.flatMapM 📋 Init.Data.List.Control
  {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α) : m (List β)
• List.mapM.loop 📋 Init.Data.List.Control
  {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → List β → m (List β)
• List.filterMapM.loop 📋 Init.Data.List.Control
  {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → List β → m (List β)
• List.flatMapM.loop 📋 Init.Data.List.Control
  {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) : List α → List (List β) → m (List β)
• List.filterMap_some 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} : List.filterMap some l = l
• 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.filterMap_some_fun 📋 Init.Data.List.Lemmas
  {α : Type u_1} : List.filterMap some = id
• 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.filterMap.eq_1 📋 Init.Data.List.Lemmas
  {α : Type u} {β : Type v} (f : α → Option β) : List.filterMap f [] = []
• List.flatMap_singleton' 📋 Init.Data.List.Lemmas
  {α : Type u_1} (l : List α) : List.flatMap (fun x => [x]) l = l
• List.flatMap_id 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List α)} : List.flatMap id L = L.flatten
• List.flatMap_id' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List α)} : List.flatMap (fun as => as) L = L.flatten
• List.flatten_eq_flatMap 📋 Init.Data.List.Lemmas
  {α : Type u_1} {L : List (List α)} : L.flatten = List.flatMap id L
• 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.filterMap_eq_filter 📋 Init.Data.List.Lemmas
  {α : Type u_1} {p : α → Bool} : List.filterMap (Option.guard fun x => p x) = List.filter p
• List.flatMap_singleton 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} (f : α → List β) (x : α) : List.flatMap f [x] = f x
• List.length_filterMap_le 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : (List.filterMap f l).length ≤ l.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.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 = []

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