From n<=1, get n=0 or n=1

Stream: new members

[Patrick Stevens]

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]

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

[Jeremy Avigad]

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]

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]

Hah Jeremy beat me to it :-)

[Jeremy Avigad]

The new tutorial doesn't yet mention the interval_cases tactic, but I'll add that.

[Chris Hughes]

You could use omega as well.