`isDefEq` does not always assign goals

The documentation on assign says:

/--
Add `mvarId := x` to the metavariable assignment.
This method does not check whether `mvarId` is already assigned, nor it checks whether
a cycle is being introduced, or whether the expression has the right type.
This is a low-level API, and it is safer to use `isDefEq (mkMVar mvarId) x`.
-/
def _root_.Lean.MVarId.assign [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit :=

However the suggested pattern isDefEq (mkMVar mvarId) x does not assign mvarId if the type of mvarId is a proposition. This is the source of several bugs in mathlib tactics, and at least one bug in core:

import Lean
open Lean Elab Tactic

elab "my_infer_instance" : tactic => do
  (← getMainGoal).inferInstance
  replaceMainGoal []

class Foo : Prop
instance : Foo := sorry
example : Foo := by my_infer_instance
-- (kernel) declaration has metavariables '_example'

This is because inferInstance doesn't actually assign the mvar:

def _root_.Lean.MVarId.inferInstance (mvarId : MVarId) : MetaM Unit := mvarId.withContext do
  mvarId.checkNotAssigned `infer_instance
  let synthVal ← synthInstance (← mvarId.getType)
  unless (← isDefEq (mkMVar mvarId) synthVal) do
    throwTacticEx `infer_instance mvarId "`infer_instance` tactic failed to assign instance"

The current workaround is to do isDefEq first and then call mvarId.assign val afterward. It would probably be good to have an API function for this (and point users to it in MVarId.assign).

Start with Lean.MVarId.assign, MVarId.inferInstance, and the isDefEq call shown in the issue. Trace how proposition-typed metavariables are handled, then define or document an API that reliably assigns them and update the guidance in MVarId.assign; verify the example no longer leaves declaration metavariables.