## 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: May 12 2021 at 04:19 UTC