issue with case and let tactics

[cipher1024]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

This code fails:

example (n m : ℕ) : n + m = m + n :=
begin
let s := n + m,
induction n,
case nat.zero : {sorry}, -- error: could not find open goal of given case
case nat.succ : {sorry}
end

While this code succeeds:

example (n m : ℕ) : n + m = m + n :=
begin
-- let s := n + m,
induction n,
case nat.zero : {sorry}, -- error: could not find open goal of given case
case nat.succ : {sorry}
end

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.