Loogle!

Result

Found 371 declarations mentioning Functor.map. Of these, only the first 200 are shown.

• Functor.map 📋 Init.Prelude
  {f : Type u → Type v} [self : Functor f] {α β : Type u} : (α → β) → f α → f β
• 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
• LawfulApplicative.pure_seq 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Applicative f} [self : LawfulApplicative f] {α β : Type u} (g : α → β) (x : f α) : pure g <*> x = g <$> 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)
• LawfulApplicative.seq_pure 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Applicative f} [self : LawfulApplicative f] {α β : Type u} (g : f (α → β)) (x : α) : g <*> pure x = (fun h => h x) <$> g
• 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)
• LawfulMonad.bind_pure_comp 📋 Init.Control.Lawful.Basic
  {m : Type u → Type v} {inst✝ : Monad m} [self : LawfulMonad m] {α β : Type u} (f : α → β) (x : m α) : (do let a ← x pure (f a)) = f <$> x
• LawfulApplicative.seqLeft_eq 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Applicative f} [self : LawfulApplicative f] {α β : Type u} (x : f α) (y : f β) : x <* y = Function.const β <$> x <*> y
• LawfulApplicative.seqRight_eq 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Applicative f} [self : LawfulApplicative f] {α β : Type u} (x : f α) (y : f β) : x *> y = Function.const α id <$> x <*> y
• seq_eq_bind 📋 Init.Control.Lawful.Basic
  {m : Type u → Type u_1} {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α) : mf <*> x = do let f ← mf f <$> x
• 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
• LawfulApplicative.seq_assoc 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Applicative f} [self : LawfulApplicative f] {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• LawfulFunctor.mk 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} [Functor f] (map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β) (id_map : ∀ {α : Type u} (x : f α), id <$> x = x) (comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x) : LawfulFunctor f
• LawfulMonad.mk 📋 Init.Control.Lawful.Basic
  {m : Type u → Type v} [Monad m] [toLawfulApplicative : LawfulApplicative m] (bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α), (do let a ← x pure (f a)) = f <$> x) (bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α), (do let x_1 ← f x_1 <$> x) = f <*> x) (pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x) (bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g) : LawfulMonad m
• LawfulApplicative.mk 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} [Applicative f] [toLawfulFunctor : LawfulFunctor f] (seqLeft_eq : ∀ {α β : Type u} (x : f α) (y : f β), x <* y = Function.const β <$> x <*> y) (seqRight_eq : ∀ {α β : Type u} (x : f α) (y : f β), x *> y = Function.const α id <$> x <*> y) (pure_seq : ∀ {α β : Type u} (g : α → β) (x : f α), pure g <*> x = g <$> x) (map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)) (seq_pure : ∀ {α β : Type u} (g : f (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g) (seq_assoc : ∀ {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)), h <*> (g <*> x) = Function.comp <$> h <*> g <*> x) : LawfulApplicative f
• LawfulMonad.mk' 📋 Init.Control.Lawful.Basic
  (m : Type u → Type v) [Monad m] (id_map : ∀ {α : Type u} (x : m α), id <$> x = x) (pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x) (bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g) (map_const : ∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <$> y := by intros; rfl) (seqLeft_eq : ∀ {α β : Type u} (x : m α) (y : m β), x <* y = do let a ← x let _ ← y pure a := by intros; rfl) (seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), x *> y = do let _ ← x y := by intros; rfl) (bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α), (do let y ← x pure (f y)) = f <$> x := by intros; rfl) (bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α), (do let x_1 ← f x_1 <$> x) = f <*> x := by intros; rfl) : LawfulMonad m
• ExceptT.run_lift 📋 Init.Control.Lawful.Instances
  {m : Type u → Type v} {α ε : Type u} [Monad m] (x : m α) : (ExceptT.lift x).run = Except.ok <$> x
• ExceptT.lift.eq_1 📋 Init.Control.Lawful.Instances
  {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) : ExceptT.lift t = ExceptT.mk (Except.ok <$> t)
• StateT.run'_eq 📋 Init.Control.Lawful.Instances
  {m : Type u_1 → Type u_2} {σ α : Type u_1} [Monad m] (x : StateT σ m α) (s : σ) : x.run' s = (fun x => x.1) <$> x.run s
