# Zulip Chat Archive

## Stream: new members

### Topic: From n<=1, get n=0 or n=1

#### Patrick Stevens (May 11 2020 at 17:34):

I'm sure I've seen before that there's a tactic to turn a hypothesis `n <= 1`

into `n = 1 \/ n = 0`

, but I can't find it :( I could prove it by induction, but I think I remember someone mentioning a more general tactic that splits inequalities into individual cases. Can anyone remember what that was?

#### Jeremy Avigad (May 11 2020 at 17:36):

https://leanprover-community.github.io/mathlib_docs/tactics.html#interval_cases

#### Jeremy Avigad (May 11 2020 at 17:44):

For small examples like this, `cases`

is also sometimes useful:

```
example (n : ℕ) (h : n ≤ 1) : n = 0 ∨ n =1 :=
begin
cases h with h h,
{ right, refl },
cases h with h h,
{ left, refl }
end
```

It's also mentioned and used briefly in the last example here, https://avigad.github.io/mathematics_in_lean/the_natural_numbers.html. Some of the tricks in Section 3.2 may also be helpful.

```
import data.nat.basic
example : ∀ n, n ≤ 1 → n = 0 ∨ n = 1 :=
dec_trivial
```

#### Kevin Buzzard (May 11 2020 at 17:44):

Back in the old days, before that tactic, I would just do cases on n and then cases on everything that showed up until I was down to the two cases. For n<=1 this would work fine but for any larger ranges the tactic is definitely the way to proceed. Actually I bet this can be done with `rcases`

in some cool way.

#### Kevin Buzzard (May 11 2020 at 17:44):

Hah Jeremy beat me to it :-)

#### Jeremy Avigad (May 11 2020 at 17:45):

The new tutorial doesn't yet mention the `interval_cases`

tactic, but I'll add that.

#### Chris Hughes (May 11 2020 at 18:02):

You could use `omega `

as well.

Last updated: Dec 20 2023 at 11:08 UTC