feat: withAssignableSyntheticOpaque in assumption (#2596)

* feat: withAssignableSyntheticOpaque in assumption
* add test

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -232,7 +232,10 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
   | some msg => withRef stx[0] <| addRawTrace msg
 
 @[builtin_tactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic := fun _ =>
-  liftMetaTactic fun mvarId => do mvarId.assumption; pure []
+  -- The `withAssignableSyntheticOpaque` is needed here to accommodate
+  -- `assumption` after `refine`.
+  -- See https://github.com/leanprover/lean4/issues/2361
+  liftMetaTactic fun mvarId => withAssignableSyntheticOpaque do mvarId.assumption; pure []
 
 @[builtin_tactic Lean.Parser.Tactic.contradiction] def evalContradiction : Tactic := fun _ =>
   liftMetaTactic fun mvarId => do mvarId.contradiction; pure []

tests/lean/2361.lean

@@ -0,0 +1,16 @@
+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