m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
⊢ (do
      let a ← x
      pure (id a)) =
    x
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
⊢ x >>= pure = x
show x >>= (fun a => pure (id a)) = x
no goals
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
⊢ (do
      let a ← x
      pure (id a)) =
    x
rw [bind_pure_comp, id_map]