• 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
• 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
• ExceptT.bind_pure_comp 📋 Init.Control.Lawful.Instances
  {m : Type u_1 → Type u_2} {α β ε : Type u_1} [Monad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x
• ExceptT.seq_eq 📋 Init.Control.Lawful.Instances
  {m : Type u → Type u_1} {α β ε : Type u} [Monad m] (mf : ExceptT ε m (α → β)) (x : ExceptT ε m α) : mf <*> x = do let f ← mf f <$> x
• 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.seqLeft_eq 📋 Init.Control.Lawful.Instances
  {α β ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = Function.const β <$> x <*> y
• StateT.seqLeft_eq 📋 Init.Control.Lawful.Instances
  {m : Type u_1 → Type u_2} {σ α β : Type u_1} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x <* y = Function.const β <$> x <*> y
• ExceptT.seqRight_eq 📋 Init.Control.Lawful.Instances
  {m : Type u_1 → Type u_2} {ε α β : Type u_1} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x *> y = Function.const α id <$> x <*> y
• StateT.seqRight_eq 📋 Init.Control.Lawful.Instances
  {m : Type u_1 → Type u_2} {σ α β : Type u_1} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x *> y = Function.const α id <$> x <*> y
• StateT.run_seq 📋 Init.Control.Lawful.Instances
  {m : Type u → Type u_1} {α β σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α) (s : σ) : (f <*> x).run s = do let fs ← f.run s (fun p => (fs.1 p.1, p.2)) <$> x.run fs.2
• 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
• Option.map_eq_map 📋 Init.Data.Option.Lemmas
  {α✝ α✝¹ : Type u_1} {f : α✝ → α✝¹} : Functor.map f = Option.map f
• List.getElem?_set_self' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} {i : ℕ} {a : α} : (l.set i a)[i]? = Function.const α a <$> l[i]?
• List.getElem?_set' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l : List α} {i j : ℕ} {a : α} : (l.set i a)[j]? = if i = j then Function.const α a <$> l[j]? else l[j]?
• List.zipWithAll_map_left 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {α' : Type u_1} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {f : α → α'} {g : Option α' → Option β → γ} : List.zipWithAll g (List.map f l₁) l₂ = List.zipWithAll (fun a b => g (f <$> a) b) l₁ l₂
• List.zipWithAll_map_right 📋 Init.Data.List.Zip
  {α : Type u_1} {β β' : Type u_2} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {f : β → β'} {g : Option α → Option β' → γ} : List.zipWithAll g l₁ (List.map f l₂) = List.zipWithAll (fun a b => g a (f <$> b)) l₁ l₂
• List.zipWithAll_map 📋 Init.Data.List.Zip
  {γ : Type u_1} {δ : Type u_2} {α : Type u_1} {β : Type u_2} {μ : Type u_3} {f : Option γ → Option δ → μ} {g : α → γ} {h : β → δ} {l₁ : List α} {l₂ : List β} : List.zipWithAll f (List.map g l₁) (List.map h l₂) = List.zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂
• List.getElem?_modify_eq 📋 Init.Data.List.Nat.Modify
  {α : Type u_1} (f : α → α) (i : ℕ) (l : List α) : (l.modify i f)[i]? = f <$> l[i]?
• List.getElem?_modify 📋 Init.Data.List.Nat.Modify
  {α : Type u_1} (f : α → α) (i : ℕ) (l : List α) (j : ℕ) : (l.modify i f)[j]? = (fun a => if i = j then f a else a) <$> l[j]?
• List.allM_eq_not_anyM_not 📋 Init.Data.List.Monadic
  {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} : List.allM p as = (fun x => !x) <$> List.anyM (fun x => (fun x => !x) <$> p x) as
• List.mapA.eq_2 📋 Init.Data.List.Monadic
  {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) (a : α) (as : List α) : List.mapA f (a :: as) = List.cons <$> f a <*> List.mapA f as
• List.filterMapM_loop_eq 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → m (Option β)} {l : List α} {acc : List β} : List.filterMapM.loop f l acc = (fun x => acc.reverse ++ x) <$> List.filterMapM.loop f l []
• List.flatMapM_loop_eq 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → m (List β)} {l : List α} {acc : List (List β)} : List.flatMapM.loop f l acc = (fun x => acc.reverse.flatten ++ x) <$> List.flatMapM.loop f l []
• List.mapM_eq_reverse_foldlM_cons 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} : List.mapM f l = List.reverse <$> List.foldlM (fun acc a => do let __do_lift ← f a pure (__do_lift :: acc)) [] l
• List.forIn_yield_eq_foldlM 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] {l : List α} (f : α → β → m γ) (g : α → β → γ → β) (init : β) : (forIn l init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = List.foldlM (fun b a => g a b <$> f a b) init l
• List.forIn_eq_foldlM 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} (f : α → β → m (ForInStep β)) (init : β) : forIn l init f = ForInStep.value <$> List.foldlM (fun b a => match b with | ForInStep.yield b => f a b | ForInStep.done b => pure (ForInStep.done b)) (ForInStep.yield init) l
• List.foldlM_cons_eq_append 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → m β} {as : List α} {b : β} {bs : List β} : List.foldlM (fun acc a => do let __do_lift ← f a pure (__do_lift :: acc)) (b :: bs) as = (fun x => x ++ b :: bs) <$> List.foldlM (fun acc a => do let __do_lift ← f a pure (__do_lift :: acc)) [] as
• List.forIn'_eq_foldlM 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) : forIn' l init f = ForInStep.value <$> List.foldlM (fun b x => match x with | ⟨a, m_1⟩ => match b with | ForInStep.yield b => f a m_1 b | ForInStep.done b => pure (ForInStep.done b)) (ForInStep.yield init) l.attach
• List.forIn'_yield_eq_foldlM 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] {l : List α} (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) : (forIn' l init fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) = List.foldlM (fun b x => match x with | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b) init l.attach
• Array.mapM_eq_mapM_toList 📋 Init.Data.Array.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α} : Array.mapM f xs = List.toArray <$> List.mapM f xs.toList
• Array.toList_mapM 📋 Init.Data.Array.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α} : Array.toList <$> Array.mapM f xs = List.mapM f xs.toList
• List.mapM_toArray 📋 Init.Data.Array.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} : Array.mapM f l.toArray = List.toArray <$> List.mapM f l
• Array.mapM_eq_foldlM.aux 📋 Init.Data.Array.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α} (i : ℕ) (bs : Array β) : Array.mapM.map f xs i bs = List.foldlM (fun bs a => bs.push <$> f a) bs (List.drop i xs.toList)
• Array.mapM_eq_foldlM 📋 Init.Data.Array.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α} : Array.mapM f xs = Array.foldlM (fun bs a => bs.push <$> f a) #[] xs
• Array.allM_eq_not_anyM_not 📋 Init.Data.Array.Lemmas
  {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α} : Array.allM p as = (fun x => !x) <$> Array.anyM (fun x => (fun x => !x) <$> p x) as
