mathlib3

3c1368ca - fix(data/nat/squarefree): `norm_num` only supports `squarefree` on naturals (#18708)

fix(data/nat/squarefree): `norm_num` only supports `squarefree` on naturals (#18708) We have a `norm_num` extension for proving whether natural numbers are squarefree. This tactic does not work on other rings, like integers, but the check for this case was broken, meaning it returned a proof with a type error instead of skipping the goal. This PR changes the check to only fire the `norm_num` extension on natural numbers. I've included a small test that checks `norm_num` fails on integers, instead of returning a type-incorrect proof. We'd have to replace this test if `norm_num` gains support for `squarefree` on integers.