diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 3cfbf8d6c..14203591a 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -708,6 +708,8 @@ public:
             return visit(get_annotation_arg(e), cs);
         } else if (is_typed_expr(e)) {
             return visit_typed_expr(e, cs);
+        } else if (is_implicit(e)) {
+            return visit_core(get_implicit_arg(e), cs);
         } else {
             switch (e.kind()) {
             case expr_kind::Local:      return e;