Strange issue in Natural Numbers game

Stream: new members

[Nilesh]

I'm unable to complete this goal on Level 6 / 10 : mul_right_eq_one:

image.png

[Nilesh]

Looks like something has broken. The goal just doesn't get completed:
image.png

[Nilesh]

The full code is:

theorem mul_right_eq_one (x y : ℕ) (h : x * y = 1) : x = 1 := by
have h2 : x * y ≠ 0
rw [h]
exact one_ne_zero
apply le_mul_right at h2
rw [h] at h2
apply le_one at h2
cases h2 with h0 h1
· rw [h0, zero_mul] at h
rw [h1]
rfl

[Nilesh]

But this worked:

have h2 : x * y ≠ 0
rw [h]
exact one_ne_zero
apply le_mul_right at h2
rw [h] at h2
apply le_one at h2
cases h2 with h0 h1
rw [h0, zero_mul] at h
tauto
exact h1

[Kevin Buzzard]

In the screenshot: You had two goals, you solved one, now you have one goal.

[Nilesh]

No, I think it had something to do with beginning my line with a · after the case.

[Kevin Buzzard]

Oh yes! Yes, I'm sure we're not bargaining for that, NNG doesn't teach anything about grouping, the point of the infrastructure is so that you don't have to know about the dots.