norm_num and fin

Stream: maths

[Yury G. Kudryashov]

The following #mwe doesn't work. How can I make norm_num work with fin n? @Mario Carneiro

import tactic.norm_num

example : (2 : fin 3) = 0 := by norm_num

[Mario Carneiro]

norm_fin

[Mario Carneiro]

actually that one should work in norm_num

[Yury G. Kudryashov]

It doesn't. norm_fin works.

[Mario Carneiro]

oh, it's just your imports

[Mario Carneiro]

if you import tactic.norm_fin then norm_num works

[Mario Carneiro]

because tactic.norm_fin declares a norm_num extension

[Jakub Kądziołka]

wait, how come 2 = 0 in that type?

[Alex J. Best]

It doesn't, I guess its a typo

[Kevin Buzzard]

yeah, it adds to the mystery of the question that an expert Lean user is complaining about how he can't prove an obviously false statement

[Mario Carneiro]

when I say "works" above I mean it reduces to false instead of leaving it as is

[Eric Wieser]

Who needs norm_num?

example : (3 : fin 3) = 0 := rfl