• Array.toList_mapIdxM 📋 Init.Data.Array.MapIdx
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} {f : ℕ → α → m β} : Array.toList <$> Array.mapIdxM f xs = List.mapIdxM f xs.toList
• List.mapIdxM_toArray 📋 Init.Data.Array.MapIdx
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : ℕ → α → m β} : Array.mapIdxM f l.toArray = List.toArray <$> List.mapIdxM f l
• Array.toList_mapFinIdxM 📋 Init.Data.Array.MapIdx
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} {f : (i : ℕ) → α → i < xs.size → m β} : Array.toList <$> xs.mapFinIdxM f = xs.toList.mapFinIdxM f
• List.mapFinIdxM_toArray 📋 Init.Data.Array.MapIdx
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : (i : ℕ) → α → i < l.length → m β} : l.toArray.mapFinIdxM f = List.toArray <$> l.mapFinIdxM f
• List.mapFinIdxM_toArray.go 📋 Init.Data.Array.MapIdx
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : (i : ℕ) → α → i < l.length → m β} (i : ℕ) (acc : Array β) (inv : i + acc.size = l.length) : Array.mapFinIdxM.map l.toArray f i acc.size inv acc = List.toArray <$> List.mapFinIdxM.go l f (List.drop acc.size l) acc ⋯
• 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.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.toList_filterM 📋 Init.Data.Array.Monadic
  {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] {xs : Array α} {p : α → m Bool} : Array.toList <$> Array.filterM p xs = List.filterM p xs.toList
• Array.toList_filterRevM 📋 Init.Data.Array.Monadic
  {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] {xs : Array α} {p : α → m Bool} : Array.toList <$> Array.filterRevM p xs = List.filterRevM p xs.toList
• List.filterM_toArray 📋 Init.Data.Array.Monadic
  {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} : Array.filterM p l.toArray = List.toArray <$> List.filterM p l
• List.filterRevM_toArray 📋 Init.Data.Array.Monadic
  {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} : Array.filterRevM p l.toArray = List.toArray <$> List.filterRevM p l
• Array.toList_filterMapM 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} {f : α → m (Option β)} : Array.toList <$> Array.filterMapM f xs = List.filterMapM f xs.toList
• List.filterM_toArray' 📋 Init.Data.Array.Monadic
  {m : Type → Type u_1} {α : Type} {stop : ℕ} [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} (w : stop = l.length) : Array.filterM p l.toArray 0 stop = List.toArray <$> List.filterM p l
• List.filterRevM_toArray' 📋 Init.Data.Array.Monadic
  {m : Type → Type u_1} {α : Type} {start : ℕ} [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} (w : start = l.length) : Array.filterRevM p l.toArray start = List.toArray <$> List.filterRevM p l
• List.filterMapM_toArray 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} : Array.filterMapM f l.toArray = List.toArray <$> List.filterMapM f l
• List.filterMapM_toArray' 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : ℕ} [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} (w : stop = l.length) : Array.filterMapM f l.toArray 0 stop = List.toArray <$> List.filterMapM f l
• Array.toList_flatMapM 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} {f : α → m (Array β)} : Array.toList <$> Array.flatMapM f xs = List.flatMapM (fun a => Array.toList <$> f a) xs.toList
• List.flatMapM_toArray 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Array β)} : Array.flatMapM f l.toArray = List.toArray <$> List.flatMapM (fun a => Array.toList <$> f a) l
• Array.filterRevM.eq_1 📋 Init.Data.Array.Monadic
  {m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start stop : ℕ) : Array.filterRevM p as start stop = Array.reverse <$> Array.foldrM (fun a acc => do let __do_lift ← p a if __do_lift = true then pure (acc.push a) else pure acc) #[] as start stop
• Array.forIn_yield_eq_foldlM 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} (f : α → β → m γ) (g : α → β → γ → β) (init : β) : (forIn xs init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = Array.foldlM (fun b a => g a b <$> f a b) init xs
• Array.forIn_eq_foldlM 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} (f : α → β → m (ForInStep β)) (init : β) : forIn xs init f = ForInStep.value <$> Array.foldlM (fun b a => match b with | ForInStep.yield b => f a b | ForInStep.done b => pure (ForInStep.done b)) (ForInStep.yield init) xs
• Array.forIn'_eq_foldlM 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} (f : (a : α) → a ∈ xs → β → m (ForInStep β)) (init : β) : forIn' xs init f = ForInStep.value <$> Array.foldlM (fun b x => match x with | ⟨a, m_1⟩ => match b with | ForInStep.yield b => f a m_1 b | ForInStep.done b => pure (ForInStep.done b)) (ForInStep.yield init) xs.attach
• Array.forIn'_yield_eq_foldlM 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} (f : (a : α) → a ∈ xs → β → m γ) (g : (a : α) → a ∈ xs → β → γ → β) (init : β) : (forIn' xs init fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) = Array.foldlM (fun b x => match x with | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b) init xs.attach
• Option.forIn_eq_elim 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : α → β → m (ForInStep β)) (b : β) : forIn o b f = o.elim (pure b) fun a => ForInStep.value <$> f a b
• Option.forIn'_eq_pelim 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : (a : α) → a ∈ o → β → m (ForInStep β)) (b : β) : forIn' o b f = o.pelim (pure b) fun a h => ForInStep.value <$> f a h b
• Option.forIn_yield_eq_elim 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : α → β → m γ) (g : α → β → γ → β) (b : β) : (forIn o b fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = o.elim (pure b) fun a => g a b <$> f a b
• Option.forIn'_yield_eq_pelim 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : (a : α) → a ∈ o → β → m γ) (g : (a : α) → a ∈ o → β → γ → β) (b : β) : (forIn' o b fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) = o.pelim (pure b) fun a h => g a h b <$> f a h b
• Vector.toArray_mapM 📋 Init.Data.Vector.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} : Vector.toArray <$> Vector.mapM f xs = Array.mapM f xs.toArray
• Vector.allM_eq_not_anyM_not 📋 Init.Data.Vector.Lemmas
  {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Vector α n} : Vector.allM p xs = (fun x => !x) <$> Vector.anyM (fun x => (fun x => !x) <$> p x) xs
