diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 07e03fe4e..d579842f9 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -318,7 +318,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     if (!found_cached) {
         if (is_theorem) {
             auto type_pos = p.pos_of(type);
-            std::tie(type, new_ls) = p.elaborate_type(type);
+            bool clear_pre_info = false; // we don't want to clear pre_info data until we process the proof.
+            std::tie(type, new_ls) = p.elaborate_type(type, list<expr>(), clear_pre_info);
             check_no_metavar(env, real_n, type, true);
             ls = append(ls, new_ls);
             expr type_as_is = p.save_pos(mk_as_is(type), type_pos);
diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index bb484be9e..c355206f2 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -386,9 +386,8 @@ struct info_manager::imp {
             synch_line(i);
             if (!overwrite && m_line_valid[i])
                 continue;
-            unsigned range = m_line_data[i].empty() ? 0 : m_line_data[i].max()->get_column() + 1;
             s.for_each([&](info_data const & d) {
-                    if (overwrite || d.get_column() >= range)
+                    if (overwrite || !m_line_data[i].contains(d))
                         m_line_data[i].insert(d);
                 });
         }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 329114d36..9152fc87a 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -569,14 +569,15 @@ std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, li
     return r;
 }
 
-std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> const & ctx) {
+std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> const & ctx, bool clear_pre_info) {
     bool relax            = false;
     bool check_unassigned = true;
     bool ensure_type      = true;
     parser_pos_provider pp = get_pos_provider();
     elaborator_context env = mk_elaborator_context(pp, check_unassigned);
     auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
-    m_pre_info_manager.clear();
+    if (clear_pre_info)
+        m_pre_info_manager.clear();
     return r;
 }
 
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 30a124312..7c3157ae6 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -324,7 +324,7 @@ public:
     /** \brief Elaborate \c e, and tolerate metavariables in the result. */
     std::tuple<expr, level_param_names> elaborate_relaxed(expr const & e, list<expr> const & ctx = list<expr>());
     /** \brief Elaborate \c e, and ensure it is a type. */
-    std::tuple<expr, level_param_names> elaborate_type(expr const & e, list<expr> const & ctx = list<expr>());
+    std::tuple<expr, level_param_names> elaborate_type(expr const & e, list<expr> const & ctx = list<expr>(), bool clear_pre_info = true);
     /** \brief Elaborate \c e in the given environment. */
     std::tuple<expr, level_param_names> elaborate_at(environment const & env, expr const & e);
     /** \brief Elaborate \c e (making sure the result does not have metavariables). */