unexpected pattern match fail

Stream: new members

[Shi Zhengyu]

(deleted)

[Shi Zhengyu]

(deleted)

[Shi Zhengyu]

Sorry for the previous deletes, I just figured out the previous problem was due to my poor understanding! But this one frustrates me:
I have
image.png
but rw what at funny2 throws error that says
image.png
It's right there ... Why does pattern matching fail to detect it? Or am I somewhere wrong?
Thanks!

[Scott Morrison]

Screenshots are not super useful: if you can post a #mwe, we're much more likely to be able to help.

[Scott Morrison]

I think we're going to need to have a reproducible context to debug.

[Scott Morrison]

Do you by chance have more than one N hypothesis?

[Scott Morrison]

(The fact that N appears below funny2 in the hypothesis list makes me suspicious.)

[Shi Zhengyu]

Scott Morrison said:

(The fact that N appears below funny2 in the hypothesis list makes me suspicious.)

Yes That is correct! I accidentally added another N into environment .. ! Hope lean have some warnings on variable shadowing in local environment though ...

[Shi Zhengyu]

Scott Morrison said:

Screenshots are not super useful: if you can post a #mwe, we're much more likely to be able to help.

I see. Thanks for reminder :D

[Scott Morrison]

Hopefully we can be more helpful about shadowing in Lean 4. In Lean 3 it has been hard to avoid.

[Mario Carneiro]

Lean 4 should never display shadowed variables in a confusable way, because it puts the dagger on shadowed variables even if that's not in the actual name of the variable