missing `add_left_cancel`

Open joneugster opened this issue 1 year ago • 3 comments

As reported on Zulip:

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Bug.20in.20NNG.3F

Is this a namespace/import issue?

Oct 10 '24 07:10 joneugster

FYI the theorem is in Mathlib.Algebra.Group.Defs.

Oct 10 '24 07:10 madvorak

I think NNG does not import Mathlib at all, but instead it recreates anything it uses

Oct 10 '24 13:10 joneugster

This bug occurs when the user has completed adv_addition_world and has unlocked add_left_cancel or add_right_cancel but for solving the levels in multiplication_world, both of those are not necessary. The right panel in the UI shows the theorems as unlocked but lean does not have those theorems imported. Hence, it shows the observed error unknown identifier: add_left_cancel.

Same as https://github.com/leanprover-community/NNG4/issues/96 and https://github.com/leanprover-community/NNG4/issues/98

Aug 04 '25 15:08 DeathStroke19891