feat: withAssignableSyntheticOpaque in assumption

[kim-em]

• Put an X in this bracket to confirm you have read the
  External Contribution Guidelines.

• Fixes Missing withAssignableSyntheticOpaque for assumption tactic? #2361

[leanprover-community-mathlib4-bot]

• ✅ Mathlib branch lean-pr-testing-2596 has successfully built against this PR. (2023-09-27 06:13:37) View Log

[kmill]

I don't have permission to push to this branch, but here's a test for tests/lean/2361.lean:

import Lean

-- This worked before issue #2361
example {α : Type} {P : α → Prop} (a : α) (h : P a) : ∃ x, P x := by
  constructor
  assumption

example {α : Type} {P : α → Prop} (a : α) (h : P a) : ∃ x, P x := by
  refine ⟨?m, ?c⟩
  -- `?m` is synthetic opaque, so `assumption` needs to be able to assign such metavariables
  -- for this to succeed.
  case c => assumption

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