diff --git a/tests/lean/run/1692.lean b/tests/lean/run/1692.lean
new file mode 100644
index 0000000000..f8eaa2732e
--- /dev/null
+++ b/tests/lean/run/1692.lean
@@ -0,0 +1,21 @@
+import Lean.Hygiene
+
+def otherInhabited : Inhabited Nat := ⟨42⟩
+
+def f := Id.run do
+  let ⟨n⟩ ← pure otherInhabited
+  -- do-notation expands to `pure otherInhabited >>= fun x : Inhabited Nat => ...`
+  -- the `x : Inhabited Nat` should not be available for TC synth (i.e., `default` should be 0)
+  return default + n
+
+example : f = 42 := rfl
+
+open Lean
+def g : Syntax :=
+  let rec stx : Syntax := Unhygienic.run `(f 0 1)
+  let stx := stx
+  match stx with
+  | `(f $_args*) => ‹Syntax› -- should not resolve to tmp var created by stx matcher
+  | _ => default
+
+example : g = g.stx := rfl