feat: experimental hack to allow by finiteness auto-params

[grunweg]

This provides a way to apply by finiteness auto-parameters in simp lemmas.

(Making simp run dischargers natively requires unfortunate hacks... so is not easily doable.)

Another alternative: make a simproc to run auto-params in general. This might be even better.

Written at the Mathlib Initiative Retreat. Thanks to Joachim Breitner and Henrik Böving for the help writing this!

---

The hack is calling runTactic: if finiteness (and, hence, aesop) could be called from an appropriate meta function instead, we could make the implementation more robust.

[github-actions]

PR summary 55d0c0d87d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.ENNReal.Basic	725	726	+1 (+0.14%)

Import changes for all files

Files	Import difference
5 files Mathlib.Analysis.Normed.Lp.WithLp Mathlib.Data.ENNReal.Basic Mathlib.Data.ENNReal.Lemmas Mathlib.Data.ENNReal.Real Mathlib.Data.Real.ENatENNReal	1

---

Declarations diff

+ autofinite

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[grunweg]

Actually, #39333 may be a better solution here. That will not require modifying any existing auto-params.
(Like this PR, it only addresses the issue for simp lemmas, not rw lemmas.)

Using the discharger as in that PR may break proofs (where previously simp was used as discharger) --- but using disch := first | run_auto_param | simp as discharger will fix that.

In the future, if simp's default discharger were changed to this discharger, that would simplify live in mathlib greatly.