perf(Tactic/FastInstance): use whnf on data fields

[JovanGerb]

This PR lets fast_instance% make even faster instances by using whnf on data fields.

This PR also changes withReducible to the more appropriate withReducibleAndInstances in the implementation.

---

[github-actions]

PR summary b1b1f5f52d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for e283a60 against b1b1f5f are in. Significant changes detected! @JovanGerb

• ✅ build//instructions: -154.8G (-0.09%)

Large changes (1✅)

• ✅ build/module/Mathlib.Algebra.Order.Ring.StandardPart//instructions: -57.2G (-34.55%)

Medium changes (7✅, 4🟥)

• 🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic//instructions: +1.9G (+7.65%)
• 🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula//instructions: +3.2G (+5.63%)
• 🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point//instructions: +8.2G (+7.06%)
• 🟥 build/module/Mathlib.Analysis.CStarAlgebra.lpSpace//instructions: +1.7G (+7.79%)
• ✅ build/module/Mathlib.FieldTheory.Galois.Profinite//instructions: -2.5G (-3.60%)
• ✅ build/module/Mathlib.FieldTheory.IntermediateField.Algebraic//instructions: -3.8G (-8.37%)
• ✅ build/module/Mathlib.FieldTheory.RatFunc.IntermediateField//instructions: -2.9G (-5.42%)
• ✅ build/module/Mathlib.FieldTheory.Relrank//instructions: -5.4G (-5.32%)
• ✅ build/module/Mathlib.FieldTheory.SeparableClosure//instructions: -8.4G (-7.05%)
• ✅ build/module/Mathlib.NumberTheory.NumberField.CMField//instructions: -7.4G (-7.42%)
• ✅ build/module/Mathlib.NumberTheory.NumberField.Completion.InfinitePlace//instructions: -3.5G (-7.42%)

Small changes (25✅, 6🟥)

Too many entries to display here. View the full report on radar instead.

[JovanGerb]

That's a nice speedup, but it's worrying that there's also a slowdown.