Natural Number Game \leq World Level 7

Stream: new members

[Tetsuya Ishiu]

I am a little confused in Level 7/11 in \leq World of the Natural Number Game. The instruction says "use `cases h with hx hy'" and it goes through there. But if you try it on Lean 4 Web or a local installation, it returns "Alternative 'inl' has not been provided". What is going on?
I have been using "rcases h with hx | hy" in this situation, and I can adjust. However, I plan to ask my students to try this game and would like to minimize the confusion.

Thank you in advance!

[Kenny Lau]

the syntax changed to cases'

[Kenny Lau]

why would there be confusion if your students use the NNG website?

[Tetsuya Ishiu]

I had to import Mathlib.Tactic.Cases, but cases' worked after that. I think beginners are confused every time what they learned did not work in the real environment. So, I would like to be ready to fill these small differences.

[Kevin Buzzard]

Yes sorry for this, a few tactics behave slightly differently in NNG. Another one is that rw in NNG is like rewrite in Lean as opposed to rw, which also tries rfl after the rewrite (and thus confuses beginners whose goals are randomly closed too early).

[Tetsuya Ishiu]

That is totally fine. It is a great learning tool, and the confusion can be minimized by a little guidance.