source
theorem monadLift_map {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
source
theorem monadLift_seq {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] (mf : m (α → β)) (ma : m α) :
monadLift (mf <*> ma) = monadLift mf <*> monadLift ma
source
theorem monadLift_seqLeft {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] (x : m α) (y : m β) :
monadLift (x <* y) = monadLift x <* monadLift y
source
theorem monadLift_seqRight {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] (x : m α) (y : m β) :
monadLift (x *> y) = monadLift x *> monadLift y

We duplicate the theorems for `monadLift` to `liftM` since `rw` matches on syntax only.

source
@[simp]
theorem liftM_pure {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α : Type u} (a : α) :
liftM (pure a) = pure a
source
@[simp]
theorem liftM_bind {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u} (ma : m α) (f : α → m β) :
liftM (ma >>= f) = do let a ← liftM ma liftM (f a)
source
@[simp]
theorem liftM_map {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
source
@[simp]
theorem liftM_seq {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] (mf : m (α → β)) (ma : m α) :
liftM (mf <*> ma) = liftM mf <*> liftM ma
source
@[simp]
theorem liftM_seqLeft {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] (x : m α) (y : m β) :
liftM (x <* y) = liftM x <* liftM y
source
@[simp]
theorem liftM_seqRight {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] (x : m α) (y : m β) :
liftM (x *> y) = liftM x *> liftM y