fix: rw ... at h unknown fvar bug

[thorimur]

• Put an X in this bracket to confirm you have read the
  External Contribution Guidelines.

Second half of fixing #2711. Simply moves replaceLocalDecl outside of Term.withSynthesize, but does not fix the general issues mentioned in #2727.

---

This was benched on mathlib against nightly testing here. Note: this is actually a couple of commits off the baseline, which likely account for a couple things getting faster.

To find the relevant mathlib4 branches on speedcenter manually, search "2712" and compare the branch bench-nightly-testing-for-2712 (baseline of #2712, which this PR depends on) to lean-pr-testing-2728.

Note: it took a while to get mathlib and std synced up to the current lean changes; the mathlib build failures were unrelated to this PR. This PR doesn't require any changes to mathlib or std.

---

• depends on: fix: add instantiateMVars to replaceLocalDecl #2712

[leanprover-community-mathlib4-bot]

• 💥 Mathlib branch lean-pr-testing-2728 build failed against this PR. (2023-10-21 09:17:07) View Log
• 💥 Mathlib branch lean-pr-testing-2728 build failed against this PR. (2023-10-21 20:00:25) View Log
• ❌ Mathlib branch lean-pr-testing-2728 built against this PR, but testing failed. (2023-10-22 09:18:20) View Log
• 💥 Mathlib branch lean-pr-testing-2728 build failed against this PR. (2023-10-22 09:43:27) View Log
• ✅ Mathlib branch lean-pr-testing-2728 has successfully built against this PR. (2023-10-22 10:59:58) View Log
• ✅ Mathlib branch lean-pr-testing-2728 has successfully built against this PR. (2023-10-23 04:06:50) View Log
• 💥 Mathlib branch lean-pr-testing-2728 build failed against this PR. (2023-10-25 00:18:00) View Log

[thorimur]

awaiting-review