Prime norm num extension

[kmill]

The extension now lives in the Mathlib.Tactic.NormNum.Prime module, and you don't get it automatically by importing the definitions like you did in Lean 3 (we're trying to keep theory and meta code separate in mathlib4).

This tripped up a number of students during the first week of the MSRI workshop, and there was another question about it on Zulip which reminded me to make an issue.

[PatrickMassot]

I fixed that issue in b3adcb0.