• Vector.toArray_mapM_go 📋 Init.Data.Vector.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} {i : ℕ} (h : i ≤ n) {acc : Vector β i} : Vector.toArray <$> Vector.mapM.go f xs i h acc = Array.mapM.map f xs.toArray i acc.toArray
• Vector.toArray_mapIdxM 📋 Init.Data.Vector.MapIdx
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} {f : ℕ → α → m β} : Vector.toArray <$> Vector.mapIdxM f xs = Array.mapIdxM f xs.toArray
• Vector.toArray_mapFinIdxM 📋 Init.Data.Vector.MapIdx
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} {f : (i : ℕ) → α → i < n → m β} : Vector.toArray <$> xs.mapFinIdxM f = xs.mapFinIdxM fun i x h => f i x ⋯
• Vector.toArray_mapFinIdxM.go 📋 Init.Data.Vector.MapIdx
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} {f : (i : ℕ) → α → i < n → m β} (i j : ℕ) (inv : i + j = n) (bs : Vector β (n - i)) : Vector.toArray <$> Vector.mapFinIdxM.map xs f i j inv bs = Array.mapFinIdxM.map xs.toArray (fun i x h => f i x ⋯) i j ⋯ bs.toArray
• Vector.map_toArray_inj 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [Monad m] [LawfulMonad m] {xs ys : m (Vector α n)} : Vector.toArray <$> xs = Vector.toArray <$> ys ↔ xs = ys
• Vector.forIn_yield_eq_foldlM 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β γ : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β → m γ) (g : α → β → γ → β) (init : β) : (forIn xs init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = Vector.foldlM (fun b a => g a b <$> f a b) init xs
• Vector.forIn_eq_foldlM 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β → m (ForInStep β)) (init : β) : forIn xs init f = ForInStep.value <$> Vector.foldlM (fun b a => match b with | ForInStep.yield b => f a b | ForInStep.done b => pure (ForInStep.done b)) (ForInStep.yield init) xs
• Vector.forIn'_eq_foldlM 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} (f : (a : α) → a ∈ xs → β → m (ForInStep β)) (init : β) : forIn' xs init f = ForInStep.value <$> Vector.foldlM (fun b x => match x with | ⟨a, m_1⟩ => match b with | ForInStep.yield b => f a m_1 b | ForInStep.done b => pure (ForInStep.done b)) (ForInStep.yield init) xs.attach
• Vector.forIn'_yield_eq_foldlM 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β γ : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} (f : (a : α) → a ∈ xs → β → m γ) (g : (a : α) → a ∈ xs → β → γ → β) (init : β) : (forIn' xs init fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) = Vector.foldlM (fun b x => match x with | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b) init xs.attach
• Lean.Order.Functor.monotone_map 📋 Init.Internal.Order.Lemmas
  {m : Type u → Type v} [Monad m] [(α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α β : Type u} {γ : Type w} [Lean.Order.PartialOrder γ] [LawfulMonad m] (f : γ → m α) (g : α → β) (hmono : Lean.Order.monotone f) : Lean.Order.monotone fun x => g <$> f x
• EStateM.run_map 📋 Batteries.Lean.EStateM
  {α β ε σ : Type u_1} {s : σ} (f : α → β) (x : EStateM ε σ α) : (f <$> x).run s = EStateM.Result.map f (x.run s)
• Except.map_error 📋 Batteries.Lean.Except
  {α β : Type u_1} {ε : Type u} (f : α → β) (e : ε) : f <$> Except.error e = Except.error e
• Except.map_ok 📋 Batteries.Lean.Except
  {α β : Type u_1} {ε : Type u} (f : α → β) (x : α) : f <$> Except.ok x = Except.ok (f x)
• Except.map_pmap 📋 Batteries.Lean.Except
  {β γ : Type u_1} {ε : Type u_2} {α : Type u_1} (g : β → γ) (x : Except ε α) (f : (a : α) → x = Except.ok a → β) : g <$> x.pmap f = x.pmap fun a h => g (f a h)
• ExceptT.map_mk 📋 Batteries.Lean.Except
  {m : Type u_1 → Type u_2} {α β ε : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : m (Except ε α)) : f <$> ExceptT.mk x = ExceptT.mk ((fun x => f <$> x) <$> x)
• SatisfiesM.map_pre 📋 Batteries.Classes.SatisfiesM
  {m : Type u_1 → Type u_2} {α α✝ : Type u_1} {p : α✝ → Prop} {f : α → α✝} [Functor m] [LawfulFunctor m] {x : m α} (hx : SatisfiesM (fun a => p (f a)) x) : SatisfiesM p (f <$> x)
• SatisfiesM.map 📋 Batteries.Classes.SatisfiesM
  {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {α✝ : Type u_1} {q : α✝ → Prop} {f : α → α✝} [Functor m] [LawfulFunctor m] {x : m α} (hx : SatisfiesM p x) (hf : ∀ {a : α}, p a → q (f a)) : SatisfiesM q (f <$> x)
• SatisfiesM.map_post 📋 Batteries.Classes.SatisfiesM
  {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {α✝ : Type u_1} {f : α → α✝} [Functor m] [LawfulFunctor m] {x : m α} (hx : SatisfiesM p x) : SatisfiesM (fun b => ∃ a, p a ∧ b = f a) (f <$> x)
• MonadSatisfying.val_eq 📋 Batteries.Classes.SatisfiesM
  {m : Type u → Type v} {inst✝ : Functor m} {inst✝¹ : LawfulFunctor m} [self : MonadSatisfying m] {α : Type u} {p : α → Prop} {x : m α} (h : SatisfiesM p x) : Subtype.val <$> satisfying h = x
• SatisfiesM.eq_1 📋 Batteries.Classes.SatisfiesM
  {α : Type u} {m : Type u → Type v} [Functor m] (p : α → Prop) (x : m α) : SatisfiesM p x = ∃ x', Subtype.val <$> x' = x
• MonadSatisfying.mk 📋 Batteries.Classes.SatisfiesM
  {m : Type u → Type v} [Functor m] [LawfulFunctor m] (satisfying : {α : Type u} → {p : α → Prop} → {x : m α} → SatisfiesM p x → m { a // p a }) (val_eq : ∀ {α : Type u} {p : α → Prop} {x : m α} (h : SatisfiesM p x), Subtype.val <$> satisfying h = x) : MonadSatisfying m
• OptionT.run_monadLift 📋 Batteries.Control.OptionT
  {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α : Type u_1} [Monad m] [LawfulMonad m] [MonadLiftT n m] (x : n α) : (monadLift x).run = some <$> monadLift x
• OptionT.run_map 📋 Batteries.Control.OptionT
  {m : Type u_1 → Type u_2} {α β : Type u_1} (x : OptionT m α) (f : α → β) [Monad m] [LawfulMonad m] : (f <$> x).run = Option.map f <$> x.run
• OptionT.run_mapConst 📋 Batteries.Control.OptionT
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : OptionT m α) (y : β) : (Functor.mapConst y x).run = Option.map (Function.const α y) <$> x.run
• Option.elimM_map 📋 Batteries.Control.OptionT
  {m : Type u_1 → Type u_2} {α β γ : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (f : α → Option β) (y : m γ) (z : β → m γ) : Option.elimM (f <$> x) y z = do let __do_lift ← x (f __do_lift).elim y z
• OptionT.run_seqLeft 📋 Batteries.Control.OptionT
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) : (x <* y).run = Option.elimM x.run (pure none) fun x => Option.map (Function.const β x) <$> y.run
• OptionT.run_seq 📋 Batteries.Control.OptionT
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (f : OptionT m (α → β)) (x : OptionT m α) : (f <*> x).run = Option.elimM f.run (pure none) fun f => Option.map f <$> x.run
• LawfulAlternative.map_failure 📋 Batteries.Control.AlternativeMonad
  {m : Type u_1 → Type u_2} {inst✝ : Alternative m} [self : LawfulAlternative m] {α β : Type u_1} (f : α → β) : f <$> failure = failure
• LawfulAlternative.map_orElse 📋 Batteries.Control.AlternativeMonad
  {m : Type u_1 → Type u_2} {inst✝ : Alternative m} [self : LawfulAlternative m] {α β : Type u_1} (x y : m α) (f : α → β) : f <$> (x <|> y) = (f <$> x <|> f <$> y)
• LawfulAlternative.mk 📋 Batteries.Control.AlternativeMonad
  {m : Type u_1 → Type u_2} [Alternative m] [toLawfulApplicative : LawfulApplicative m] (map_failure : ∀ {α β : Type u_1} (f : α → β), f <$> failure = failure) (failure_seq : ∀ {α β : Type u_1} (x : m α), failure <*> x = failure) (orElse_failure : ∀ {α : Type u_1} (x : m α), (x <|> failure) = x) (failure_orElse : ∀ {α : Type u_1} (y : m α), (failure <|> y) = y) (orElse_assoc : ∀ {α : Type u_1} (x y z : m α), (x <|> y <|> z) = ((x <|> y) <|> z)) (map_orElse : ∀ {α β : Type u_1} (x y : m α) (f : α → β), f <$> (x <|> y) = (f <$> x <|> f <$> y)) : LawfulAlternative m
• liftM_map 📋 Batteries.Control.Lawful.MonadLift
  {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u_1} [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α) : liftM (f <$> ma) = f <$> liftM ma
• monadLift_map 📋 Batteries.Control.Lawful.MonadLift
  {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u_1} [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α) : monadLift (f <$> ma) = f <$> monadLift ma
• LawfulFunctor.map_inj_right_of_nonempty 📋 Batteries.Control.Monad
  {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
• LawfulMonad.map_inj_right 📋 Batteries.Control.Monad
  {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
• List.modifyNth_eq_set_get? 📋 Batteries.Data.List.Lemmas
  {α : Type u_1} (f : α → α) (n : ℕ) (l : List α) : l.modify n f = ((fun a => l.set n (f a)) <$> l[n]?).getD l
• List.modify_eq_set_get? 📋 Batteries.Data.List.Lemmas
  {α : Type u_1} (f : α → α) (n : ℕ) (l : List α) : l.modify n f = ((fun a => l.set n (f a)) <$> l[n]?).getD l
• List.modify_eq_set_getElem? 📋 Batteries.Data.List.Lemmas
  {α : Type u_1} (f : α → α) (n : ℕ) (l : List α) : l.modify n f = ((fun a => l.set n (f a)) <$> l[n]?).getD l
• List.getElem?_modifyNth_eq 📋 Batteries.Data.List.Lemmas
  {α : Type u_1} (f : α → α) (i : ℕ) (l : List α) : (l.modify i f)[i]? = f <$> l[i]?
• List.forIn_eq_bindList 📋 Batteries.Data.List.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → β → m (ForInStep β)) (l : List α) (init : β) : forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)
• List.getElem?_modifyNth 📋 Batteries.Data.List.Lemmas
  {α : Type u_1} (f : α → α) (i : ℕ) (l : List α) (j : ℕ) : (l.modify i f)[j]? = (fun a => if i = j then f a else a) <$> l[j]?
• Batteries.RBNode.forIn.eq_1 📋 Batteries.Data.RBMap.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {σ : Type u_1} [Monad m] (as : Batteries.RBNode α) (init : σ) (f : α → σ → m (ForInStep σ)) : as.forIn init f = ForInStep.run <$> Batteries.RBNode.forIn.visit f as init
• Vector.mapM_mk 📋 Batteries.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] (a : Array α) (h : a.size = n) (f : α → m β) : Vector.mapM f { toArray := a, size_toArray := h } = (fun x => match x with | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$> satisfying ⋯
• Vector.mapIdxM_mk 📋 Batteries.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] (a : Array α) (h : a.size = n) (f : ℕ → α → m β) : Vector.mapIdxM f { toArray := a, size_toArray := h } = (fun x => match x with | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$> satisfying ⋯
• Vector.mapFinIdxM_mk 📋 Batteries.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] (a : Array α) (h : a.size = n) (f : (i : ℕ) → α → i < n → m β) : { toArray := a, size_toArray := h }.mapFinIdxM f = (fun x => match x with | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$> satisfying ⋯
• Option.map_coe 📋 Mathlib.Data.Option.Basic
  {α β : Type u_5} {a : α} {f : α → β} : f <$> some a = some (f a)
• Option.map₂_def 📋 Mathlib.Data.Option.NAry
  {α β γ : Type u} (f : α → β → γ) (a : Option α) (b : Option β) : Option.map₂ f a b = f <$> a <*> b
• joinM_map_pure 📋 Mathlib.Control.Basic
  {m : Type u → Type u} [Monad m] [LawfulMonad m] {α : Type u} (a : m α) : joinM (pure <$> a) = a
• joinM_map_joinM 📋 Mathlib.Control.Basic
  {m : Type u → Type u} [Monad m] [LawfulMonad m] {α : Type u} (a : m (m (m α))) : joinM (joinM <$> a) = joinM (joinM a)
• seq_bind_eq 📋 Mathlib.Control.Basic
  {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : m α) {g : β → m γ} {f : α → β} : f <$> x >>= g = x >>= g ∘ f
• joinM_map_map 📋 Mathlib.Control.Basic
  {m : Type u → Type u} [Monad m] [LawfulMonad m] {α β : Type u} (f : α → β) (a : m (m α)) : joinM (Functor.map f <$> a) = f <$> joinM a
• CommApplicative.commutative_map 📋 Mathlib.Control.Basic
  {m : Type u → Type v} [h : Applicative m] [CommApplicative m] {α β γ : Type u} (a : m α) (b : m β) {f : α → β → γ} : f <$> a <*> b = flip f <$> b <*> a
• map_seq 📋 Mathlib.Control.Basic
  {α β γ : Type u} {F : Type u → Type v} [Applicative F] [LawfulApplicative F] (f : β → γ) (x : F (α → β)) (y : F α) : f <$> (x <*> y) = (fun x => f ∘ x) <$> x <*> y
• seq_map_assoc 📋 Mathlib.Control.Basic
  {α β γ : Type u} {F : Type u → Type v} [Applicative F] [LawfulApplicative F] (x : F (α → β)) (f : γ → α) (y : F γ) : x <*> f <$> y = (fun x => x ∘ f) <$> x <*> y
• CommApplicative.commutative_prod 📋 Mathlib.Control.Basic
  {m : Type u → Type v} {inst✝ : Applicative m} [self : CommApplicative m] {α β : Type u} (a : m α) (b : m β) : Prod.mk <$> a <*> b = (fun b a => (a, b)) <$> b <*> a
• CommApplicative.mk 📋 Mathlib.Control.Basic
  {m : Type u → Type v} [Applicative m] [toLawfulApplicative : LawfulApplicative m] (commutative_prod : ∀ {α β : Type u} (a : m α) (b : m β), Prod.mk <$> a <*> b = (fun b a => (a, b)) <$> b <*> a) : CommApplicative m
• Tree.traverse.eq_2 📋 Mathlib.Data.Tree.Basic
  {m : Type u_1 → Type u_2} [Applicative m] {α : Type u_3} {β : Type u_1} (f : α → m β) (a : α) (a_1 a_2 : Tree α) : Tree.traverse f (Tree.node a a_1 a_2) = Tree.node <$> f a <*> Tree.traverse f a_1 <*> Tree.traverse f a_2
• Functor.map_id 📋 Mathlib.Control.Functor
  {F : Type u → Type v} {α : Type u} [Functor F] [LawfulFunctor F] : (fun x => id <$> x) = id
• Functor.ext 📋 Mathlib.Control.Functor
  {F : Type u_1 → Type u_2} {F1 F2 : Functor F} [LawfulFunctor F] [LawfulFunctor F] : (∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x) → F1 = F2
• Functor.Comp.map.eq_1 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] {α β : Type v} (h : α → β) (x✝ : Functor.Comp F G α) : Functor.Comp.map h x✝ = Functor.Comp.mk ((fun x => h <$> x) <$> x✝)
• Functor.map_comp_map 📋 Mathlib.Control.Functor
  {F : Type u → Type v} {α β γ : Type u} [Functor F] [LawfulFunctor F] (f : α → β) (g : β → γ) : ((fun x => g <$> x) ∘ fun x => f <$> x) = fun x => (g ∘ f) <$> x
• Functor.Comp.map_mk 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] {α β : Type v} (h : α → β) (x : F (G α)) : h <$> Functor.Comp.mk x = Functor.Comp.mk ((fun x => h <$> x) <$> x)
• Functor.Comp.run_map 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] {α β : Type v} (h : α → β) (x : Functor.Comp F G α) : (h <$> x).run = (fun x => h <$> x) <$> x.run
• Functor.Comp.run_seq 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] {α β : Type v} (f : Functor.Comp F G (α → β)) (x : Functor.Comp F G α) : (f <*> x).run = (fun x1 x2 => x1 <*> x2) <$> f.run <*> x.run
• List.map_eq_map 📋 Mathlib.Data.List.Basic
  {α β : Type u_2} (f : α → β) (l : List α) : f <$> l = List.map f l
