diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean
index 33ec89f7be..f4a88fc621 100644
--- a/src/Lean/Elab/Tactic/Do/Spec.lean
+++ b/src/Lean/Elab/Tactic/Do/Spec.lean
@@ -199,7 +199,7 @@ public def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag
   let_expr f@Triple m ps instWP α prog P Q := specTy
     | liftMetaM <| throwError "target not a Triple application {specTy}"
   let wp' := mkApp5 (mkConst ``WP.wp f.constLevels!) m ps instWP α prog
-  unless (← withAssignableSyntheticOpaque <| isDefEqGuarded wp wp') do
+  unless (← isDefEqGuarded wp wp') do
     Term.throwTypeMismatchError none wp wp' spec
 
   -- Try synthesizing synthetic MVars. We don't have the convenience of `TermElabM`, hence
diff --git a/tests/lean/run/mspecNoAssignSyntheticOpaque.lean b/tests/lean/run/mspecNoAssignSyntheticOpaque.lean
new file mode 100644
index 0000000000..c0ce5b1b2c
--- /dev/null
+++ b/tests/lean/run/mspecNoAssignSyntheticOpaque.lean
@@ -0,0 +1,17 @@
+import Lean
+
+open Std.Do
+
+set_option mvcgen.warning false
+
+theorem set_spec : ⦃⌜True⌝⦄ set (m := StateM Nat) 42 ⦃⇓_ s => ⌜s = 42⌝⦄ := by
+  mvcgen
+
+example : True := by
+  have : ⦃⌜True⌝⦄ set (m := StateM Nat) (?n : Nat) ⦃⇓_ s => ⌜s = 42⌝⦄ := by
+    -- apply set_spec -- this fails, so `mspec` below should fail, too
+    mintro _
+    fail_if_success mspec set_spec
+    have : ?n = 42 := by rfl
+    mspec set_spec
+  trivial