fix: reuse the instances of a non-exposed definition in inferInstanceAs

[gasparattila]

This PR makes inferInstanceAs reuse the existing instances of a non-exposed definition. This is done by checking the reusability of an instance in the private scope, as neither the auxiliary definitions being generated nor the ones in the existing instance are exposed in this case.

Closes #14470.

[gasparattila]

changelog-language

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b80e8491105a1bcc679136b8b583ee7896b24a78 --onto dec70ee4980b571229f784a33d72b421ede3b1d5. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-19 10:51:57)
• ✅ Mathlib branch lean-pr-testing-14840 has successfully built against this PR. (2026-08-19 12:22:36) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b80e8491105a1bcc679136b8b583ee7896b24a78 --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force reference manual CI using the force-manual-ci label. (2026-08-19 10:51:59)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-18 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-19 11:29:34)