Natural Numbers Game le_antisymm

Stream: new members

[Jafar Tanoukhi]

Hi, I was playing through NNG and I reached this weird point while proving anti-symmetry of ≤.

image.png

Why was the goal not closed? And what is N as a goal?

[Aaron Liu]

something introduced a metavariable which was not unified

[Aaron Liu]

do you have a version I can copy into the website

[Jafar Tanoukhi]

not sure if you can directly access the level from here : https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/LessOrEqual/level/6

also here's the code :

cases hxy with a ha
cases hyx with b hb
rw [ha, add_left_eq_self x, zero_add] at hb
symm at hb
apply add_right_eq_zero at hb
rw [hb] at ha
rw [add_zero] at ha
symm at ha
exact ha

[Aaron Liu]

when you rewrote with add_left_eq_self x you failed to provide the proof that x + y = y and then Lean got couldn't figure out what is y so it put that as a new goal as well

[Jafar Tanoukhi]

Oh I see, by changing it to add_left_eq_self x (a+b) it gave a more "normal" result
but the goal still did not close after the exact instead i received another goal x + (a + b) = a + b

I assume this has something to do with cases ?

[Aaron Liu]

this has to do with how add_left_eq_self expects you to give it a proof that x + y = y

[Aaron Liu]

but you didn't so rw assumed you wanted to do it later and put it into a new goal

[Jafar Tanoukhi]

Makes perfect sense thanks!

[Jafar Tanoukhi]

by changing it to apply i was able to make it work

[Jafar Tanoukhi]

I understand the difference between apply and rw better now :D (also not sure if that was on purpose, but thanks for not outright giving the solution) :slight_smile:

[Jafar Tanoukhi]

I have another question regarding another level within the natural numbers game, should i open another thread?

[Kevin Buzzard]

Up to you, threads are cheap

[Kevin Buzzard]

I would open another one yes, if it's a different question