Stuck at totality proof in natural numbers game

Stream: new members

[metakuntyyy]

This is what i have proven so far

induction y with d hd
right
apply zero_le
cases hd with he hf
left
cases he with a ha
induction a with aa haa
rw[ha]
rw[add_zero]
apply le_succ_self
rw[ha]
use ( succ (succ aa))
rw[add_succ]
symm
rw[add_succ]
rw[add_succ]
rfl

Now I am stuck proving
Objects:
xd: ℕ

Assumptions:
hf: d ≤ x

Goal:

x ≤ succ d ∨ succ d ≤ x

It feels as if I have made zero progress.

[metakuntyyy]

And what is also hard while I have proven some theorems like le_trans for example I have no idea how to get it into context
It is not explained which tactics make an useful application of this theorem possible

[metakuntyyy]

Oh and that is the level https://adam.math.hhu.de/#/g/leanprover-community/NNG4/world/LessOrEqual/level/8

[Bbbbbbbbba]

metakuntyyy said:

It feels as if I have made zero progress.

Actually this is good progress as you really just need to know d - x to progress

[metakuntyyy]

Yeah, but I don't really understand what that means. I know there should be two cases either d = x or d < x. If d=x then left is correct, but if d<x then the right is correct. I don't know how to apply it though

[metakuntyyy]

Do I do induction, or split, or use or a rewrite?

[Bbbbbbbbba]

If d = x then x - d = 0, and if d < x then x - d > 0

[Bbbbbbbbba]

And you can figure out which because you have x - d

[metakuntyyy]

induction y with d hd
right
apply zero_le
cases hd with he hf
left
cases he with a ha
induction a with aa haa
rw[ha]
rw[add_zero]
apply le_succ_self
rw[ha]
use ( succ (succ aa))
rw[add_succ]
symm
rw[add_succ]
rw[add_succ]
rfl
cases hf with c hhc
cases c
rw [add_zero] at hhc
left
rw[hhc]
apply le_succ_self
right
rw[hhc]
rw[add_succ]
rw[← succ_add]
rw[← add_zero (succ d)]
rw[add_assoc]
rw[zero_add]

Alright I am left with the following goal:
Objects:
xda: ℕ

Assumptions:
hhc: x = d + succ a

Goal:

succ d + 0 ≤ succ d + a

How do I close it now?

[metakuntyyy]

Nevermind, I've closed it. It was use a

[metakuntyyy]

That was pretty hard.

[metakuntyyy]

Well but I have no idea now how to prove the next one. I need to show that succ_le_succ: If succ(x)≤succ(y) then x≤y.
I have no idea where to start and which theorems to use.

induction x with x h
apply zero_le

This was my start but then I am completely stuck

[Bbbbbbbbba]

Don't need induction at all for this one

[Bbbbbbbbba]

Remember to prove x≤y you just need to find the value of y-x

[metakuntyyy]

Yeah but I still don't understand what that means. Do I unfold the hypothesis. Do I do cases? Do i do use?

cases x
apply zero_le

This would be my ansatz, which leaves me with this goal:
Objects:
ya: ℕ

Assumptions:
hx: succ (succ a) ≤ succ y

Goal:

succ a ≤ y

Which again feels like I've made no progress

[Bbbbbbbbba]

You can do cases hx at the start

[metakuntyyy]

ayy, that helps. Thanks, I didn't know that

[metakuntyyy]

It worked. Thank you very much.

[metakuntyyy]

Ok I am further in the game. Level 9/10 of the last level.

induction b with d hd generalizing c
cases a with d j
trivial
rw[mul_zero] at h
rw[succ_mul] at h
symm at h
apply add_left_eq_zero at h
rw[h]
rfl

I am stuck proving
a: ℕ
d: ℕ
c: ℕ

Assumptions:
ha: a ≠ 0
hd: ∀ (c : ℕ), a * d = a * c → d = c
h: a * succ d = a * c

Goal:

succ d = c
In my opinion I should just be able to apply hd at h. But it doesn't work for some reason

[Bbbbbbbbba]

Because the d in h is the same d in hd

[metakuntyyy]

So what did I do wrong here?
I really am not grasping this concept

[metakuntyyy]

What do I need to do, do I need to shift the succ from the left side to the right side to be able to apply the theorem?

[Yaël Dillies]

This is a tricky one

[Yaël Dillies]

a * succ d = a * c definitely doesn't hold if c = 0. So what about you deal with that case first?

[metakuntyyy]

Alright, so cases c?

[metakuntyyy]

Thanks, it worked. ;)

[metakuntyyy]

Final level, final boss, here I come.

[metakuntyyy]

Alright, I have finished with advanced multiplication world. It mentions a division world yet that one seems not there.

[Kevin Buzzard]

Sorry, I've been distracted by other things. There are some worlds which are in a half-finished or even near-finished state but which aren't online

[metakuntyyy]

Ah cool. No worries @Kevin Buzzard I absolutely enjoyed playing your game, even if I were stuck for an hour or so on a particularly difficult problem. Where do I go from here, are there any more tutorials/games I could play to learn theorem proving?

[Kevin Buzzard]

You should read Mathematics in Lean next, which is at the other end of this link #mil .

[Mark Fischer]

If your goal is just to gain extra familiarity with Theorem proving, I would also recommend the Set Theory Game (It uses the same framework as NNG) - https://adam.math.hhu.de/#/g/djvelleman/stg4 :smile: