fix: use infer type config when checking types at metavariable assign…

…ment

This PR fixes an issue at `isDefEq`. We must use the liberal infer
type `MetaM` config when checking types at the assignment `?m := v`.

src/Lean/Meta/ExprDefEq.lean

@@ -381,7 +381,7 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
       let vType ← inferType v
-      if (← withTransparency TransparencyMode.default <| Meta.isExprDefEqAux mvarType vType) then
+      if (← withAtLeastTransparency .default <| withInferTypeConfig <| Meta.isExprDefEqAux mvarType vType) then
         mvar.mvarId!.assign v
         pure true
       else