Monad laws restated via do notation

Lean 4.29 changed do-notation elaboration so that the desugared bind may use a Bind instance that differs syntactically from Monad.toBind. This prevents the standard pure_bind, bind_assoc, and bind_pure lemmas from matching do-block goals via simp or rw.

The lemmas in this file re-derive the laws with their statements written using do notation, so the elaborated Bind instance matches the one produced in proof goals.

@[simp]

theorem LawfulMonad.do_pure_bind {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β : Type u} (a : α) (f : α → m β) : (do let x ← pure a f x) = f a

@[simp]

theorem LawfulMonad.do_bind_pure {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u} (x : m α) : (do let a ← x pure a) = x

@[simp]

theorem LawfulMonad.do_bind_assoc {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ) : (do let b ← do let a ← x f a g b) = do let a ← x let b ← f a g b

@[simp]

theorem LawfulMonad.do_bind_pure_comp {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β : Type u} (f : α → β) (x : m α) : (do let a ← x pure (f a)) = f <$> x

@[simp]

theorem LawfulMonad.do_map_bind {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β γ : Type u} (f : β → γ) (x : m α) (g : α → m β) : (f <$> do let a ← x g a) = do let a ← x f <$> g a

@[simp]

theorem LawfulMonad.do_bind_map_left {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β γ : Type u} (f : α → β) (x : m α) (g : β → m γ) : (do let b ← f <$> x g b) = do let a ← x g (f a)