fix: don't error in defeq for missing unification hints

[Rob23oba]

This PR fixes the handling of unification hints to not fail with an "unknown constant" error if the unification hint is not available in the current environment. This happens mostly when the unification hint is only imported privately but we are in a public context.

Closes #14734

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-08 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-10 12:42:13)

[TwoFX]

This needs a test :)

[Rob23oba]

Here you go :-)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14733 has successfully built against this PR. (2026-08-10 13:35:41) View Log
• ✅ Mathlib branch lean-pr-testing-14733 has successfully built against this PR. (2026-08-10 14:47:33) View Log

[Rob23oba]

By the way, I would consider this one low priority, since I'm not blocked by this anymore. But I'd also like to mention that it seems to be a larger issue that also affects e.g. simp:

public def abc := 3

@[local simp]
theorem abc_eq : abc = 3 := (rfl)

@[expose]
public def hello (x : Fin 3) : Fin abc := by simp -- error: unknown constant `abc_eq`

Maybe you can discuss this in the FRO some time though (i.e. what's the right thing to do for environment extensions like this under the module system?)