proof of total order in the N game

Stream: new members

[Daniel Teixeira]

I'm stuck at the <= world part 8 of the natural number game. Right now I have the current hypothesis and subgoal and I up to getting the correct syntax I think this subgoal would be closed by

exact le_trans x d d.succ h1 (le_succ_self d)

but there is a message saying that le_trans isn't available.

image.png

[Aaron Liu]

is _root_.le_trans bleeding through?

[Aaron Liu]

try doing exact MyNat.le_trans x d d.succ h1 (le_succ_self d)

[Aaron Liu]

I would be able to help more if you shared your full code for the level instead of just that part that didn't work

[Daniel Teixeira]

right

exact zero_le x

cases hd with h1 h2

left

exact le_trans x d d.succ h1 (le_succ_self d)

[Daniel Teixeira]

using MyNat.le_trans did work

[Aaron Liu]

interesting, it seems to work fine on my end

[Eduardo Cavazos]

Daniel Teixeira said:

using MyNat.le_trans did work

I can confirm I'm seeing this as well.

In level 8 of "≤ World":

https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/LessOrEqual/level/8

if I use le_trans we get the message:

The theorem/definition 'le_trans' is not available in this game!

image.png

Workaround

If I use apply MyNat.le_trans x d, the message goes away:

image.png

Bug?

We prove le_trans in level 4 of the same world. So it seems it should be available without issue:

image.png

Hey @Kevin Buzzard :man_raising_hand:
Do you think this is a bug?
I.e. should le_trans be available in level 8 without having to qualify it as MyNat.le_trans?

[Kevin Buzzard]

Works fine for me:

Screenshot from 2025-10-02 09-16-55.png

I have "Rules" switched to "none". Have you just not unlocked le_trans or something?

[Aaron Liu]

Kevin Buzzard said:

Works fine for me:

Screenshot from 2025-10-02 09-16-55.png

I have "Rules" switched to "none". Have you just not unlocked le_trans or something?

I think the problem is that le_trans is being elaborated as _root_.le_trans instead of MyNat.le_trans and you never unlock _root_.le_trans

[Eduardo Cavazos]

Kevin Buzzard said:

Works fine for me:

Screenshot from 2025-10-02 09-16-55.png

I have "Rules" switched to "none". Have you just not unlocked le_trans or something?

I have "Rules" set to regular:

image.png

[Eduardo Cavazos]

Kevin Buzzard said:

Works fine for me:

Screenshot from 2025-10-02 09-16-55.png

Have you just not unlocked le_trans or something?

As far as le_trans being unlocked, I've completed level 4:

image.png

And it shows up under "Theorems" as available (also shown in screenshot above).

[Aaron Liu]

Aaron Liu said:

Kevin Buzzard said:

Works fine for me:

Screenshot from 2025-10-02 09-16-55.png

I have "Rules" switched to "none". Have you just not unlocked le_trans or something?

I think the problem is that le_trans is being elaborated as _root_.le_trans instead of MyNat.le_trans and you never unlock _root_.le_trans

After trying it out again I can confirm this is definitely not what's happening

[Aaron Liu]

After a bit more inspection I have discovered that it shows the hover information of MyNat.le_trans but it elaborates as _root_.le_trans

[Aaron Liu]

I give up debugging this is too weird

[Kevin Buzzard]

@Eduardo Cavazos maybe you want to open an issue on the NNG4 repo? This is not going to be something I can help you with.