diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 81fd072570..9920bc0a81 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -217,20 +217,27 @@ void elaborator::copy_info_to_manager(substitution s) {
     m_pre_info_data.clear();
 }
 
+optional<name> elaborator::mk_mvar_suffix(expr const & b) {
+    if (!infom())
+        return optional<name>();
+    else
+        return optional<name>(binding_name(b));
+}
+
 /** \brief Create a metavariable, and attach choice constraint for generating
     solutions using class-instances and tactic-hints.
 */
-expr elaborator::mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict,
-                                     bool is_inst_implicit, constraint_seq & cs) {
+expr elaborator::mk_placeholder_meta(optional<name> const & suffix, optional<expr> const & type,
+                                     tag g, bool is_strict, bool is_inst_implicit, constraint_seq & cs) {
     if (is_inst_implicit) {
         auto ec = mk_placeholder_elaborator(env(), ios(), m_context,
-                                            m_ngen.next(), m_relax_main_opaque, use_local_instances(),
+                                            m_ngen.next(), suffix, m_relax_main_opaque, use_local_instances(),
                                             is_strict, type, g, m_unifier_config);
         register_meta(ec.first);
         cs += ec.second;
         return ec.first;
     } else {
-        expr m = m_context.mk_meta(m_ngen, type, g);
+        expr m = m_context.mk_meta(m_ngen, suffix, type, g);
         register_meta(m);
         return m;
     }
@@ -323,7 +330,8 @@ expr elaborator::add_implict_args(expr e, constraint_seq & cs, bool relax) {
         tag g = e.get_tag();
         bool is_strict = true;
         bool inst_imp  = binding_info(type).is_inst_implicit();
-        expr imp_arg   = mk_placeholder_meta(some_expr(binding_domain(type)), g, is_strict, inst_imp, cs);
+        expr imp_arg   = mk_placeholder_meta(mk_mvar_suffix(type), some_expr(binding_domain(type)),
+                                             g, is_strict, inst_imp, cs);
         e              = mk_app(e, imp_arg, g);
         type           = instantiate(binding_body(type), imp_arg);
         constraint_seq new_cs;
@@ -553,7 +561,8 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
             tag g          = f.get_tag();
             bool is_strict = true;
             bool inst_imp  = binding_info(f_type).is_inst_implicit();
-            expr imp_arg   = mk_placeholder_meta(some_expr(binding_domain(f_type)), g, is_strict, inst_imp, f_cs);
+            expr imp_arg   = mk_placeholder_meta(mk_mvar_suffix(f_type), some_expr(binding_domain(f_type)),
+                                                 g, is_strict, inst_imp, f_cs);
             f              = mk_app(f, imp_arg, g);
             auto f_t       = ensure_fun(f, f_cs);
             f              = f_t.first;
@@ -871,7 +880,8 @@ pair<expr, constraint_seq> elaborator::visit(expr const & e) {
                 }
             }
             bool inst_imp = bi.is_inst_implicit();
-            imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, inst_imp, cs);
+            imp_arg = mk_placeholder_meta(mk_mvar_suffix(r_type), some_expr(binding_domain(r_type)),
+                                          g, is_strict, inst_imp, cs);
             r       = mk_app(r, imp_arg, g);
             r_type  = whnf(instantiate(binding_body(r_type), imp_arg), cs);
         }
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index fbbc2fe57e..2efd4ce8bb 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -87,7 +87,13 @@ class elaborator : public coercion_info_manager {
     virtual void save_coercion_info(expr const & e, expr const & c);
     virtual void erase_coercion_info(expr const & e);
     void copy_info_to_manager(substitution s);
-    expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, bool inst_implicit, constraint_seq & cs);
+    /** \brief If info manager is being used, then create a metavariable suffix based on binding_name(b) */
+    optional<name> mk_mvar_suffix(expr const & b);
+    expr mk_placeholder_meta(optional<name> const & suffix, optional<expr> const & type,
+                             tag g, bool is_strict, bool inst_implicit, constraint_seq & cs);
+    expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, bool inst_implicit, constraint_seq & cs) {
+        return mk_placeholder_meta(optional<name>(), type, g, is_strict, inst_implicit, cs);
+    }
 
     expr visit_expecting_type(expr const & e, constraint_seq & cs);
     expr visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs);
