[Merged by Bors] - fix(ClickSuggestions): instantiate all metavariables in the local context

[JovanGerb]

This PR fixes the panic in #click_suggestions that was reported at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.23click_suggestions.20doesn.27t.20find.20lemma/near/606231763

There are two separate problems that this PR fixes:

1. The implementation of #click_suggestion assumes all metavariables have already been instantiated. This is valid because they are all instantiated at the very beginning. However, this was not done properly, causing the types of free variables to still be able to contain metavariables.
2. The function viewKAbstractSubExpr was able to reach its unreachable! block. The reason is that kabstractPositions calls instantiateMVars on the expression e but not on the pattern p, causing a discrepancy. This is fixed by removing the instantiateMVars call. This is fine, because in both of the use cases (rw?? and #click_suggestions), the expressions already have instantiated metavariables at this point.

---

[github-actions]

PR summary 85fabd70e2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 85fabd7).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 85fabd70e2
Reference commit 9e46613652

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

[joneugster]

maintainer delegate (my bad, didn't read the PR description carefully)

maintainer merge

Thanks for the PR!

[github-actions]

🚀 Pull request has been placed on the maintainer queue by joneugster.

[fpvandoorn]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Test and lint
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job
• ci (staging) / Lint style