fix: populate local instances during pretty printing

[thorimur]

Experimental. This PR populates local instances during delaboration.

Closes #10830.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-17 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. (2025-10-18 05:29:17)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 11e4e44be070ec99bc734e40f8431fd92725842d --onto 0f866236c7c2e77e8d12ff61d08ef48694a0cbfb. You can force reference manual CI using the force-manual-ci label. (2026-01-07 00:26:14)

[thorimur]

!bench

[leanprover-radar]

Benchmark results for aad65be against 4ce7ad1 are in! @thorimur

[leanprover-bot]

Here are the benchmark results for commit aad65be.
There were significant changes against commit 4ce7ad1:

  Benchmark      Metric           Change
  ================================================
+ channel.lean   boundedn_seq      -1.1%
+ stdlib         congr simp thm    -1.6% (-39.8 σ)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-10832 has successfully built against this PR. (2025-10-18 06:26:46) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 11e4e44be070ec99bc734e40f8431fd92725842d --onto 0f866236c7c2e77e8d12ff61d08ef48694a0cbfb. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-07 00:26:12)