getting from 2 = 1 to false

Stream: new members

[Matt Diamond]

I was working on a simple proof by contradiction and got to the point where I was able to generate the hypothesis h : 2 = 1. On a whim I tried cases h and it closed out the goal (which was false). So I have two questions:
1) why did cases work here?
2) is there a better or more "correct" way to get from 2 = 1 to false? I figure I'm probably missing something embarrassingly obvious...

[Marcus Rossel]

(deleted)

[Alex J. Best]

cases seems fine in this situation, if the numbers were bigger using tactic#norm_num would be better.

[Alex J. Best]

For example:

example (h : 200000 = 1000000) : false :=
begin
  norm_num at h,
end

works, but

example (h : 200000 = 1000000) : false :=
begin
  cases h,
end

gives
deep recursion was detected at 'expression equality test' (potential solution: increase stack space in your system), not so fun

[Riccardo Brasca]

If your question is why Lean can prove this "by cases", this is because N is an inductive type: a natural number is 0 or of the form succ n for some n : N. cases is smart enough to write 1 as succ 0 and 2 as succ 1 = succ (succ 0) and it also knows that succ is injective (this is quite subtle point I think, related to no_confusion).

[Riccardo Brasca]

This is analogous to having a finite set $S = \{a, b\}$ and saying that, given $x \in S$, we have $x=a$ or $x=b$. Even if for a human being (at least, for me) these two situations are rather different, for Lean they are very similar, a finite type is an inductive type where you can enumerate all elements.

[Riccardo Brasca]

See for example https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html

[Matt Diamond]

that makes sense

[Matt Diamond]

thank you both for the helpful answers!