diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 86968ee1d3..3583f812f0 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -497,11 +497,24 @@ fun stx => do
     logInfo stx.val (e ++ " : " ++ type);
     pure ()
 
+@[builtinCommandElab «synth»] def elabSynth : CommandElab :=
+fun stx => do
+  let ref  := stx.val;
+  let term := stx.getArg 1;
+  runTermElabM `_synth_cmd $ fun _ => do
+    inst ← Term.elabTerm term none;
+    Term.synthesizeSyntheticMVars false;
+    inst ← Term.instantiateMVars ref inst;
+    val  ← Term.liftMetaM ref $ Meta.synthInstance inst;
+    logInfo stx.val val;
+    pure ()
+
 def setOption (ref : Syntax) (optionName : Name) (val : DataValue) : CommandElabM Unit := do
 decl ← liftIO ref $ getOptionDecl optionName;
 unless (decl.defValue.sameCtor val) $ throwError ref "type mismatch at set_option";
 modifyScope $ fun scope => { opts := scope.opts.insert optionName val, .. scope }
 
+
 @[builtinCommandElab «set_option»] def elabSetOption : CommandElab :=
 fun stx => do
   let ref        := stx.val;
diff --git a/tests/lean/run/typeclass_easy.lean b/tests/lean/run/typeclass_easy.lean
new file mode 100644
index 0000000000..93472317fa
--- /dev/null
+++ b/tests/lean/run/typeclass_easy.lean
@@ -0,0 +1,12 @@
+new_frontend
+set_option ppOld false
+
+#synth HasToString (Nat × (Nat × Bool))
+
+#synth HasAdd Nat
+
+#synth HasCoe Bool Prop
+
+#synth Decidable (True ∧ 1 = 1)
+
+#synth DecidableEq (Nat × Nat)