Idiomatic Lean for "Do Nothing"

Stream: lean4

[Mac]

When performing a match inside a do block, sometimes I just want the match to do nothing. Currently I am using pure (), but is their a better idiomatic solution? For example of when this is necessary: The fall through case (i.e., _), throws an error, other cases perform a action, but the do nothing case exists because I neither want it to perform an action or error.

[Mario Carneiro]

you might be able to use just ()

[Mario Carneiro]

lean does auto lifting into the monad in some cases, I'm not sure about what the extent is