• Set.Finite.map 📋 Mathlib.Data.Set.Finite.Basic
  {α β : Type u_1} {s : Set α} (f : α → β) : s.Finite → (f <$> s).Finite
• Set.fintypeMap 📋 Mathlib.Data.Set.Finite.Basic
  {α β : Type u_1} [DecidableEq β] (s : Set α) (f : α → β) [Fintype ↑s] : Fintype ↑(f <$> s)
• map_eq_bind_pure_comp 📋 Mathlib.Control.Monad.Basic
  {α β : Type u} (m : Type u → Type v) [Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = x >>= pure ∘ f
• Part.map_eq_map 📋 Mathlib.Data.Part
  {α β : Type u_4} (f : α → β) (o : Part α) : f <$> o = Part.map f o
• Part.instAdd.eq_1 📋 Mathlib.Data.Part
  {α : Type u_1} [Add α] : Part.instAdd = { add := fun a b => (fun x1 x2 => x1 + x2) <$> a <*> b }
• Part.instDiv.eq_1 📋 Mathlib.Data.Part
  {α : Type u_1} [Div α] : Part.instDiv = { div := fun a b => (fun x1 x2 => x1 / x2) <$> a <*> b }
• Part.instMul.eq_1 📋 Mathlib.Data.Part
  {α : Type u_1} [Mul α] : Part.instMul = { mul := fun a b => (fun x1 x2 => x1 * x2) <$> a <*> b }
• Part.instSub.eq_1 📋 Mathlib.Data.Part
  {α : Type u_1} [Sub α] : Part.instSub = { sub := fun a b => (fun x1 x2 => x1 - x2) <$> a <*> b }
• OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.map 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type u_6} {f : β → γ} {g : α → Part β} (hg : OmegaCompletePartialOrder.ωScottContinuous g) : OmegaCompletePartialOrder.ωScottContinuous fun x => f <$> g x
• Applicative.pure_seq_eq_map' 📋 Mathlib.Control.Applicative
  {F : Type u → Type v} [Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → β) : (fun x => pure f <*> x) = fun x => f <$> x
