How to prove n.succ \geq 1 for nat n?

Stream: new members

[Sara Fish]

Originally I wanted to prove

theorem nonzero_gt_one (n : ℕ ): ¬ n = 0 → n ≥ 1

I tried library_search but couldn't find anything. So I started to try to prove this theorem by hand and got stuck here.

theorem nonzero_gt_one (n : ℕ ): ¬ n = 0 → n ≥ 1 :=
begin
    intro h,
    induction n,
    exfalso, apply h, refl,
    sorry -- how to prove n_n.succ ≥ 1 ?
end

Once again, these seems like something library_search should be able to handle but nothing was coming up. I also typed "nat." in VSCode and manually looked through proven results about natural numbers but nothing seemed particularly applicable.

How can I prove this (frustratingly simple) theorem?

[Jalex Stark]

omega?

[Jalex Stark]

I think if you replace n \ge 1 with 1 \le n you will have more library_search luck

[Sara Fish]

omega did the trick, thanks. Forgot it exists.

[Jalex Stark]

library_search doesn't try as hard as you might expect to unify the goal with each theorem it compares it to

[Jalex Stark]

so it's sensitive to syntactic equality

[Sara Fish]

Replacing with \le still didn't work...is there any way to find out what omega did?

[Jalex Stark]

I think the omega algorithm doesn't naturally produce readable certificates

[Bryan Gin-ge Chen]

You can write show_term { omega }, but it's not going to be very enlightening.

[Jalex Stark]

also replace \n n = 0 with n \ne 0

[Jalex Stark]

this is another syntactic choice; in mathlib we try to consistently use \ne and \le in order to make search work (or at least, work up to knowing which expressions are "idiomatic" or "normal form")

[Bryan Gin-ge Chen]

There's some info on omega here: tactic#omega

[Bryan Gin-ge Chen]

I am a little surprised this one isn't in the library. I tried changing to \ne and \le and library_search and suggest still couldn't find a proof.

[Reid Barton]

theorem nonzero_gt_one (n : ℕ ): ¬ n = 0 → n ≥ 1 := nat.pos_of_ne_zero

[Jalex Stark]

suggest works for me here

import tactic

theorem nonzero_gt_one (n : ℕ ): ¬ n = 0 → n ≥ 1 :=
begin
  intro h,
  induction n,
  contrapose! h, { refl },
  suggest,
  --exact inf_eq_left.mp rfl,
  sorry -- how to prove n_n.succ ≥ 1 ?
end

[Sara Fish]

OK, I've learned to always try suggest and hint before posting here! :)

[Sara Fish]

(hint just told me to use omega)

[Bryan Gin-ge Chen]

I opened an issue about library_search: #3432

[Alex J. Best]

library_search! works for me for the original goal here (with the !) giving exact inf_eq_left.mp rfl, , but not for Bryans ticket