Odd resolution of goal in natural numbers game

Stream: new members

[Michaël Maex]

I'm a total newbie who's working their way through the natural numbers game.
During an attempt to solve level 4 of the advanced multiplication world I stumbled upon behaviour that struck me as odd and that I would like to understand.

The code looks like this

theorem mul_left_cancel (a b c : mynat) (ha : a ≠ 0) : a * b = a * c → b = c :=
begin
cases a,
exfalso,
apply ha,
refl,
revert b,
induction c with n hn,
intro b,
intro h,
rw mul_zero at h,
rw mul_eq_zero_iff at h,
cc,
intro b,
cases b,
intro hf,
exfalso,
rw mul_zero at hf,
end

After the exfalso the context looks like

2 goals
a : mynat,
ha : succ a ≠ 0,
n : mynat,
hn : ∀ (b : mynat), succ a * b = succ a * n → b = n,
hf : succ a * 0 = succ a * succ n
⊢ false

case mynat.succ
a : mynat,
ha : succ a ≠ 0,
n : mynat,
hn : ∀ (b : mynat), succ a * b = succ a * n → b = n,
b : mynat
⊢ succ a * succ b = succ a * succ n → succ b = succ n

After rw mul_zero at hf, the context suddenly looks like

case mynat.zero
a : mynat,
ha : succ a ≠ 0
⊢ ∀ (b : mynat), succ a * b = succ a * zero → b = zero

Not only did one goal disappear or get resolved in a very non-trivial way. The other goal changed in a way that I find very odd.
Does anyone see what's going on? I'd love to know

[Kevin Buzzard]

lol it's the line 71 column 18 bug in NNG :-) Hit enter a couple of times and sanity will be restored!

[Kevin Buzzard]

https://github.com/leanprover-community/lean/issues/468

[Kevin Buzzard]

This is a super-obscure bug whereby the actual goal is not correctly printed if the cursor is in a couple of extremely specific places. It is unlikely to ever be fixed in Lean 3 because we're moving to Lean 4 (and even if it was fixed in Lean 3 I'm unlikely to port the fix to NNG...)