diff --git a/src/frontends/lean/local_context.cpp b/src/frontends/lean/local_context.cpp
index 6b675acbc9..3703543cea 100644
--- a/src/frontends/lean/local_context.cpp
+++ b/src/frontends/lean/local_context.cpp
@@ -81,15 +81,17 @@ expr local_context::mk_type_meta(name_generator & ngen, tag g) {
     return apply_context(mk_type_metavar(ngen, g), g);
 }
 
-expr local_context::mk_metavar(name_generator & ngen, optional<expr> const & type, tag g) {
+expr local_context::mk_metavar(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g) {
     name n      = ngen.next();
+    if (suffix)
+        n = n + *suffix;
     expr r_type = type ? *type : mk_type_meta(ngen, g);
     expr t      = pi_abstract_context(r_type, g);
     return ::lean::mk_metavar(n, t, g);
 }
 
-expr local_context::mk_meta(name_generator & ngen, optional<expr> const & type, tag g) {
-    expr mvar = mk_metavar(ngen, type, g);
+expr local_context::mk_meta(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g) {
+    expr mvar = mk_metavar(ngen, suffix, type, g);
     expr meta = apply_context(mvar, g);
     return meta;
 }
diff --git a/src/frontends/lean/local_context.h b/src/frontends/lean/local_context.h
index 7257b5e8dc..14a17657d9 100644
--- a/src/frontends/lean/local_context.h
+++ b/src/frontends/lean/local_context.h
@@ -61,8 +61,10 @@ public:
         where ?m2 is another fresh metavariable with type
            <tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u})</tt>,
         and \c ?u is a fresh universe metavariable.
+
+        \remark If \c suffix is not none, then it is appended to the (fresh) metavariable name.
     */
-    expr mk_metavar(name_generator & ngen, optional<expr> const & type, tag g);
+    expr mk_metavar(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g);
 
     /** \brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
            <tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
@@ -70,8 +72,13 @@ public:
         created using \c mk_metavar.
 
         \see mk_metavar
+
+        \remark If \c suffix is not none, then it is appended to the (fresh) metavariable name.
     */
-    expr mk_meta(name_generator & ngen, optional<expr> const & type, tag g);
+    expr mk_meta(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g);
+    expr mk_meta(name_generator & ngen, optional<expr> const & type, tag g) {
+        return mk_meta(ngen, optional<name>(), type, g);
+    }
 
     /** \brief Return context as a list */
     list<expr> const & get_data() const;
diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp
index 73cdef5941..36c131315b 100644
--- a/src/frontends/lean/placeholder_elaborator.cpp
+++ b/src/frontends/lean/placeholder_elaborator.cpp
@@ -268,10 +268,10 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
 */
 pair<expr, constraint> mk_placeholder_elaborator(
     environment const & env, io_state const & ios, local_context const & ctx,
-    name const & prefix, bool relax, bool use_local_instances,
+    name const & prefix, optional<name> const & suffix, bool relax, bool use_local_instances,
     bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg) {
     auto C       = std::make_shared<placeholder_context>(env, ios, ctx, prefix, relax, use_local_instances);
-    expr m       = C->m_ctx.mk_meta(C->m_ngen, type, g);
+    expr m       = C->m_ctx.mk_meta(C->m_ngen, suffix, type, g);
     constraint c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, delay_factor());
     return mk_pair(m, c);
 }