• Functor.Comp.map_pure 📋 Mathlib.Control.Applicative
  {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α β : Type v} (f : α → β) (x : α) : f <$> pure x = pure (f x)
• Functor.Comp.pure_seq_eq_map 📋 Mathlib.Control.Applicative
  {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α β : Type v} (f : α → β) (x : Functor.Comp F G α) : pure f <*> x = f <$> x
• Functor.Comp.seq_pure 📋 Mathlib.Control.Applicative
  {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α β : Type v} (f : Functor.Comp F G (α → β)) (x : α) : f <*> pure x = (fun g => g x) <$> f
• Applicative.map_seq_map 📋 Mathlib.Control.Applicative
  {F : Type u → Type v} [Applicative F] [LawfulApplicative F] {α β γ σ : Type u} (f : α → β → γ) (g : σ → β) (x : F α) (y : F σ) : f <$> x <*> g <$> y = ((fun x => x ∘ g) ∘ f) <$> x <*> y
• Comp.seq_mk 📋 Mathlib.Control.Applicative
  {α β : Type w} {f : Type u → Type v} {g : Type w → Type u} [Applicative f] [Applicative g] (h : f (g (α → β))) (x : f (g α)) : Functor.Comp.mk h <*> Functor.Comp.mk x = Functor.Comp.mk ((fun x1 x2 => x1 <*> x2) <$> h <*> x)
