perf: skip preprocessOutParam for noMVars queries

This reverts part of the `OrderDual` workaround from #12286.

The `preprocessOutParam` step is morally not needed when the type has
no metavariables, because output params should be uniquely determined
by the input params. The optimization was removed because
semireducible type aliases like `OrderDual` caused TC resolution to
fail (e.g. `FunLike F (OrderDual α) (OrderDual β)` where the last
two arguments are output parameters — without `preprocessOutParam`,
TC resolution fails because it cannot unfold `OrderDual`).

This is an experimental branch for testing whether Mathlib's
`OrderDual` refactoring has progressed enough to restore this
optimization.

src/Lean/Meta/SynthInstance.lean

@@ -893,28 +893,7 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
       trace[Meta.synthInstance.cache] "new: {type}"
       let abstResult? ← withNewMCtxDepth (allowLevelAssignments := true) do
         match kind with
-        | .noMVars =>
-          /-
-          **Note**: The expensive `preprocessOutParam` step is morally **not** needed here because
-          the output params should be uniquely determined by the input params. During type class
-          resolution, definitional equality only unfolds `[reducible]` and `[instance_reducible]`
-          declarations. This is a contract with our users to ensure performance is reasonable.
-          However, the same `OrderDual` declaration that creates problems for `assignOutParams`
-          also prevents us from using this optimization. As an example, suppose we are trying to
-          synthesize
-          ```
-          FunLike F (OrderDual α) (OrderDual β)
-          ```
-          where the last two arguments of `FunLike` are output parameters. This term has no
-          metavariables, and it seems natural to skip `preprocessOutParam`, which would replace
-          the last two arguments with metavariables. However, if we don't replace them,
-          TC resolution fails because it cannot unfold `OrderDual` since it is semireducible.
-
-          **Note**: We should remove `preprocessOutParam` from the following line as soon as
-          Mathlib refactors `OrderDual`.
-          -/
-          SynthInstance.main (← preprocessOutParam type) maxResultSize
-        | .mvarsNoOutputParams => SynthInstance.main type maxResultSize
+        | .noMVars | .mvarsNoOutputParams => SynthInstance.main type maxResultSize
         | .mvarsOutputParams => SynthInstance.main (← preprocessOutParam type) maxResultSize
       let result? ← applyAbstractResult? type abstResult?
       trace[Meta.synthInstance] "result {result?}"