feat: port Mathlib 3's Nat.factors norm_num extension to a simproc

[eric-wieser]

This is a partial attempt at #15410, porting #8009

---

[github-actions]

PR summary 3da8b59516

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Tactic	1
Mathlib.Tactic.NormNum.Factors (new file)	472

---

Declarations diff

+ FactorsHelper.cons
+ FactorsHelper.cons_of_le
+ FactorsHelper.cons_self
+ FactorsHelper.nil
+ FactorsHelper.primeFactorsList_eq
+ FactorsHelper.singleton
+ FactorsHelper.singleton_self
+ evalPrimeFactorsList
- factorsHelper_cons
- factorsHelper_cons'
- factorsHelper_end
- factorsHelper_nil
- factorsHelper_same
- factorsHelper_same_sn
- factorsHelper_sn

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[YaelDillies]

Could you add more inline comments in the meta code? It would help maintainability

[YaelDillies]

Suggested change

	theorem FactorsHelper.same {n m : ℕ} (a : ℕ) {l : List ℕ}
	(h : IsNat (a * m) n) (H : FactorsHelper m a l) :
	FactorsHelper n a (a :: l) := fun pa =>
	theorem FactorsHelper.cons_self {n m : ℕ} (a : ℕ) {l : List ℕ}
	(h : IsNat (a * m) n) (H : FactorsHelper m a l) :
	FactorsHelper n a (a :: l) := fun pa =>

maybe?

[YaelDillies]

By the same logic, this would be

Suggested change

	theorem FactorsHelper.same_singleton (a : ℕ) : FactorsHelper a a [a] :=
	theorem FactorsHelper.singleton_self (a : ℕ) : FactorsHelper a a [a] :=

[YaelDillies]

Why do we give up on computing primeFactorsList 0 here?

[eric-wieser]

This is the aux function, which expects the 0 and 1 cases to already have been dispatched, such that a can be chosen as a prime less than n.

I'll make it private to make this a little more clear.