Unknown identifier in NNG Multiplication World 3/9

Stream: new members

[R Dong]

I'm trying to figure out why I can't proceed with the proof:

induction b with b' h
repeat rw [mul_zero]
rw [add_zero]
rfl
repeat rw [mul_succ]
nth_rewrite 2 [succ_eq_add_one a]
rw [succ_eq_add_one b']
repeat rw [← add_assoc]

Lean says add_right_cancel is unknown. However, I can see that it's available (and not locked) from the panel to the right. Am I misunderstanding what theorems are available?

[R Dong]

It seems like I can't apply any theorem

[R Dong]

I solved it with only rewrite rules, but I feel like that's not the best way to do it...

[Etienne Marion]

I don't know why add_right_cancel is unknown, but here it won't help you anyway because what you want to prove is in the other direction

[R Dong]

image.png
Is this not exactly add_right_cancel?

[R Dong]

Isn't (a b n : ℕ) (a✝ : a + n = b + n) : a = b directly applicable?

[R Dong]

Ok, I see what you mean

[Etienne Marion]

Personally on this level I went for a full rw proof too

[R Dong]

I explored a different path where I tried to apply succ_inj and that one is unknown too

[Etienne Marion]

I think this is because these lemmas are introduced in worlds parallel to multiplication world and so are considered unknown even if you completed those worlds before

[R Dong]

But they are not locked/grayed out in the panel. I can also use all the other rewrite rules

[Etienne Marion]

You can't use all the rewrites

[R Dong]

Ok, I didn't try all the rewrite rules

[Martin Dvořák]

Maybe it is related to the bug:
#general > Bug in NNG?