n + 1 = 1 -> n = 0

Stream: general

[Valéry Croizier]

Hi, Lean and Zulip newbie there, not sure where to post exactly. Stuck on this calculation. How to prove it?

[Bryan Gin-ge Chen]

Welcome! Is this what you want:

example (n : ℕ) : n+1 = 1 → n = 0 := nat.succ.inj

[Bryan Gin-ge Chen]

In general you can find lemmas from the library with library_search:

import tactic

example (n : ℕ) : n+1 = 1 → n = 0 := by library_search

[Valéry Croizier]

Is this a reference to succ_inj in nat/lemmas ?

[Johan Commelin]

@Valéry Croizier To explain why nat.succ.inj proves this: n + 1 = succ n by definition, and 1 = succ 0, by definition.

[Valéry Croizier]

My Lean doesn't know library_search :(

[Johan Commelin]

Did you import tactic?

[Bryan Gin-ge Chen]

I think nat.succ_inj was renamed to nat.succ.inj recently, so it may depend on what version of Lean you're using.

[Valéry Croizier]

I use VSCode and elan on WSL2.

[Bryan Gin-ge Chen]

See #install for instructions on installing the latest version of Lean along with mathlib.

[Valéry Croizier]

My install is just a few days old. leanpkg.toml says leanprover-community/lean:3.16.4.

[Bryan Gin-ge Chen]

Then example (n : ℕ) : n+1 = 1 → n = 0 := nat.succ.inj should work...

[Valéry Croizier]

Anyway, nat.succ.inj works, so thank you very much for you help.

[Bryan Gin-ge Chen]

I recommend figuring out how to install mathlib so you can use library_search and other tactic goodies though. Let us know if you have any trouble.

[Valéry Croizier]

OK, library_search missed some imports mentioned in the doc. Nice. :slight_smile: