N, order, 0 and 1

Stream: general

[Ned Summers]

Hey, I'm trying to prove the seemingly very simple

example (n : ℕ) (h : n < 1) : n = 0 := sorry

It's revealing a lot about what I don't know in lean (like getting stuck getting 1>n from n<1) and would welcome any advice/solutions. I'm not working very much at all with order or N at any other stage so, despite wading through theorems the past couple of days trying to find what I need, I'm giving up a bit. Thanks.

(Also, I'm using this to show that if you take any (a : fin 1) then a = 0. I suspect too that this is probably much simpler than what I'm doing.)

[Mario Carneiro]

you should be able to do it by cases

[Mario Carneiro]

not my favorite proof:

example (n : ℕ) (h : n < 1) : n = 0 :=
by cases h with _ h; [refl, cases h]

[Mario Carneiro]

example (n : fin 1) : n = 0 :=
fin.cases rfl (λ i, i.elim0) n

[Mario Carneiro]

example : ∀ (n : fin 1), n = 0 := dec_trivial

[Patrick Massot]

It's revealing a lot about what I don't know in lean (like getting stuck getting 1>n from n<1) and would welcome any advice/solutions.

This is literaly the same thing.

example (n : ℕ) (h : 1 > n) : n < 1 := h

example (n : ℕ) (h : 1 > n) : n < 1 :=
begin
change 1 > n,
assumption
end

[Patrick Massot]

Note that the change is here so you see it in the interative message window, but it's useless

[Kenny Lau]

import data.nat.basic

example : ∀ (n : ℕ), n < 1 → n = 0 :=
dec_trivial

[Ned Summers]

Thanks everyone, dec_trivial is a nice thing to know about. Will be using this to ponder where my break in understanding was.