• Functor.Comp.seq_assoc 📋 Mathlib.Control.Applicative
  {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α β γ : Type v} (x : Functor.Comp F G α) (f : Functor.Comp F G (α → β)) (g : Functor.Comp F G (β → γ)) : g <*> (f <*> x) = Function.comp <$> g <*> f <*> x
• LawfulTraversable.traverse_eq_map_id 📋 Mathlib.Control.Traversable.Basic
  {t : Type u → Type u} {inst✝ : Traversable t} [self : LawfulTraversable t] {α β : Type u} (f : α → β) (x : t α) : traverse (pure ∘ f) x = id.mk (f <$> x)
• ApplicativeTransformation.preserves_map 📋 Mathlib.Control.Traversable.Basic
  {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) [LawfulApplicative F] [LawfulApplicative G] {α β : Type u} (x : α → β) (y : F α) : (fun {α} => η.app α) (x <$> y) = x <$> (fun {α} => η.app α) y
• ApplicativeTransformation.preserves_map' 📋 Mathlib.Control.Traversable.Basic
  {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) [LawfulApplicative F] [LawfulApplicative G] {α β : Type u} (x : α → β) : (fun {α} => η.app α) ∘ Functor.map x = Functor.map x ∘ fun {α} => η.app α
• LawfulTraversable.comp_traverse 📋 Mathlib.Control.Traversable.Basic
  {t : Type u → Type u} {inst✝ : Traversable t} [self : LawfulTraversable t] {F G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t α) : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
