Loogle!

Result

Found 456 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 β
• Option.sequence_some 📋 Init.Data.Option.Basic
  {m : Type u_1 → Type u_2} {α : Type u_1} [Applicative m] (f : m α) : (some f).sequence = some <$> f
• Option.mapM_some 📋 Init.Data.Option.Basic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative m] (x : α) (f : α → m β) : Option.mapM f (some x) = some <$> f x
• 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
• Id.run_map 📋 Init.Control.Lawful.Basic
  {α β : Type u_1} (x : Id α) (f : α → β) : (f <$> x).run = f x.run
• 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
• liftM_map 📋 Init.Control.Lawful.MonadLift.Lemmas
  {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α) : liftM (f <$> ma) = f <$> liftM ma
• monadLift_map 📋 Init.Control.Lawful.MonadLift.Lemmas
  {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α) : monadLift (f <$> ma) = f <$> monadLift ma
• 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.idRun_forIn_yield_eq_foldl 📋 Init.Data.List.Monadic
  {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β → Id β) (init : β) : (forIn l init fun a b => ForInStep.yield <$> f a b).run = List.foldl (fun b a => (f a b).run) init l
• 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.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 => (fun x => x :: acc) <$> f a) [] 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.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 => (fun x => x :: acc) <$> f a) (b :: bs) as = (fun x => x ++ b :: bs) <$> List.foldlM (fun acc a => (fun x => x :: acc) <$> f a) [] as
• List.idRun_forIn'_yield_eq_foldl 📋 Init.Data.List.Monadic
  {α : Type u_1} {β : Type u_2} (l : List α) (f : (a : α) → a ∈ l → β → Id β) (init : β) : (forIn' l init fun a m b => ForInStep.yield <$> f a m b).run = List.foldl (fun b x => match x with | ⟨a, h⟩ => (f a h b).run) init l.attach
• 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
• List.foldlM_push_eq_append 📋 Init.Data.Array.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} : List.foldlM (fun xs x => xs.push <$> f x) xs l = do let __do_lift ← List.mapM f l pure (xs ++ __do_lift.toArray)
• List.foldrM_push_eq_append 📋 Init.Data.Array.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} : List.foldrM (fun x xs => xs.push <$> f x) xs l = do let __do_lift ← List.mapM f l.reverse pure (xs ++ __do_lift.toArray)
• 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
• Array.map_toList_inj 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {xs ys : m (Array α)} : Array.toList <$> xs = Array.toList <$> ys ↔ xs = ys
• 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.idRun_forIn_yield_eq_foldl 📋 Init.Data.Array.Monadic
  {α : Type u_1} {β : Type u_2} {xs : Array α} (f : α → β → Id β) (init : β) : (forIn xs init fun a b => ForInStep.yield <$> f a b).run = Array.foldl (fun b a => (f a b).run) init xs
• 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.idRun_forIn'_yield_eq_foldl 📋 Init.Data.Array.Monadic
  {α : Type u_1} {β : Type u_2} {xs : Array α} (f : (a : α) → a ∈ xs → β → Id β) (init : β) : (forIn' xs init fun a m b => ForInStep.yield <$> f a m b).run = Array.foldl (fun b x => match x with | ⟨a, h⟩ => (f a h b).run) init xs.attach
• 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
• Array.toList_ofFnM 📋 Init.Data.Array.OfFn
  {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin n → m α} : Array.toList <$> Array.ofFnM f = List.ofFnM f
• 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
• Option.filterM_some 📋 Init.Data.Option.Monadic
  {m : Type → Type u_1} {α : Type} [Applicative m] (p : α → m Bool) (a : α) : Option.filterM p (some a) = (fun b => if b = true then some a else none) <$> p a
• Option.sequence_join 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_1} [Applicative m] [LawfulApplicative m] {o : Option (Option (m α))} : o.join.sequence = Option.join <$> (Option.map Option.sequence o).sequence
• Option.mapM_join 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative m] [LawfulApplicative m] {f : α → m β} {o : Option (Option α)} : Option.mapM f o.join = Option.join <$> Option.mapM (Option.mapM f) o
• Option.elimM_map 📋 Init.Data.Option.Monadic
  {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
• Option.mapM_guard 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative m] {x : α} {p : α → Bool} {f : α → m β} : Option.mapM f (Option.guard p x) = if p x = true then some <$> f x else pure none
• Option.idRun_forIn_yield_eq_elim 📋 Init.Data.Option.Monadic
  {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → β → Id β) (b : β) : (forIn o b fun a b => ForInStep.yield <$> f a b).run = o.elim b fun a => (f a b).run
