feat(Tactic): add inferInstanceAs% to fix type leakage

[kim-em]

This PR adds inferInstanceAs%, a drop-in replacement for inferInstanceAs that prevents "type leakage" in synthesized instances.

When inferInstanceAs (SomeClass A) is used to define SomeClass B (where B is a non-reducible alias for A), the synthesized instance may contain lambda binder domains (and other sub-expressions) referring to A or deeper unfoldings instead of B. This is invisible at default transparency but causes isDefEq failures at reducibleAndInstances transparency — which is the level used by grind's checkInst.

inferInstanceAs% fixes this by recursively normalizing the constructor tree: it WHNFs to expose the constructor, patches carrier type parameters via isDefEq matching against the unfolding chain, recursively processes instance-implicit fields, and replaces lambda binder domains in function fields.

As a demonstration, this fixes the grind failure in FiniteResidueField that was worked around with #adaptation_note and a manual proof on nightly-testing.

🤖 Prepared with Claude Code

[github-actions]

PR summary ba37a5c6ee

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
3 files Mathlib.Algebra.Order.Ring.StandardPart Mathlib.Analysis.Real.Hyperreal Mathlib.Tactic	1
Mathlib.Tactic.InferInstanceAsPercent (new file)	50

---

Declarations diff

+ B
+ MyInv
+ MyNat
+ TestDivInvMonoid
+ TestField
+ TestInv
+ TestNat
+ addUnfoldings
+ buildReplacements
+ getCtorApp?
+ getFieldInfo
+ instance : Field (FiniteResidueField K)
+ instance : MyInv Nat
+ instance : SomeClass B := inferInstanceAs (SomeClass A)
+ instance : TestField Nat
+ matchesAnyDefeq
+ myNatInv_fixed
+ myNatInv_leaky
+ replaceCarriersInType
+ testField_direct
+ testField_fixed
+ testField_fixed'
+ testField_leaky
+ unfoldChain

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.

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.01)

Current number	Change	Type
132	-1	adaptation notes

Current commit 4c91a86a72
Reference commit ba37a5c6ee

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).

[astrainfinita]

Should we make an elaborator for normalizeInstance? This would also be a better version of #13795.

[JovanGerb]

I've left some small comments, but I do have one high level criticism. This function will unfold the instance all the way down to its constructors when possible. For some instances this will give some very big terms. It is typically better to use pre-existing instances of sub-structures in place of those sub-structures. This is also what fast_instance% does. So I can imagine that we will see some slowdowns as a result of this.

[astrainfinita]

So I can imagine that we will see some slowdowns as a result of this.

Using fast_instance% and normalizeInstance appropriately can provide further acceleration (see my PR above) rather than a slowdown. You can always use fast_instance% after normalizeInstance.

[JovanGerb]

You're right, and we can use fast_instance% after inferInstanceAs%

[kim-em]

I've left some small comments, but I do have one high level criticism. This function will unfold the instance all the way down to its constructors when possible. For some instances this will give some very big terms. It is typically better to use pre-existing instances of sub-structures in place of those sub-structures. This is also what fast_instance% does. So I can imagine that we will see some slowdowns as a result of this.

I've changed behaviour: when we hit sub-structures, we try to decide if they are "leaky". If so, we emit a (suppresible) warning, hopefully encouraging the user to go fix those first.