7 is prime?

Stream: maths

[Geno Racklin Asher]

In the following example from the book Mathematics in Lean, why is norm_num unable to determine the primality of 7?

example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by
  use 5
  use 7
  norm_num
  sorry

[Geno Racklin Asher]

Ah, apparently I needed to import Mathlib.Tactic.NormNum.Prime as well as just the base tactic.

[Kyle Miller]

(Mathematics in Lean needs to be updated here. The book was ported to Lean 4 recently, and the Prime norm num extension was ported at about the same time, but it was put in a different module from where it used to be. I created an issue to track this.)

[Kevin Buzzard]

@Geno Racklin Asher just import Mathlib.Tactic if you want to get all the useful tactics.

[Patrick Massot]

I'm sorry about this inconvenience. I just added import Mathlib.Tactic on top of every file in the book.

[Kevin Buzzard]

@Patrick Massot this has broken the book. For example in chapter 7 section 1 the local notation notation "𝟙" => One₁.one conflicts with category theory notation, and in chapter 3 section 4 Import Tactic makes norm_num better and it closes a goal too early.

[Patrick Massot]

:sad: we really need proper CI for this project... I'm sorry

[Patrick Massot]

That being said, I really understand why important Mathlib.Tactic needs category theory...

[Patrick Massot]

And category theory also takes 𝟭

[Patrick Massot]

We really need to get rid of the habit of putting such notations in the root namespace.

[Kevin Buzzard]

If you just remove import Mathlib.Tactic from those two files, it compiles again.

[Patrick Massot]

I pushed fixes already.

[Patrick Massot]

And I'm currently recompiling mathlib4 with the proper fix.

[Sebastien Gouezel]

If you PR a change putting the category theory notations in a namespace and open this namespace in the relevant files, I am sure category theory people will be happy to merge it.

[Patrick Massot]

Yes, I'm simply adding scoped at the beginning of a couple of lines in CategoryTheory.Category.Basic. And so far I found only one file where you need to add open CategoryTheory (the sheafify file).

[Patrick Massot]

I opened #5685. The final count is that two files needed an extra open CategoryTheory.