## Stream: new members

### Topic: getting from 2 = 1 to false

#### Matt Diamond (Jan 14 2021 at 21:40):

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...

(deleted)

#### Alex J. Best (Jan 14 2021 at 21:45):

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

#### Alex J. Best (Jan 14 2021 at 21:45):

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 (Jan 14 2021 at 22:01):

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 (Jan 14 2021 at 22:09):

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.

that makes sense