diff --git a/src/frontends/lean/placeholder_elaborator.h b/src/frontends/lean/placeholder_elaborator.h
index 63eb9dbe08..7647110681 100644
--- a/src/frontends/lean/placeholder_elaborator.h
+++ b/src/frontends/lean/placeholder_elaborator.h
@@ -15,6 +15,7 @@ namespace lean {
 
     \param ctx Local context where placeholder is located
     \param prefix Prefix for metavariables that will be created by this procedure
+    \param suffix If provided, then it is added to the main metavariable created by this procedure.
     \param relax True if opaque constants in the current module should be treated
                  as transparent
     \param use_local_instances If instances in the local context should be used
@@ -26,6 +27,6 @@ namespace lean {
 */
 pair<expr, constraint> mk_placeholder_elaborator(
     environment const & env, io_state const & ios, local_context const & ctx,
-    name const & prefix, bool relax_opaque, bool use_local_instances,
+    name const & prefix, optional<name> const & suffix, bool relax_opaque, bool use_local_instances,
     bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg);
 }
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 8c5cf6ce48..a69a8467ec 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -96,13 +96,55 @@ void finalize_pp() {
     delete g_tmp_prefix;
 }
 
+/** \brief We assume a metavariable name has a suggestion embedded in it WHEN its
+    last component is a string. */
+static bool has_embedded_suggestion(name const & m) {
+    return m.is_string();
+}
+
+/** \see extract_suggestion */
+static name extract_suggestion_core(name const & m) {
+    if (m.is_string()) {
+        if (m.is_atomic())
+            return m;
+        else
+            return name(extract_suggestion_core(m.get_prefix()), m.get_string());
+    } else {
+        return name();
+    }
+}
+
+/** \brief Extract "suggested name" embedded in a metavariable name
+
+    \pre has_embedded_suggestion(m)
+*/
+static name extract_suggestion(name const & m) {
+    lean_assert(has_embedded_suggestion(m));
+    name r = extract_suggestion_core(m);
+    lean_assert(!r.is_anonymous());
+    return r;
+}
+
 name pretty_fn::mk_metavar_name(name const & m) {
     if (auto it = m_purify_meta_table.find(m))
         return *it;
-    name new_m = m_meta_prefix.append_after(m_next_meta_idx);
-    m_next_meta_idx++;
-    m_purify_meta_table.insert(m, new_m);
-    return new_m;
+    if (has_embedded_suggestion(m)) {
+        name suggested = extract_suggestion(m);
+        name r         = suggested;
+        unsigned i     = 1;
+        while (m_purify_used_metas.contains(r)) {
+            r = suggested.append_after(i);
+            i++;
+        }
+        m_purify_used_metas.insert(r);
+        m_purify_meta_table.insert(m, r);
+        return r;
+    } else {
+        name new_m = m_meta_prefix.append_after(m_next_meta_idx);
+        m_next_meta_idx++;
+        m_purify_meta_table.insert(m, new_m);
+        return new_m;
+    }
 }
 
 name pretty_fn::mk_local_name(name const & n, name const & suggested) {
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index d48bf98310..3e6970ca6e 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -44,6 +44,7 @@ private:
     name                m_meta_prefix;
     unsigned            m_next_meta_idx;
     name_map<name>      m_purify_meta_table;
+    name_set            m_purify_used_metas;
     name_map<name>      m_purify_local_table;
     name_set            m_purify_used_locals;
     // cached configuration
diff --git a/tests/lean/interactive/info.input.expected.out b/tests/lean/interactive/info.input.expected.out
index c206adaf23..1940d45805 100644
--- a/tests/lean/interactive/info.input.expected.out
+++ b/tests/lean/interactive/info.input.expected.out
@@ -2,7 +2,7 @@
 -- ENDWAIT
 -- BEGININFO
 -- TYPE|6|8
-?M_1 → ?M_2 → ?M_1 ∧ ?M_2
+?a → ?b → ?a ∧ ?b
 -- ACK
 -- IDENTIFIER|6|8
 and.intro