In lean 3 we had

https://github.com/leanprover-community/mathlib3/blob/65a1391a0106c9204fe45bc73a039f056558cb83/src/data/nat/prime_norm_num.lean#L158-L251

Probably this is no longer elegible for norm_num, but it would be eligible for a simproc.

Either we should revive the old code, or use a simpler strategy of computing the factors and showing that [2, 3, 3].prod = 12 by rfl.