# Zulip Chat Archive

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

#### Marcus Rossel (Jan 14 2021 at 21:43):

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

#### Riccardo Brasca (Jan 14 2021 at 22:09):

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

#### Matt Diamond (Jan 14 2021 at 22:12):

that makes sense

#### Matt Diamond (Jan 14 2021 at 22:13):

thank you both for the helpful answers!

Last updated: May 10 2021 at 00:31 UTC