fix: out of scope let-variable can appear in fun binder type of metav…

[JovanGerb]

This PR fixes a bug in checkAsssignment.

When unification tries to solve ?m a₁ ... aₙ =?= v by assigning ?m := fun a₁ ... aₙ => v, a number of things needs to be checked.

1. occurs check, that is, check that ?m doesn't appear in the assignment
2. check that the free variables in the assignment are present in the local context of ?m. If a let-varaible isn't in the local context, then this can be resolved by instantiating it with its definition.
3. check that the metavariables in the assignment have local contexts that are at most as large as the local context of ?m. If a metavariable has a local context with extra free variables, this can be resolved by assigning it to a new fresh metavariable with a restricted local context.

Previously, checkAssignment does checks 1-3 on v, and does check 1 on the types of a₁ ... aₙ and on the type of v.

However, as reported in #5939, checks 2-3 also need to be executed on the types of a₁ ... aₙ, because these types appear as lambda binder types in ?m := fun a₁ ... aₙ => v.

This PR fixes checkAssignment: besides returning an updated v, it now also returns an updated LocalContext. This LocalContext is then used in mkLambdaFVars in order to obtain the correct lambda binder types.

In order to also fix #5387, I modified the function Lean.Meta.CheckAssignment.checkMVar, so that it can use the checked types of a₁ ... aₙ, which makes it so that it can avoid removing some of a₁ ... aₙ from the context of the metavariable that is being reduced.

This PR also removes the function mkLambdaFVarsWithLetDeps. This function was introduced as a fix for a bug that is independently fixed by this fix. Additionally, mkLambdaFVarsWithLetDeps gives surprising behaviour in that it creates let-binders for let-variables that would normally just be instantiated (see check 2). Additionally, mkLambdaFVarsWithLetDeps has a faulty implementation, because it assumes the free variables appear in the same order as they appear in the local context, which may not be true (see this comment).

I added the tests to the file that contains the original test for mkLambdaFVarsWithLetDeps

Closes #5939
Closes #5387

[Kha]

We cannot accept such an invasive change to a core component, please consider contributing to less critical parts first!

[JovanGerb]

Ok, I hope this at least helped with understanding what the problem is and how it can be fixed.