fix: remove transparency bumps from assignOutParams and checkTypesAndAssign

Remove the `withDefault` from `assignOutParams` in TC synthesis (the
change from #12488), and also guard the `withInferTypeConfig` transparency
bump in `checkTypesAndAssign` on `backward.isDefEq.respectTransparency`,
matching the pattern used for `isDefEqArgs` and `withProofIrrelTransparency`.

The `checkTypesAndAssign` bump was causing `tryResolve` to accept
instance candidates at `.default` transparency that `assignOutParams`
would later reject at `.instances` transparency, with no backtracking.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Meta/ExprDefEq.lean

@@ -413,14 +413,17 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
     else
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
-      -- **TODO**: avoid transparency bump. Let's fix other issues first
-      withInferTypeConfig do
+      let check := do
         let vType ← inferType v
         if (← Meta.isExprDefEqAux mvarType vType) then
           mvar.mvarId!.assign v
           pure true
         else
           pure false
+      if backward.isDefEq.respectTransparency.get (← getOptions) then
+        check
+      else
+        withInferTypeConfig check
 
 /--
 Auxiliary method for solving constraints of the form `?m xs := v`.

src/Lean/Meta/SynthInstance.lean

@@ -785,18 +785,8 @@ private def assignOutParams (type : Expr) (result : Expr) : MetaM Bool := do
   Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
   We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
   TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`.
-
-  **Note**: We tried to remove `withDefault` at the following `isDefEq` because it was a potential performance footgun. TC is supposed to unfold only `reducible` definitions and `instances`.
-  We reverted the change because it triggered thousands of failures related to the `OrderDual` type. Example:
-  ```
-  variable {ι : Type}
-  def OrderDual (α : Type) : Type := α
-  instance [I : DecidableEq ι] : DecidableEq (OrderDual ι) := inferInstance -- Failure
-  ```
-  Mathlib developers are currently trying to refactor the `OrderDual` declaration,
-  but it will take time. We will try to remove the `withDefault` again after the refactoring.
   -/
-  let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType
+  let defEq ← withAssignableSyntheticOpaque <| isDefEq type resultType
   unless defEq do
     trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
   return defEq