test: unfold reducible abbreviations in inline-elaborated invariant values (#13668)

This PR fixes an issue in the `mvcgen'` prototype where user-provided
invariant values were elaborated against a goal type containing
reducible abbreviations like `PostShape.args ps`, baking
`(PostShape.args PostShape.pure)` into the assignment instead of `[]`.

After `tryInlineInvariant` confirms the user tactic assigned the
invariant metavariable, reduce its assignment with `unfoldReducible`.
Fixes the `mvcgen'` migration path for several `tests/elab/*` proofs
that had been blocked on the entailment-phase apply failure.

Co-authored-by: Sebastian Graf <sg@lean-fro.org>

tests/bench/mvcgen/sym/lib/VCGen/Driver.lean

@@ -68,7 +68,15 @@ private meta def tryInlineInvariant (n : Nat) (mv : MVarId) : VCGenM Bool := do
     let _ ← Lean.Elab.runTactic mv tac {} {}
     -- The tactic runs without throwing even when it fails to close the goal;
     -- check explicitly that the MVar got assigned.
-    mv.isAssigned
+    if ← mv.isAssigned then
+      -- Preprocess the assignment to `mv` because it will interact with the `SymM` world
+      if let some val ← getExprMVarAssignment? mv then
+        let val ← unfoldReducible val
+        let val ← shareCommon val
+        mv.assign val
+      return true
+    else
+      return false
   catch _ =>
     return false