fix: have simpa ... using ... do exact-like checks

[kmill]

Closes #5634. Before assigning the simplified using clause expression to the goal, this adds a check that the expression has no new metavariables. It also adjusts how new hypotheses are added to the goal to prevent spurious "don't know how to synthesize placeholder" errors on that goal metavariable. We also throw in an occurs check immediately after elaboration to avoid some counterintuitive behavior when simplifying such a term closes the goal.

Closes #4101. This also improves the type mismatch error message, showing the elaborated using clause rather than h✝:

example : False := by
  simpa using (fun x : True => x)
/-
error: type mismatch, term
  fun x => x
after simplification has type
  True : Prop
but is expected to have type
  False : Prop
-/

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5648 build failed against this PR. (2024-10-08 07:20:46) View Log
• 💥 Mathlib branch lean-pr-testing-5648 build failed against this PR. (2024-10-08 08:21:22) View Log
• 💥 Mathlib branch lean-pr-testing-5648 build failed against this PR. (2024-10-08 19:24:24) View Log
• 💥 Mathlib branch lean-pr-testing-5648 build failed against this PR. (2024-10-08 19:55:45) View Log
• ✅ Mathlib branch lean-pr-testing-5648 has successfully built against this PR. (2024-10-08 22:51:15) View Log
• ✅ Mathlib branch lean-pr-testing-5648 has successfully built against this PR. (2024-10-09 00:12:46) View Log