theorem instMonadLiftTOfMonadLift_instMonadLiftTOfPure {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] {x✝ : MonadLift m n} [LawfulMonadLift m n] : instMonadLiftTOfMonadLift Id m n = Id.instMonadLiftTOfPure

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

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

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

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.

@[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

@[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)

@[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

@[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

@[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

@[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