Missing withAssignableSyntheticOpaque for assumption tactic?

[kmill]

When you use refine in place of constructor, then the metavariables you get are all synthetic opaque. If you focus on a later goal, then you cannot use assumption to assign both the goal and a preceding metavariable since this causes it to fail the isDefEq check.

import Lean

example {α : Type} {P : α → Prop} (a : α) (h : P a) : ∃ x, P x := by
  constructor
  assumption -- succeeds

example {α : Type} {P : α → Prop} (a : α) (h : P a) : ∃ x, P x := by
  refine ⟨?m, ?c⟩
  case c =>
    /-
    α : Type
    P : α → Prop
    a : α
    h : P a
    ⊢ P ?m
    -/
    assumption -- fails

open Lean Elab Tactic Meta in
elab "assumption'" : tactic => do
  liftMetaTactic fun mvarId => withAssignableSyntheticOpaque do mvarId.assumption; pure []

example {α : Type} {P : α → Prop} (a : α) (h : P a) : ∃ x, P x := by
  refine ⟨?m, ?c⟩
  case c => assumption' -- succeeds

[kim-em]

@kmill, I made #2596 following this suggestion. Mathlib builds fine. Would you be interested in adding a few tests?