• LawfulTraversable.mk 📋 Mathlib.Control.Traversable.Basic
  {t : Type u → Type u} [Traversable t] [toLawfulFunctor : LawfulFunctor t] (id_traverse : ∀ {α : Type u} (x : t α), traverse pure x = x) (comp_traverse : ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t α), traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)) (traverse_eq_map_id : ∀ {α β : Type u} (f : α → β) (x : t α), traverse (pure ∘ f) x = id.mk (f <$> x)) (naturality : ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : t α), (fun {α} => η.app α) (traverse f x) = traverse ((fun {α} => η.app α) ∘ f) x) : LawfulTraversable t
• List.Vector.traverse_def 📋 Mathlib.Data.Vector.Basic
  {n : ℕ} {F : Type u → Type u} [Applicative F] {α β : Type u} (f : α → F β) (x : α) (xs : List.Vector α n) : List.Vector.traverse f (x ::ᵥ xs) = List.Vector.cons <$> f x <*> List.Vector.traverse f xs
• List.Vector.comp_traverse 📋 Mathlib.Data.Vector.Basic
  {n : ℕ} {F G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : List.Vector α n) : List.Vector.traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (List.Vector.traverse f <$> List.Vector.traverse g x)
• Encodable.decode_list_succ 📋 Mathlib.Logic.Equiv.List
  {α : Type u_1} [Encodable α] (v : ℕ) : Encodable.decode v.succ = (fun x1 x2 => x1 :: x2) <$> Encodable.decode (Nat.unpair v).1 <*> Encodable.decode (Nat.unpair v).2
• Encodable.decodeList.eq_2 📋 Mathlib.Logic.Equiv.List
  {α : Type u_1} [Encodable α] (v : ℕ) : Encodable.decodeList v.succ = match Nat.unpair v, ⋯ with | (v₁, v₂), h => let_fun this := ⋯; (fun x1 x2 => x1 :: x2) <$> Encodable.decode v₁ <*> Encodable.decodeList v₂
• Encodable.decodeList.eq_def 📋 Mathlib.Logic.Equiv.List
  {α : Type u_1} [Encodable α] (x✝ : ℕ) : Encodable.decodeList x✝ = match x✝ with | 0 => some [] | v.succ => match Nat.unpair v, ⋯ with | (v₁, v₂), h => let_fun this := ⋯; (fun x1 x2 => x1 :: x2) <$> Encodable.decode v₁ <*> Encodable.decodeList v₂
• Filter.map_def 📋 Mathlib.Order.Filter.Map
  {α β : Type u_6} (m : α → β) (f : Filter α) : m <$> f = Filter.map m f
• Filter.map_swap_eq_comap_swap 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter (α × β)} : Prod.swap <$> f = Filter.comap Prod.swap f
• CategoryTheory.ofTypeFunctor_map 📋 Mathlib.CategoryTheory.Types
  (m : Type u → Type v) [Functor m] [LawfulFunctor m] {α β : Type u} (f : α → β) : (CategoryTheory.ofTypeFunctor m).map f = Functor.map f
• decodeMultiset.eq_1 📋 Mathlib.Logic.Equiv.Multiset
  {α : Type u_1} [Encodable α] (n : ℕ) : decodeMultiset n = Multiset.ofList <$> Encodable.decode n
• FreeAddGroup.map_zero 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α β : Type u} (f : α → β) : f <$> 0 = 0
• FreeGroup.map_one 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α β : Type u} (f : α → β) : f <$> 1 = 1
• FreeAddGroup.map_pure 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α β : Type u} (f : α → β) (x : α) : f <$> pure x = pure (f x)
• FreeGroup.map_pure 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α β : Type u} (f : α → β) (x : α) : f <$> pure x = pure (f x)
• FreeAddGroup.map_neg 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α β : Type u} (f : α → β) (x : FreeAddGroup α) : f <$> (-x) = -f <$> x
• FreeGroup.map_inv 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α β : Type u} (f : α → β) (x : FreeGroup α) : f <$> x⁻¹ = (f <$> x)⁻¹
• FreeAddGroup.map_add 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α β : Type u} (f : α → β) (x y : FreeAddGroup α) : f <$> (x + y) = f <$> x + f <$> y

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