• 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.idRun_forIn'_yield_eq_pelim 📋 Init.Data.Option.Monadic
  {α : Type u_1} {β : Type u_2} (o : Option α) (f : (a : α) → a ∈ o → β → Id β) (b : β) : (forIn' o b fun a m b => ForInStep.yield <$> f a m b).run = o.pelim b fun a h => (f a h b).run
• 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_join 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [Monad m] [LawfulMonad m] (o : Option (Option α)) (f : α → β → m (ForInStep β)) : forIn o.join init f = forIn o init fun o' b => ForInStep.yield <$> forIn o' b f
• 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
• Option.forIn'_join 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] [LawfulMonad m] (b : β) (o : Option (Option α)) (f : (a : α) → a ∈ o.join → β → m (ForInStep β)) : forIn' o.join b f = forIn' o b fun o' ho' b => ForInStep.yield <$> forIn' o' b fun a ha b' => f a ⋯ 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.toArray.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.idRun_forIn_yield_eq_foldl 📋 Init.Data.Vector.Monadic
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} (f : α → β → Id β) (init : β) : (forIn xs init fun a b => ForInStep.yield <$> f a b).run = Vector.foldl (fun b a => (f a b).run) init xs
• 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.idRun_forIn'_yield_eq_foldl 📋 Init.Data.Vector.Monadic
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} (f : (a : α) → a ∈ xs → β → Id β) (init : β) : (forIn' xs init fun a m b => ForInStep.yield <$> f a m b).run = Vector.foldl (fun b x => match x with | ⟨a, h⟩ => (f a h b).run) init xs.attach
• 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
• Vector.toArray_ofFnM 📋 Init.Data.Vector.OfFn
  {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin n → m α} : Vector.toArray <$> Vector.ofFnM f = Array.ofFnM f
• Vector.toList_ofFnM 📋 Init.Data.Vector.OfFn
  {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin n → m α} : Vector.toList <$> Vector.ofFnM f = List.ofFnM f
• Std.Iterators.PostconditionT.operation_lift 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Functor m] {α : Type w} {x : m α} : (Std.Iterators.PostconditionT.lift x).operation = (fun x_1 => ⟨x_1, ⋯⟩) <$> x
• Std.Iterators.PostconditionT.ext 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type w} {x y : Std.Iterators.PostconditionT m α} (h : x.Property = y.Property) (h' : (fun p => ⟨↑p, ⋯⟩) <$> x.operation = y.operation) : x = y
• Std.Iterators.PostconditionT.ext_iff 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type w} {x y : Std.Iterators.PostconditionT m α} : x = y ↔ ∃ (h : x.Property = y.Property), (fun p => ⟨↑p, ⋯⟩) <$> x.operation = y.operation
• Std.Iterators.PostconditionT.map.eq_1 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Functor m] {α β : Type w} (f : α → β) (x : Std.Iterators.PostconditionT m α) : Std.Iterators.PostconditionT.map f x = { Property := fun b => ∃ a, f ↑a = b, operation := (fun a => ⟨f ↑a, ⋯⟩) <$> x.operation }
• Std.Iterators.PostconditionT.operation_map 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Functor m] {α β : Type w} {x : Std.Iterators.PostconditionT m α} {f : α → β} : (Std.Iterators.PostconditionT.map f x).operation = (fun a => ⟨f ↑a, ⋯⟩) <$> x.operation
• Std.Internal.LawfulMonadLiftFunction.lift_map 📋 Init.Data.Iterators.Internal.LawfulMonadLiftFunction
  {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {lift : ⦃α : Type u⦄ → m α → n α} {α β : Type u} [LawfulMonad m] [LawfulMonad n] [Std.Internal.LawfulMonadLiftFunction lift] (f : α → β) (ma : m α) : lift (f <$> ma) = f <$> lift ma
• Std.Iterators.IterM.mapM 📋 Init.Data.Iterators.Combinators.Monadic.FilterMap
  {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Std.Iterators.Iterator α m β] [Monad n] [MonadLiftT m n] (f : β → n γ) (it : Std.IterM m β) : Std.IterM n γ
• Std.Iterators.ULiftT.run_map 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {n : Type (max u v) → Type v'} [Monad n] {α β : Type u} {x : Std.Iterators.ULiftT n α} {f : α → β} : (f <$> x).run = do let a ← x.run pure { down := f a.down }
• Std.Iterators.Iter.mapM 📋 Init.Data.Iterators.Combinators.FilterMap
  {α β γ : Type w} [Std.Iterators.Iterator α Id β] {m : Type w → Type w'} [Monad m] (f : β → m γ) (it : Std.Iter β) : Std.IterM m γ
• Std.Iterators.IterM.toList_toArray 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
  {α β : Type w} {m : Type w → Type w'} [Monad m] [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] {it : Std.IterM m β} : Array.toList <$> it.toArray = it.toList
• Std.Iterators.IterM.toArray_toList 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
  {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] {it : Std.IterM m β} : List.toArray <$> it.toList = it.toArray
• Std.Iterators.IterM.reverse_toListRev 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
  {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] {it : Std.IterM m β} : List.reverse <$> it.toListRev = it.toList
• Std.Iterators.IterM.toListRev_eq 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
  {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] {it : Std.IterM m β} : it.toListRev = List.reverse <$> it.toList
• Std.Iterators.IterM.toListRev.go.aux₂ 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
  {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] {it : Std.IterM m β} {acc : List β} : Std.Iterators.IterM.toListRev.go it acc = (fun x => x ++ acc) <$> it.toListRev
• Std.Iterators.IterM.DefaultConsumers.toArrayMapped.go.aux₂ 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
  {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃δ : Type w⦄ → m δ → n δ} {f : β → n γ} {it : Std.IterM m β} [Monad n] [LawfulMonad n] [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] {acc : Array γ} : Std.Iterators.IterM.DefaultConsumers.toArrayMapped.go lift f it acc = (fun x => acc ++ x) <$> Std.Iterators.IterM.DefaultConsumers.toArrayMapped lift f it
• Std.Iterators.IterM.toListRev.go.aux₁ 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
  {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] {it : Std.IterM m β} {b : β} {bs : List β} : Std.Iterators.IterM.toListRev.go it (bs ++ [b]) = (fun x => x ++ [b]) <$> Std.Iterators.IterM.toListRev.go it bs
• Std.Iterators.IterM.DefaultConsumers.toArrayMapped.go.aux₁ 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
  {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃δ : Type w⦄ → m δ → n δ} {f : β → n γ} {it : Std.IterM m β} [Monad n] [LawfulMonad n] [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] {b : γ} {bs : Array γ} : Std.Iterators.IterM.DefaultConsumers.toArrayMapped.go lift f it (#[b] ++ bs) = (fun x => #[b] ++ x) <$> Std.Iterators.IterM.DefaultConsumers.toArrayMapped.go lift f it bs
• Std.Iterators.IterM.drain_eq_map_toListRev 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
  {α β : Type w} {m : Type w → Type w'} [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Monad m] [LawfulMonad m] [Std.Iterators.IteratorLoop α m m] [Std.Iterators.LawfulIteratorLoop α m m] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] {it : Std.IterM m β} : it.drain = (fun x => PUnit.unit) <$> it.toListRev
• Std.Iterators.IterM.drain_eq_map_toArray 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
  {α β : Type w} {m : Type w → Type w'} [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Monad m] [LawfulMonad m] [Std.Iterators.IteratorLoop α m m] [Std.Iterators.LawfulIteratorLoop α m m] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] {it : Std.IterM m β} : it.drain = (fun x => PUnit.unit) <$> it.toList
• Std.Iterators.IterM.drain_eq_map_toList 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
  {α β : Type w} {m : Type w → Type w'} [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Monad m] [LawfulMonad m] [Std.Iterators.IteratorLoop α m m] [Std.Iterators.LawfulIteratorLoop α m m] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] {it : Std.IterM m β} : it.drain = (fun x => PUnit.unit) <$> it.toList
• Std.Iterators.IterM.foldM_eq_forIn 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
  {α β γ : Type w} {m : Type w → Type w'} [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''} [Monad n] [Std.Iterators.IteratorLoop α m n] [MonadLiftT m n] {f : γ → β → n γ} {init : γ} {it : Std.IterM m β} : Std.Iterators.IterM.foldM f init it = forIn it init fun x acc => ForInStep.yield <$> f acc x
• Std.Iterators.IterM.forIn_yield_eq_foldM 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
  {α β γ δ : Type w} {m : Type w → Type w'} [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] [Std.Iterators.IteratorLoop α m n] [Std.Iterators.LawfulIteratorLoop α m n] [MonadLiftT m n] {f : β → γ → n δ} {g : β → γ → δ → γ} {init : γ} {it : Std.IterM m β} : (forIn it init fun c b => (fun d => ForInStep.yield (g c b d)) <$> f c b) = Std.Iterators.IterM.foldM (fun b c => g c b <$> f c b) init it
• Std.Iterators.IterM.forIn_eq 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
  {α β : Type w} {m : Type w → Type w'} [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''} [Monad n] [Std.Iterators.IteratorLoop α m n] [hl : Std.Iterators.LawfulIteratorLoop α m n] [MonadLiftT m n] {γ : Type w} {it : Std.IterM m β} {init : γ} {f : β → γ → n (ForInStep γ)} : forIn it init f = Std.Iterators.IterM.DefaultConsumers.forIn' (fun x => monadLift) γ (fun x x x => True) ⋯ it init it.IsPlausibleIndirectOutput ⋯ fun out x acc => (fun x => ⟨x, True.intro⟩) <$> f out acc
• Std.Iterators.IterM.forIn'_eq 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
  {α β : Type w} {m : Type w → Type w'} [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''} [Monad n] [Std.Iterators.IteratorLoop α m n] [hl : Std.Iterators.LawfulIteratorLoop α m n] [MonadLiftT m n] {γ : Type w} {it : Std.IterM m β} {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)} : forIn' it init f = Std.Iterators.IterM.DefaultConsumers.forIn' (fun x => monadLift) γ (fun x x x => True) ⋯ it init it.IsPlausibleIndirectOutput ⋯ fun x1 x2 x3 => (fun x => ⟨x, True.intro⟩) <$> f x1 x2 x3
• Std.Iterators.Iter.foldM_eq_forIn 📋 Init.Data.Iterators.Lemmas.Consumers.Loop
  {α β γ : Type w} [Std.Iterators.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type w → Type w'} [Monad m] [Std.Iterators.IteratorLoop α Id m] {f : γ → β → m γ} {init : γ} {it : Std.Iter β} : Std.Iterators.Iter.foldM f init it = forIn it init fun x acc => ForInStep.yield <$> f acc x
• Std.Iterators.Iter.forIn_yield_eq_foldM 📋 Init.Data.Iterators.Lemmas.Consumers.Loop
  {α β γ δ : Type w} [Std.Iterators.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [Std.Iterators.IteratorLoop α Id m] [Std.Iterators.LawfulIteratorLoop α Id m] {f : β → γ → m δ} {g : β → γ → δ → γ} {init : γ} {it : Std.Iter β} : (forIn it init fun c b => (fun d => ForInStep.yield (g c b d)) <$> f c b) = Std.Iterators.Iter.foldM (fun b c => g c b <$> f c b) init it
• Std.Iterators.IterM.forIn_eq_foldM 📋 Init.Data.Iterators.Lemmas.Consumers.Loop
  {α β : Type w} [Std.Iterators.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [Std.Iterators.IteratorLoop α Id m] [Std.Iterators.LawfulIteratorLoop α Id m] [Std.Iterators.IteratorCollect α Id Id] [Std.Iterators.LawfulIteratorCollect α Id Id] {γ : Type w} {it : Std.Iter β} {init : γ} {f : β → γ → m (ForInStep γ)} : forIn it init f = ForInStep.value <$> Std.Iterators.Iter.foldM (fun c b => match c with | ForInStep.yield c => f b c | ForInStep.done c => pure (ForInStep.done c)) (ForInStep.yield init) it
• Std.Iterators.Iter.forIn_eq 📋 Init.Data.Iterators.Lemmas.Consumers.Loop
  {α β : Type w} [Std.Iterators.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type w → Type w''} [Monad m] [Std.Iterators.IteratorLoop α Id m] [hl : Std.Iterators.LawfulIteratorLoop α Id m] {γ : Type w} {it : Std.Iter β} {init : γ} {f : β → γ → m (ForInStep γ)} : forIn it init f = Std.Iterators.IterM.DefaultConsumers.forIn' (fun x c => pure c.run) γ (fun x x x => True) ⋯ it.toIterM init it.toIterM.IsPlausibleIndirectOutput ⋯ fun out x acc => (fun x => ⟨x, True.intro⟩) <$> f out acc
• Std.Iterators.Iter.forIn'_eq 📋 Init.Data.Iterators.Lemmas.Consumers.Loop
  {α β : Type w} [Std.Iterators.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type w → Type w''} [Monad m] [Std.Iterators.IteratorLoop α Id m] [hl : Std.Iterators.LawfulIteratorLoop α Id m] {γ : Type w} {it : Std.Iter β} {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → m (ForInStep γ)} : forIn' it init f = Std.Iterators.IterM.DefaultConsumers.forIn' (fun x c => pure c.run) γ (fun x x x => True) ⋯ it.toIterM init it.toIterM.IsPlausibleIndirectOutput ⋯ fun out h acc => (fun x => ⟨x, True.intro⟩) <$> f out ⋯ acc
• Std.Iterators.IterM.map_unattach_toListRev_attachWith 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
  {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} {n : Type u_1 → Type u_2} [Std.Iterators.Iterator α m β] [Monad m] [Monad n] {it : Std.IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [LawfulMonad m] [Std.Iterators.LawfulIteratorCollect α m m] : List.unattach <$> (it.attachWith P hP).toListRev = it.toListRev
• Std.Iterators.IterM.map_unattach_toList_attachWith 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
  {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} [Std.Iterators.Iterator α m β] [Monad m] {it : Std.IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [LawfulMonad m] [Std.Iterators.LawfulIteratorCollect α m m] : List.unattach <$> (it.attachWith P hP).toList = it.toList
• Std.Iterators.IterM.map_unattach_toArray_attachWith 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
  {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} {n : Type u_1 → Type u_2} [Std.Iterators.Iterator α m β] [Monad m] [Monad n] {it : Std.IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [LawfulMonad m] [Std.Iterators.LawfulIteratorCollect α m m] : (fun x => Array.map Subtype.val x) <$> (it.attachWith P hP).toArray = it.toArray
• Std.Iterators.IterM.step_attachWith 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
  {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} [Std.Iterators.Iterator α m β] [Monad m] {it : Std.IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} : (it.attachWith P hP).step = (fun s => ⟨Std.Iterators.Types.Attach.Monadic.modifyStep (it.attachWith P hP) s, ⋯⟩) <$> it.step
• Std.Iterators.PostconditionT.lift.eq_1 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α : Type w} {m : Type w → Type w'} [Functor m] (x : m α) : Std.Iterators.PostconditionT.lift x = { Property := fun x => True, operation := (fun x => ⟨x, True.intro⟩) <$> x }
• Std.Iterators.IterM.toListRev_filterMap 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] [Std.Iterators.Finite α m] {f : β → Option γ} (it : Std.IterM m β) : (Std.Iterators.IterM.filterMap f it).toListRev = (fun x => List.filterMap f x) <$> it.toListRev
• Std.Iterators.IterM.toListRev_map 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] [Std.Iterators.Finite α m] {f : β → γ} (it : Std.IterM m β) : (Std.Iterators.IterM.map f it).toListRev = (fun x => List.map f x) <$> it.toListRev
• Std.Iterators.IterM.toList_filterMap 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] [Std.Iterators.Finite α m] {f : β → Option γ} (it : Std.IterM m β) : (Std.Iterators.IterM.filterMap f it).toList = (fun x => List.filterMap f x) <$> it.toList
• Std.Iterators.IterM.InternalConsumers.toList_filterMap 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] [Std.Iterators.Finite α m] {f : β → Option γ} (it : Std.IterM m β) : (Std.Iterators.IterM.filterMap f it).toList = (fun x => List.filterMap f x) <$> it.toList
• Std.Iterators.IterM.toArray_map 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] [Std.Iterators.Finite α m] {f : β → γ} (it : Std.IterM m β) : (Std.Iterators.IterM.map f it).toArray = (fun x => Array.map f x) <$> it.toArray
• Std.Iterators.IterM.toList_map 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α β β' : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] [Std.Iterators.Finite α m] {f : β → β'} (it : Std.IterM m β) : (Std.Iterators.IterM.map f it).toList = (fun x => List.map f x) <$> it.toList
• Std.Iterators.IterM.toListRev_filter 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] {f : β → Bool} {it : Std.IterM m β} : (Std.Iterators.IterM.filter f it).toListRev = List.filter f <$> it.toListRev
• Std.Iterators.IterM.toArray_filterMap 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α m β] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] [Std.Iterators.Finite α m] {f : β → Option γ} (it : Std.IterM m β) : (Std.Iterators.IterM.filterMap f it).toArray = (fun x => Array.filterMap f x) <$> it.toArray
• Std.Iterators.IterM.toList_filter 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β : Type w} [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] {f : β → Bool} {it : Std.IterM m β} : (Std.Iterators.IterM.filter f it).toList = List.filter f <$> it.toList
• Std.Iterators.IterM.toArray_filter 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β : Type w} [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [Std.Iterators.LawfulIteratorCollect α m m] {f : β → Bool} {it : Std.IterM m β} : (Std.Iterators.IterM.filter f it).toArray = (fun as => Array.filter f as) <$> it.toArray
• Std.Iterators.IterM.step_mapM 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Std.Iterators.Iterator α m β] {it : Std.IterM m β} {γ : Type w} {f : β → n γ} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (Std.Iterators.IterM.mapM f it).step = do let __do_lift ← liftM it.step match __do_lift with | ⟨Std.Iterators.IterStep.yield it' out, h⟩ => do let out' ← f out pure (Std.Iterators.PlausibleIterStep.yield (Std.Iterators.IterM.mapM f it') out' ⋯) | ⟨Std.Iterators.IterStep.skip it', h⟩ => pure (Std.Iterators.PlausibleIterStep.skip (Std.Iterators.IterM.mapM f it') ⋯) | ⟨Std.Iterators.IterStep.done, h⟩ => pure (Std.Iterators.PlausibleIterStep.done ⋯)
• Std.Iterators.IterM.toListRev_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Std.Iterators.Iterator α m β] [Monad m] [Monad n] {it : Std.IterM m β} [MonadLiftT m (Std.Iterators.ULiftT n)] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [LawfulMonad m] [LawfulMonad n] [Std.Iterators.LawfulIteratorCollect α m m] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)] : (it.uLift n).toListRev = (fun l => List.map ULift.up l.down) <$> (monadLift it.toListRev).run
• Std.Iterators.IterM.toArray_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Std.Iterators.Iterator α m β] [Monad m] [Monad n] {it : Std.IterM m β} [MonadLiftT m (Std.Iterators.ULiftT n)] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [LawfulMonad m] [LawfulMonad n] [Std.Iterators.LawfulIteratorCollect α m m] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)] : (it.uLift n).toArray = (fun l => Array.map ULift.up l.down) <$> (monadLift it.toArray).run
• Std.Iterators.IterM.toList_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Std.Iterators.Iterator α m β] [Monad m] [Monad n] {it : Std.IterM m β} [MonadLiftT m (Std.Iterators.ULiftT n)] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [LawfulMonad m] [LawfulMonad n] [Std.Iterators.LawfulIteratorCollect α m m] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)] : (it.uLift n).toList = (fun l => List.map ULift.up l.down) <$> (monadLift it.toList).run
• Std.Iterators.Iter.mapM_eq_toIter_mapM_toIterM 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β γ : Type w} [Std.Iterators.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [Monad m] {f : β → m γ} : Std.Iterators.Iter.mapM f it = Std.Iterators.IterM.mapM f it.toIterM
• Std.Iterators.Iter.step_mapM 📋 Init.Data.Iterators.Lemmas.Combinators.FilterMap
  {α β γ : Type w} [Std.Iterators.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {f : β → n γ} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (Std.Iterators.Iter.mapM f it).step = match it.step with | ⟨Std.Iterators.IterStep.yield it' out, h⟩ => do let out' ← f out pure (Std.Iterators.PlausibleIterStep.yield (Std.Iterators.Iter.mapM f it') out' ⋯) | ⟨Std.Iterators.IterStep.skip it', h⟩ => pure (Std.Iterators.PlausibleIterStep.skip (Std.Iterators.Iter.mapM f it') ⋯) | ⟨Std.Iterators.IterStep.done, h⟩ => pure (Std.Iterators.PlausibleIterStep.done ⋯)
• 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
• Std.Iterators.HetT.ofPostconditionT.eq_1 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : Std.Iterators.PostconditionT m α) : Std.Iterators.HetT.ofPostconditionT x = { Property := x.Property, small := ⋯, operation := Std.Internal.USquash.deflate <$> x.operation }
• Std.Iterators.HetT.pmap.eq_1 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} (x : Std.Iterators.HetT m α) (f : (a : α) → x.Property a → β) : x.pmap f = { Property := fun b => ∃ a, ∃ (h : x.Property a), f a h = b, small := ⋯, operation := (fun a => Std.Internal.USquash.deflate ⟨f ↑a.inflate ⋯, ⋯⟩) <$> x.operation }
• Std.Iterators.HetT.bind.eq_1 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {m : Type w → Type w'} [Monad m] {α : Type u} {β : Type v} (x : Std.Iterators.HetT m α) (f : α → Std.Iterators.HetT m β) : x.bind f = { Property := fun b => ∃ a, x.Property a ∧ (f a).Property b, small := ⋯, operation := do let a ← x.operation (fun b => Std.Internal.USquash.deflate ⟨↑b.inflate, ⋯⟩) <$> (f ↑a.inflate).operation }
• Std.Iterators.HetT.pbind.eq_1 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {m : Type w → Type w'} [Monad m] {α : Type u} {β : Type v} (x : Std.Iterators.HetT m α) (f : (a : α) → x.Property a → Std.Iterators.HetT m β) : x.pbind f = { Property := fun b => ∃ a, ∃ (h : x.Property a), (f a h).Property b, small := ⋯, operation := do let a ← x.operation (fun b => Std.Internal.USquash.deflate ⟨↑b.inflate, ⋯⟩) <$> (f ↑a.inflate ⋯).operation }
• Std.Iterators.BundledIterM.stepOnQuotient_mk 📋 Std.Data.Iterators.Lemmas.Equivalence.Basic
  {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β : Type w} [Monad m] [LawfulMonad m] {bit : Std.Iterators.BundledIterM m β} : Std.Iterators.BundledIterM.stepOnQuotient (Quot.mk (Std.Iterators.BundledIterM.Equiv m β) bit) = Std.Iterators.IterStep.mapIterator (Quot.mk (Std.Iterators.BundledIterM.Equiv m β)) <$> bit.step
• Std.Iterators.IterM.Equiv.of_morphism 📋 Std.Data.Iterators.Lemmas.Equivalence.Basic
  {α₁ α₂ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β : Type w} [Std.Iterators.Iterator α₁ m β] [Std.Iterators.Iterator α₂ m β] (ita : Std.IterM m β) (f : Std.IterM m β → Std.IterM m β) (h : ∀ (it : Std.IterM m β), (f it).stepAsHetT = Std.Iterators.IterStep.mapIterator f <$> it.stepAsHetT) : ita.Equiv (f ita)
• Std.Iterators.IterM.stepAsHetT.eq_1 📋 Std.Data.Iterators.Lemmas.Equivalence.Basic
  {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Std.Iterators.Iterator α m β] [Monad m] (it : Std.IterM m β) : it.stepAsHetT = { Property := it.IsPlausibleStep, small := ⋯, operation := (fun step => Std.Internal.USquash.deflate step) <$> it.step }
• Std.Iterators.IterM.Equiv.step_eq 📋 Std.Data.Iterators.Lemmas.Equivalence.StepCongr
  {β α₁ α₂ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Std.Iterators.Iterator α₁ m β] [Std.Iterators.Iterator α₂ m β] {ita : Std.IterM m β} {itb : Std.IterM m β} (h : ita.Equiv itb) : (Quot.mk fun s₁ s₂ => (↑s₁).bundledQuotient = (↑s₂).bundledQuotient) <$> ita.step = Std.Iterators.IterM.QuotStep.transportAlongEquiv ⋯ <$> (Quot.mk fun s₁ s₂ => (↑s₁).bundledQuotient = (↑s₂).bundledQuotient) <$> itb.step
• Std.Iterators.IterM.Equiv.mapM 📋 Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Std.Iterators.Iterator α₁ m β] [Std.Iterators.Iterator α₂ m β] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n γ} {ita : Std.IterM m β} {itb : Std.IterM m β} (h : ita.Equiv itb) : (Std.Iterators.IterM.mapM f ita).Equiv (Std.Iterators.IterM.mapM f itb)
• Std.Iterators.Iter.Intermediate.zip.eq_1 📋 Std.Data.Iterators.Lemmas.Combinators.Zip
  {α₁ α₂ β₁ β₂ : Type w} [Std.Iterators.Iterator α₁ Id β₁] (it₁ : Std.Iter β₁) (memo : Option { out // ∃ it, it.toIterM.IsPlausibleOutput out }) (it₂ : Std.Iter β₂) : Std.Iterators.Iter.Intermediate.zip it₁ memo it₂ = (Std.Iterators.IterM.Intermediate.zip it₁.toIterM ((fun x => ⟨↑x, ⋯⟩) <$> memo) it₂.toIterM).toIter
• Std.Iterators.ListIterator.toArrayMapped_iterM 📋 Std.Data.Iterators.Lemmas.Producers.Monadic.List
  {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] {β γ : Type w} {lift : ⦃δ : Type w⦄ → m δ → n δ} [Std.Internal.LawfulMonadLiftFunction lift] {f : β → n γ} {l : List β} : Std.Iterators.IteratorCollect.toArrayMapped lift f (l.iterM m) = List.toArray <$> List.mapM f l
• Std.Iterators.Iter.atIdxSlow?_succ_repeat_eq_map 📋 Std.Data.Iterators.Lemmas.Producers.Repeat
  {α : Type w} {f : α → α} {init : α} {k : ℕ} : Std.Iterators.Iter.atIdxSlow? (k + 1) (Std.Iterators.Iter.repeat f init) = f <$> Std.Iterators.Iter.atIdxSlow? k (Std.Iterators.Iter.repeat f init)
• Std.Do.PredTrans.map_apply 📋 Std.Do.PredTrans
  {ps : Std.Do.PostShape} {α β : Type} (f : α → β) (x : Std.Do.PredTrans ps α) (Q : Std.Do.PostCond β ps) : (f <$> x).apply Q = x.apply (fun a => Q.1 (f a), Q.2)
• Std.Do.WPMonad.wp_map 📋 Std.Do.WP.Monad
  {m : Type → Type u} {ps : Std.Do.PostShape} {α β : Type} [Monad m] [Std.Do.WPMonad m ps] (f : α → β) (x : m α) : Std.Do.wp (f <$> x) = f <$> Std.Do.wp x
• Std.Do.WP.map 📋 Std.Do.WP.SimpLemmas
  {m : Type → Type u} {ps : Std.Do.PostShape} {α β : Type} [Monad m] [Std.Do.WPMonad m ps] (f : α → β) (x : m α) (Q : Std.Do.PostCond β ps) : (Std.Do.wp (f <$> x)).apply Q = (Std.Do.wp x).apply (fun a => Q.1 (f a), Q.2)
• Std.Do.Spec.map 📋 Std.Do.Triple.SpecLemmas
  {m : Type → Type u} {ps : Std.Do.PostShape} [Monad m] [Std.Do.WPMonad m ps] {α β : Type} {x : m α} {f : α → β} {Q : Std.Do.PostCond β ps} : ⦃(Std.Do.wp x).apply (fun a => Q.1 (f a), Q.2)⦄ (f <$> x) ⦃Q⦄
• EStateM.run_map 📋 Batteries.Lean.EStateM
  {α β ε σ : Type u_1} {s : σ} (f : α → β) (x : EStateM ε σ α) : (f <$> x).run s = EStateM.Result.map f (x.run s)

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 2c2d6a2 serving mathlib revision 288ffbb