A newbie question and Is there a newbie friendly channel?

Stream: general

[B YI]

I have a question related to the lean game server.

My question is that why I can't apply hn at h in the screenshot?

Failed to find succ 0 = succ (succ nn) as the type of a parameter of succ 0 = succ nn → 0 = nn.

screenshot-2024-07-14-15-24-44.png

[Edward van de Meent]

what would you expect to happen?

[Edward van de Meent]

also, to answer the question in the title: that's #new members

[Kevin Buzzard]

You can't apply hn because the hypothesis of hn doesn't match h, there's an extra succ in h.

[B YI]

The hypothesis of hn is more general than h. I thought I can still apply it (like apply a value of a subtype to a function).

[Kevin Buzzard]

No, both hn and h are statements about a specific number nn in your context. They do not say "for all numbers nn...".

[B YI]

Got it. Thanks.

[Kevin Buzzard]

If you had a number x in your context and also a proof hx : x = 37 then you would not be able to deduce that all numbers were equal to 37. It's the same phenomenon here.

[Kevin Buzzard]

Lean's logic can be brutal at times :-)