What do I need to import to do basic natural number stuff?

Stream: new members

[Paul Crowley]

I'm getting an error failed to synthesize LT ℕ when I try to use the < symbol, which I guess means I need to import something? But I'm not sure what to import. I finished the Natural Number game, and installed Lean 4 using the vscode extension, and this is my first time trying to use mathlib.

-- This module serves as the root of the `Test5` library.
-- Import modules here that should be built as part of the library.
import Test5.Basic

import Init.Data.Nat
import Init.Data.Nat.Basic
import Init.Data.Nat.Compare
import Batteries.Data.Nat
import Batteries.Data.Nat.Basic
import Batteries.Data.Nat.Lemmas
import Batteries.Tactic.Basic


theorem exists_add_of_lt {a b : ℕ} (h : a < b) : ∃ c, a + c = b := by
  use b - a
  rw [Nat.add_sub_of_le h.le]

#print exists_add_of_lt

[Bulhwi Cha]

Try importing Mathlib.Data.Nat.Notation. If you also want to use the use tactic, import Mathlib.Tactic.Use as well.

import Mathlib.Data.Nat.Notation
import Mathlib.Tactic.Use

theorem exists_add_of_lt {a b : ℕ} (h : a < b) : ∃ c, a + c = b := by
  use b - a
  rw [Nat.add_sub_of_le (Nat.le_of_lt h)]

#print exists_add_of_lt

[Ruben Van de Velde]

In particular, without that import, lean doesn't know \N is supposed to mean the natural numbers

[Paul Crowley]

This works, thanks! How should I have found this out for myself?

[Chris Bailey]

With the much-maligned autoImplicit feature on by default, you either have to poke around quite a bit or do what you did, which is ask someone else what's wrong. It's possible to turn the autoimplicit feature off globally in all of your projects (and I would recommend it): https://proofassistants.stackexchange.com/questions/2189/project-wide-set-option-autoimplicit-false-in-lean-4

[Paul Crowley]

what does this feature do?

[rzeta0]

So far I have been able to do all my examples with just one import Mathlib.Tactic which seems to pull in much of the common definitions and tactics.

It seems to work for your example too.

import Mathlib.Tactic

theorem exists_add_of_lt {a b : ℕ} (h : a < b) : ∃ c, a + c = b := by
  use b - a
  rw [Nat.add_sub_of_le h.le]

[Niels Voss]

what does this feature do?

When on (as it is by default), undefined variables will be converted into implicit parameters instead of giving you an error. So in your example, Lean didn't know what \N was, so it converted it into a parameter. And then you got an error later, because < is not defined for arbitrary types.

[Bulhwi Cha]

Paul Crowley said:

This works, thanks! How should I have found this out for myself?

I searched Mathlib4 docs for the notation ℕ and the use tactic. I admit it's a bit tricky.

[Paul Crowley]

This seems to be how to do it with lakefile.toml https://github.com/PatrickMassot/verbose-lean4/blob/master/lakefile.toml