Mention of ``assumption`` in Advanced Addition Level 4

[RodneyMKay]

In level 4/6 of the advanced addition world, the solution via induction uses the assumption tactic, which is not part of the course. This is not an issue per-se, but it's a bit confusing to someone (like myself), who has never seen this tactic. Might be worth it to explain what that's about in the comment or replacing both assumption with apply h.

Code reference: https://github.com/leanprover-community/NNG4/blob/7400b127d25fd8b6e5ef5591dcbaa43834dccfce/Game/Levels/AdvAddition/L04add_right_eq_self.lean#L59

If you tell me how you want it solved (whether that be an additional hint explaning assumption, replacing it with apply h or introducing assumption as a concept properly in some level), I'll gladly create a PR for it :)

PS: Thanks for creating such an awesome learning resource for lean!

[zetaraku]

I encountered this confusion too and I think it was a mistake when simplifying the level. (See: https://github.com/leanprover-community/NNG4/commit/a01eb1bd00083ff648b08fc6055608706e0c5bdf)

I think it's better to fix it by replacing it with apply h.

The maintainer may be busy, so I recommend you open a PR to fix it.

[joneugster]

Sorry for the late reply! I think the NNG usually uses exact h in these situations instead of assumption. (but apply h is fine, too) If you want to make a PR that's very welcome, otherwise I will address this the next time I'll update the game on the author's behalf, which might still take a moment as there is another problem I haven't fully addressed yet

[zetaraku]

Oh, it's exact h. My mistake. 😄

[RodneyMKay]

Oh! I just started work on a PR, but seems like someone was ahead of me in https://github.com/leanprover-community/NNG4/pull/64. Gonna close this issue then, since it's solved. Thanks again :D