Issue with NNG Multiplication World Level 1?

Stream: new members

[ZainAK283]

I'm playing the Natural Number Game Multiplication world, level 1, and this seems to solve it:

induction m with d hd,
rwa mul_zero,

Though it shouldn't, right?

[Chris Hughes]

This behaviour surprised me as well.
rw mul_zero closes the first goal. Kevin adjusted the rw tactic in the game so you would have to write refl after rewriting to close the goal, but usually rw automatically tries refl, and rwa was not modified by the game.

the second goal is closed by assumption. to see why note that the following proof works

  induction m with m ih,
  rw mul_zero, refl,
  exact ih,

This is because 0 * succ m is definitionally equal to 0 * m. Everything in the chain of equalities 0 * succ m = 0 * m + 0 = 0 * m is part of the definition of the functions + and * in simplistic terms. exact ih works because ih is definitionally equal to the goal

[Chris Hughes]

it is a bit surprising that the rw and assumption parts of rwa were applied to different goals.

[Kevin Buzzard]

Nice Easter egg!