diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index c7ada36c15..83e4ad6891 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -179,8 +179,21 @@ environment end_scoped_cmd(parser & p) {
     }
 }
 
+/* Auxiliary class to setup private naming scope for transient commands such as #check/#reduce/#eval and run_cmd */
+class transient_cmd_scope {
+    environment            m_env;
+    private_name_scope     m_prv_scope;
+public:
+    transient_cmd_scope(parser & p):
+        m_env(p.env()),
+        m_prv_scope(true, m_env) {
+        p.set_env(m_env);
+    }
+};
+
 environment check_cmd(parser & p) {
     expr e; level_param_names ls;
+    transient_cmd_scope cmd_scope(p);
     std::tie(e, ls) = parse_local_expr(p, "_check");
     type_checker tc(p.env(), true, false);
     expr type = tc.check(e, ls);
@@ -200,6 +213,7 @@ environment check_cmd(parser & p) {
 }
 
 environment reduce_cmd(parser & p) {
+    transient_cmd_scope cmd_scope(p);
     bool whnf   = false;
     if (p.curr_is_token(get_whnf_tk())) {
         p.next();
@@ -401,6 +415,7 @@ static expr convert_metavars(metavar_context & ctx, expr const & e) {
 }
 
 static environment unify_cmd(parser & p) {
+    transient_cmd_scope cmd_scope(p);
     environment const & env = p.env();
     expr e1; level_param_names ls1;
     std::tie(e1, ls1) = parse_local_expr(p, "_unify");
@@ -432,6 +447,7 @@ static environment compile_cmd(parser & p) {
 }
 
 static environment eval_cmd(parser & p) {
+    transient_cmd_scope cmd_scope(p);
     auto pos = p.pos();
     expr e; level_param_names ls;
     std::tie(e, ls) = parse_local_expr(p, "_eval", /* relaxed */ false);
@@ -536,7 +552,7 @@ environment add_key_equivalence_cmd(parser & p) {
 }
 
 static environment run_command_cmd(parser & p) {
-    /* initial state for executing the tactic */
+    transient_cmd_scope cmd_scope(p);
     module::scope_pos_info scope_pos(p.pos());
     environment env      = p.env();
     options opts         = p.get_options();
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 39d8296956..f4cf6737e4 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -186,10 +186,10 @@ static expr parse_let(parser_state & p, pos_info const & pos, bool in_do_block)
         for (expr const & l : new_locals)
             p.add_local(l);
         expr body  = parse_let_body(p, pos, in_do_block);
-        match_definition_scope match_scope;
+        match_definition_scope match_scope(p.env());
         expr fn = p.save_pos(mk_local(mk_fresh_name(), *g_let_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos);
         expr eqn = Fun(fn, Fun(new_locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, lhs), pos), body), pos), p), p);
-        equations_header h = mk_equations_header(match_scope.get_name());
+        equations_header h = mk_equations_header(match_scope.get_name(), match_scope.get_actual_name());
         expr eqns  = p.save_pos(mk_equations(h, 1, &eqn), pos);
         return p.save_pos(mk_app(eqns, value), pos);
     }
@@ -319,7 +319,7 @@ static expr parse_do(parser_state & p, bool has_braces) {
             } else {
                 // must introduce a "fake" match
                 auto pos   = ps[i];
-                match_definition_scope match_scope;
+                match_definition_scope match_scope(p.env());
                 expr fn = p.save_pos(mk_local(mk_fresh_name(), *g_do_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos);
                 buffer<expr> locals;
                 to_buffer(lhss_locals[i], locals);
@@ -342,7 +342,7 @@ static expr parse_do(parser_state & p, bool has_braces) {
                                                                      ignore_if_unused),
                                                          pos), p), p);
                 eqs.push_back(else_eq);
-                equations_header h = mk_equations_header(match_scope.get_name());
+                equations_header h = mk_equations_header(match_scope.get_name(), match_scope.get_actual_name());
                 expr eqns  = p.save_pos(mk_equations(h, eqs.size(), eqs.data()), pos);
                 expr local = mk_local("_p", mk_expr_placeholder());
                 expr match = p.mk_app(eqns, local, pos);
@@ -744,10 +744,10 @@ static expr parse_lambda_constructor(parser_state & p, pos_info const & ini_pos)
     } else {
         body = parse_lambda_core(p, ini_pos);
     }
-    match_definition_scope match_scope;
+    match_definition_scope match_scope(p.env());
     expr fn  = p.save_pos(mk_local(mk_fresh_name(), *g_lambda_match_name, mk_expr_placeholder(), mk_rec_info(true)), pos);
     expr eqn = Fun(fn, Fun(locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, pattern), pos), body), pos), p), p);
-    equations_header h = mk_equations_header(match_scope.get_name());
+    equations_header h = mk_equations_header(match_scope.get_name(), match_scope.get_actual_name());
     expr x = p.rec_save_pos(mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info()), pos);
     bool use_cache = false;
     return p.rec_save_pos(Fun(x, mk_app(mk_equations(h, 1, &eqn), x), use_cache), pos);
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index be8608e79d..a1aab39416 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -190,6 +190,25 @@ static bool curr_is_binder_annotation(parser & p) {
            p.curr_is_token(get_ldcurly_tk()) || p.curr_is_token(get_lbracket_tk());
 }
 
+/* Auxiliary class to setup naming scopes for a variable/parameter/constant/axiom command.
+
+   We need the private_name_scope because the type may contain match-expressions.
+   These match expressions produce private definitions, and we need to make sure
+   they use the same infrastructure we use for definitions/theorems.
+*/
+class var_decl_scope {
+    environment m_env;
+    declaration_info_scope m_info_scope;
+    private_name_scope     m_prv_scope;
+public:
+    var_decl_scope(parser & p, decl_modifiers const & mods):
+        m_env(p.env()),
+        m_info_scope(p, decl_cmd_kind::Var, mods),
+        m_prv_scope(true, m_env) {
+        p.set_env(m_env);
+    }
+};
+
 static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const & meta) {
     check_variable_kind(p, k);
     auto pos = p.pos();
@@ -202,6 +221,7 @@ static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const
     expr type;
     buffer<name> ls_buffer;
     if (bi && bi->is_inst_implicit() && (k == variable_kind::Parameter || k == variable_kind::Variable)) {
+        var_decl_scope var_scope(p, meta.m_modifiers);
         /* instance implicit */
         if (p.curr_is_identifier()) {
             auto n_pos = p.pos();
@@ -244,6 +264,7 @@ static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const
             type = p.parse_expr();
         }
     } else {
+        var_decl_scope var_scope(p, meta.m_modifiers);
         /* non instance implicit cases */
         if (p.curr_is_token(get_lcurly_tk()) && (k == variable_kind::Parameter || k == variable_kind::Variable))
             throw parser_error("invalid declaration, only constants/axioms can be universe polymorphic", p.pos());
@@ -301,12 +322,30 @@ static environment parameter_cmd(parser & p, cmd_meta const & meta)    {
     return variable_cmd_core(p, variable_kind::Parameter, meta);
 }
 
+/*
+Remark: we currently do not support declarations such as:
+
+  parameters P Q : match ... end
+
+User should use
+
+  parameter P : match ... end
+  parameter Q : match ... end
+
+instead.
+*/
+static void ensure_no_match_in_variables_cmd(pos_info const & pos) {
+    if (used_match_idx()) {
+        throw parser_error("match-expressions are not supported in `parameters/variables/constants` commands "
+                           "(solution use `parameter/variable/constant` commands)", pos);
+    }
+}
+
 static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta const & meta) {
     check_variable_kind(p, k);
     auto pos = p.pos();
     module::scope_pos_info scope_pos(pos);
-    environment env = p.env();
-
+    declaration_info_scope d_scope(p, decl_cmd_kind::Var, meta.m_modifiers);
     optional<binder_info> bi = parse_binder_info(p, k);
     buffer<name> ids;
     optional<parser::local_scope> scope1;
@@ -322,6 +361,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
                 p.next();
                 ids.push_back(id);
                 type = p.parse_expr();
+                ensure_no_match_in_variables_cmd(pos);
             } else if (p.curr_is_token(get_rbracket_tk())) {
                 /* annotation update: variables [decA] */
                 p.parse_close_binder_info(bi);
@@ -329,7 +369,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
                 if (curr_is_binder_annotation(p))
                     return variables_cmd_core(p, k, meta);
                 else
-                    return env;
+                    return p.env();
             } else {
                 /* anonymous : variables [decidable A] */
                 expr left    = p.id_to_expr(id, id_pos);
@@ -340,12 +380,14 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
                 }
                 ids.push_back(id);
                 type = left;
+                ensure_no_match_in_variables_cmd(pos);
             }
         } else {
             /* anonymous : variables [forall x y, decidable (x = y)] */
             name id = p.mk_anonymous_inst_name();
             ids.push_back(id);
             type = p.parse_expr();
+            ensure_no_match_in_variables_cmd(pos);
         }
     } else {
         /* non instance implicit cases */
@@ -367,7 +409,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
                 if (curr_is_binder_annotation(p))
                     return variables_cmd_core(p, k, meta);
                 else
-                    return env;
+                    return p.env();
             } else {
                 throw parser_error("invalid variables/constants/axioms declaration, ':' expected", pos);
             }
@@ -375,9 +417,10 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons
         if (k == variable_kind::Constant || k == variable_kind::Axiom)
             scope1.emplace(p);
         type = p.parse_expr();
+        ensure_no_match_in_variables_cmd(pos);
     }
     p.parse_close_binder_info(bi);
-
+    environment env = p.env();
     level_param_names ls = to_level_param_names(collect_univ_params(type));
     list<expr> ctx = p.locals_to_context();
     for (auto id : ids) {
@@ -419,13 +462,13 @@ static environment axioms_cmd(parser & p, cmd_meta const & meta) {
 }
 
 static environment definition_cmd(parser & p, cmd_meta const & meta) {
-    return definition_cmd_core(p, def_cmd_kind::Definition, meta);
+    return definition_cmd_core(p, decl_cmd_kind::Definition, meta);
 }
 static environment theorem_cmd(parser & p, cmd_meta const & meta) {
-    return definition_cmd_core(p, def_cmd_kind::Theorem, meta);
+    return definition_cmd_core(p, decl_cmd_kind::Theorem, meta);
 }
 static environment example_cmd(parser & p, cmd_meta const & meta) {
-    return definition_cmd_core(p, def_cmd_kind::Example, meta);
+    return definition_cmd_core(p, decl_cmd_kind::Example, meta);
 }
 static environment instance_cmd(parser & p, cmd_meta const & _meta) {
     auto meta = _meta;
@@ -436,7 +479,7 @@ static environment instance_cmd(parser & p, cmd_meta const & _meta) {
     if (meta.m_modifiers.m_is_mutual)
         throw exception("invalid 'mutual' modifier for instance command");
     meta.m_modifiers.m_is_protected = true;
-    return definition_cmd_core(p, def_cmd_kind::Instance, meta);
+    return definition_cmd_core(p, decl_cmd_kind::Instance, meta);
 }
 
 static environment modifiers_cmd(parser & p, cmd_meta const & _meta) {
diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index 77418d8010..f691956e22 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/trace.h"
 #include "library/placeholder.h"
 #include "library/protected.h"
+#include "library/private.h"
 #include "library/aliases.h"
 #include "library/explicit.h"
 #include "library/reducible.h"
@@ -121,6 +122,8 @@ pair<expr, decl_attributes> parse_inner_header(parser & p, name const & c_expect
     if (c_expected != n)
         throw parser_error(sstream() << "invalid mutual declaration, '" << c_expected << "' expected",
                            id_pos);
+    /* Remark: if this is a private definition, the private prefix must have been set
+       before invoking this procedure. */
     declaration_name_scope scope(n);
     p.check_token_next(get_colon_tk(), "invalid mutual declaration, ':' expected");
     return mk_pair(p.parse_expr(), attrs);
@@ -356,7 +359,8 @@ environment add_alias(environment const & env, bool is_protected, name const & c
 }
 
 struct definition_info {
-    name     m_prefix;
+    name     m_prefix; // prefix for local names
+    name     m_actual_prefix; // actual prefix used to create kernel declaration names. m_prefix and m_actual_prefix are different for scoped/private declarations.
     bool     m_is_private{true}; // pattern matching outside of definitions should generate private names
     bool     m_is_meta{false};
     bool     m_is_noncomputable{false};
@@ -367,19 +371,23 @@ struct definition_info {
 
 MK_THREAD_LOCAL_GET_DEF(definition_info, get_definition_info);
 
-declaration_info_scope::declaration_info_scope(name const & ns, def_cmd_kind kind, decl_modifiers const & modifiers) {
+declaration_info_scope::declaration_info_scope(name const & ns, decl_cmd_kind kind, decl_modifiers const & modifiers) {
     definition_info & info = get_definition_info();
     lean_assert(info.m_prefix.is_anonymous());
-    info.m_prefix           = modifiers.m_is_private ? name() : ns;
+    info.m_prefix           = name(); // prefix is used to create local name
+    /* Remark: if info.m_actual_prefix is not `anonymous`, then it has already been set using private_name_scope */
+    if (info.m_actual_prefix.is_anonymous()) {
+        info.m_actual_prefix = ns;
+    }
     info.m_is_private       = modifiers.m_is_private;
     info.m_is_meta          = modifiers.m_is_meta;
     info.m_is_noncomputable = modifiers.m_is_noncomputable;
-    info.m_is_lemma         = kind == Theorem;
-    info.m_aux_lemmas       = kind != Theorem && !modifiers.m_is_meta;
+    info.m_is_lemma         = kind == decl_cmd_kind::Theorem;
+    info.m_aux_lemmas       = kind != decl_cmd_kind::Theorem && !modifiers.m_is_meta;
     info.m_next_match_idx = 1;
 }
 
-declaration_info_scope::declaration_info_scope(parser const & p, def_cmd_kind kind, decl_modifiers const & modifiers):
+declaration_info_scope::declaration_info_scope(parser const & p, decl_cmd_kind kind, decl_modifiers const & modifiers):
     declaration_info_scope(get_namespace(p.env()), kind, modifiers) {}
 
 declaration_info_scope::~declaration_info_scope() {
@@ -390,10 +398,11 @@ bool declaration_info_scope::gen_aux_lemmas() const {
     return get_definition_info().m_aux_lemmas;
 }
 
-equations_header mk_equations_header(list<name> const & ns) {
+equations_header mk_equations_header(list<name> const & ns, list<name> const & actual_ns) {
     equations_header h;
     h.m_num_fns          = length(ns);
     h.m_fn_names         = ns;
+    h.m_fn_actual_names  = actual_ns;
     h.m_is_private       = get_definition_info().m_is_private;
     h.m_is_meta          = get_definition_info().m_is_meta;
     h.m_is_noncomputable = get_definition_info().m_is_noncomputable;
@@ -402,8 +411,8 @@ equations_header mk_equations_header(list<name> const & ns) {
     return h;
 }
 
-equations_header mk_equations_header(name const & n) {
-    return mk_equations_header(to_list(n));
+equations_header mk_equations_header(name const & n, name const & actual_n) {
+    return mk_equations_header(to_list(n), to_list(actual_n));
 }
 
 /* Auxiliary function for creating names for auxiliary declarations.
@@ -424,35 +433,73 @@ bool used_match_idx() {
 declaration_name_scope::declaration_name_scope() {
     definition_info & info = get_definition_info();
     m_old_prefix          = info.m_prefix;
+    m_old_actual_prefix   = info.m_actual_prefix;
     m_old_next_match_idx  = info.m_next_match_idx;
     info.m_next_match_idx = 1;
 }
 
 void declaration_name_scope::set_name(name const & n) {
     lean_assert(m_name.is_anonymous());
-    definition_info & info = get_definition_info();
-    info.m_prefix          = mk_decl_name(info.m_prefix, n);
-    m_name                = info.m_prefix;
+    definition_info & info    = get_definition_info();
+    info.m_prefix             = mk_decl_name(info.m_prefix, n);
+    info.m_actual_prefix      = mk_decl_name(info.m_actual_prefix, n);
+    m_name                    = info.m_prefix;
+    m_actual_name             = info.m_actual_prefix;
 }
 
 declaration_name_scope::declaration_name_scope(name const & n) {
     definition_info & info = get_definition_info();
     m_old_prefix          = info.m_prefix;
+    m_old_actual_prefix   = info.m_actual_prefix;
     m_old_next_match_idx  = info.m_next_match_idx;
     info.m_prefix         = mk_decl_name(info.m_prefix, n);
+    info.m_actual_prefix  = mk_decl_name(info.m_actual_prefix, n);
     info.m_next_match_idx = 1;
     m_name                = info.m_prefix;
+    m_actual_name         = info.m_actual_prefix;
 }
 
 declaration_name_scope::~declaration_name_scope() {
     definition_info & info = get_definition_info();
     info.m_prefix          = m_old_prefix;
+    info.m_actual_prefix  = m_old_actual_prefix;
     info.m_next_match_idx  = m_old_next_match_idx;
 }
 
-match_definition_scope::match_definition_scope() {
+private_name_scope::private_name_scope(bool is_private, environment & env) {
     definition_info & info = get_definition_info();
-    m_name = mk_decl_name(info.m_prefix, name("_match").append_after(info.m_next_match_idx));
-    info.m_next_match_idx++;
+    m_old_actual_prefix    = info.m_prefix;
+    m_old_is_private       = info.m_is_private;
+    if (is_private) {
+        name prv_prefix;
+        std::tie(env, prv_prefix) = mk_private_prefix(env);
+        info.m_is_private     = true;
+        info.m_actual_prefix = prv_prefix;
+    }
+}
+
+private_name_scope::~private_name_scope() {
+    definition_info & info = get_definition_info();
+    info.m_actual_prefix   = m_old_actual_prefix;
+    info.m_is_private      = m_old_is_private;
+}
+
+match_definition_scope::match_definition_scope(environment const & env) {
+    definition_info & info = get_definition_info();
+    while (true) {
+        m_name        = mk_decl_name(info.m_prefix, name("_match").append_after(info.m_next_match_idx));
+        m_actual_name = mk_decl_name(info.m_actual_prefix, name("_match").append_after(info.m_next_match_idx));
+        info.m_next_match_idx++;
+        if (empty(get_expr_aliases(env, m_name))) {
+            /* Make sure we don't introduce aliases.
+               This is important when match-expressions are used in several parameters in a section.
+               Example:
+
+                  parameter P : match ... end
+                  parameter Q : match ... end
+            */
+            break;
+        }
+    }
 }
 }
diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h
index d67ffd1b21..6286547e2e 100644
--- a/src/frontends/lean/decl_util.h
+++ b/src/frontends/lean/decl_util.h
@@ -13,7 +13,7 @@ namespace lean {
 class parser;
 class elaborator;
 
-enum def_cmd_kind { Theorem, Definition, Example, Instance };
+enum class decl_cmd_kind { Theorem, Definition, Example, Instance, Var };
 
 struct decl_modifiers {
     bool m_is_private{false};
@@ -29,11 +29,13 @@ struct decl_modifiers {
 
 /** \brief In Lean, declarations may contain nested definitions.
     This object is used to propagate relevant flags to
-    nested definitions. */
+    nested definitions.
+
+    It is used to set/restore the thread local information. */
 class declaration_info_scope {
-    declaration_info_scope(name const & ns, def_cmd_kind kind, decl_modifiers const & modifiers);
+    declaration_info_scope(name const & ns, decl_cmd_kind kind, decl_modifiers const & modifiers);
 public:
-    declaration_info_scope(parser const & p, def_cmd_kind kind, decl_modifiers const & modifiers);
+    declaration_info_scope(parser const & p, decl_cmd_kind kind, decl_modifiers const & modifiers);
     ~declaration_info_scope();
     bool gen_aux_lemmas() const;
 };
@@ -42,23 +44,46 @@ public:
     naming prefix for nested definitions. */
 class declaration_name_scope {
     name     m_name;
-    name     m_old_prefix;
+    name     m_actual_name;
+    name     m_old_prefix; /* save current user facing prefix */
+    name     m_old_actual_prefix; /* save current prefix */
     unsigned m_old_next_match_idx;
+    /* Remark: the operation prefix + name in the following constructors and methods tries to avoid propagating
+       the string `_main` into names. That is, `foo._main` + `bla` is `foo.bla`. */
 public:
+    /* Save the current prefix and match_idx, and set m_name to current prefix + n. */
     declaration_name_scope(name const & n);
+    /* Save the current prefix and match_idx, and reset get_definition_info().m_next_match_idx. */
     declaration_name_scope();
-    ~declaration_name_scope();
+    /* Set m_name to current prefix + n. This method is used when the constructor declaration_name_scope
+       has been used. */
     void set_name(name const & n);
+    /* Restore prefix and match_idx. */
+    ~declaration_name_scope();
     name const & get_name() const { return m_name; }
+    name const & get_actual_name() const { return m_actual_name; }
+};
+
+/** \brief Auxiliary scope for setting m_actual_prefix.
+    It is used with declaration_name_scope. */
+class private_name_scope {
+    name     m_old_actual_prefix; /* save current prefix */
+    bool     m_old_is_private;
+public:
+    /* Remark: If is_private == false, then this auxiliary scope is a no-op. */
+    private_name_scope(bool is_private, environment & env);
+    ~private_name_scope();
 };
 
 /** \brief Auxiliary scope to compute the name for a nested match expression.
     In Lean, we create auxiliary declarations for match expressions. */
 class match_definition_scope {
     name m_name;
+    name m_actual_name;
 public:
-    match_definition_scope();
+    match_definition_scope(environment const & env);
     name const & get_name() const { return m_name; }
+    name const & get_actual_name() const { return m_actual_name; }
 };
 
 /** \brief Return true if the current scope used match-expressions */
@@ -128,8 +153,8 @@ environment add_alias(environment const & env, bool is_protected, name const & c
 
 /** \brief Create an equations header for the given function names.
     It uses the information set using declaration_info_scope */
-equations_header mk_equations_header(list<name> const & fn_names);
-equations_header mk_equations_header(name const & fn_name);
+equations_header mk_equations_header(list<name> const & fn_names, list<name> const & fn_actual_names);
+equations_header mk_equations_header(name const & fn_name, name const & fn_actual_name);
 
 expr replace_locals_preserving_pos_info(expr const & e, buffer<expr> const & from, buffer<expr> const & to);
 expr replace_local_preserving_pos_info(expr const & e, expr const & from, expr const & to);
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index d9f37a1a24..4bf6deb813 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -83,13 +83,14 @@ optional<expr> parse_using_well_founded(parser & p) {
     }
 }
 
-expr mk_equations(parser & p, buffer<expr> const & fns, buffer<name> const & fn_full_names, buffer<expr> const & eqs,
+expr mk_equations(parser & p, buffer<expr> const & fns,
+                  buffer<name> const & fn_full_names, buffer<name> const & fn_prv_names, buffer<expr> const & eqs,
                   optional<expr> const & wf_tacs, pos_info const & pos) {
     buffer<expr> new_eqs;
     for (expr const & eq : eqs) {
         new_eqs.push_back(Fun(fns, eq, p));
     }
-    equations_header h = mk_equations_header(to_list(fn_full_names));
+    equations_header h = mk_equations_header(to_list(fn_full_names), to_list(fn_prv_names));
     if (wf_tacs) {
         return p.save_pos(mk_equations(h, new_eqs.size(), new_eqs.data(), *wf_tacs), pos);
     } else {
@@ -97,11 +98,12 @@ expr mk_equations(parser & p, buffer<expr> const & fns, buffer<name> const & fn_
     }
 }
 
-expr mk_equations(parser & p, expr const & fn, name const & full_name, buffer<expr> const & eqs,
+expr mk_equations(parser & p, expr const & fn, name const & full_name, name const & full_prv_name, buffer<expr> const & eqs,
                   optional<expr> const & wf_tacs, pos_info const & pos) {
     buffer<expr> fns; fns.push_back(fn);
     buffer<name> full_names; full_names.push_back(full_name);
-    return mk_equations(p, fns, full_names, eqs, wf_tacs, pos);
+    buffer<name> full_prv_names; full_prv_names.push_back(full_prv_name);
+    return mk_equations(p, fns, full_names, full_prv_names, eqs, wf_tacs, pos);
 }
 
 void check_valid_end_of_equations(parser & p) {
@@ -114,19 +116,23 @@ void check_valid_end_of_equations(parser & p) {
     }
 }
 
-expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> & fns, buffer<expr> & params) {
+static expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> & fns, buffer<name> & prv_names,
+                                    buffer<expr> & params) {
     parser::local_scope scope1(p);
     auto header_pos = p.pos();
     buffer<expr> pre_fns;
     parse_mutual_header(p, lp_names, pre_fns, params);
     buffer<expr> eqns;
     buffer<name> full_names;
+    buffer<name> full_actual_names;
     for (expr const & pre_fn : pre_fns) {
         // TODO(leo, dhs): make use of attributes
         expr fn_type = parse_inner_header(p, mlocal_pp_name(pre_fn)).first;
         declaration_name_scope scope2(mlocal_pp_name(pre_fn));
         declaration_name_scope scope3("_main");
         full_names.push_back(scope3.get_name());
+        full_actual_names.push_back(scope3.get_actual_name());
+        prv_names.push_back(scope2.get_actual_name());
         if (p.curr_is_token(get_period_tk())) {
             auto period_pos = p.pos();
             p.next();
@@ -146,7 +152,7 @@ expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> &
     for (expr & eq : eqns) {
         eq = replace_locals_preserving_pos_info(eq, pre_fns, fns);
     }
-    expr r = mk_equations(p, fns, full_names, eqns, wf_tacs, header_pos);
+    expr r = mk_equations(p, fns, full_names, full_actual_names, eqns, wf_tacs, header_pos);
     collect_implicit_locals(p, lp_names, params, r);
     return r;
 }
@@ -170,21 +176,6 @@ static void finalize_definition(elaborator & elab, buffer<expr> const & params,
     lp_names.append(implicit_lp_names);
 }
 
-static pair<environment, name> mk_real_name(environment const & env, name const & c_name, bool is_private, pos_info const & pos) {
-    environment new_env = env;
-    name c_real_name;
-    if (is_private) {
-        unsigned h  = hash(pos.first, pos.second);
-        auto env_n  = add_private_name(new_env, c_name, optional<unsigned>(h));
-        new_env     = env_n.first;
-        c_real_name = env_n.second;
-    } else {
-        name const & ns = get_namespace(env);
-        c_real_name     = ns + c_name;
-    }
-    return mk_pair(new_env, c_real_name);
-}
-
 static expr fix_rec_fn_name(expr const & e, name const & c_name, name const & c_real_name) {
     return replace(e, [&](expr const & m, unsigned) {
             if (is_rec_fn_macro(m) && get_rec_fn_name(m) == c_name) {
@@ -241,12 +232,17 @@ static environment compile_decl(parser & p, environment const & env,
 }
 
 static pair<environment, name>
-declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffer<name> const & lp_names,
-                   name const & c_name, expr type, optional<expr> val, task<expr> const & proof, cmd_meta const & meta,
+declare_definition(parser & p, environment const & env, decl_cmd_kind kind, buffer<name> const & lp_names,
+                   name const & c_name, name const & prv_name, expr type, optional<expr> val, task<expr> const & proof, cmd_meta const & meta,
                    pos_info const & pos) {
-    auto env_n = mk_real_name(env, c_name, meta.m_modifiers.m_is_private, pos);
-    environment new_env = env_n.first;
-    name c_real_name    = env_n.second;
+    name c_real_name;
+    environment new_env = env;
+    if (has_private_prefix(new_env, prv_name)) {
+        new_env     = register_private_name(new_env, c_name, prv_name);
+        c_real_name = prv_name;
+    } else {
+        c_real_name = get_namespace(env) + c_name;
+    }
     if (val && meta.m_modifiers.m_is_meta) {
         /* TODO(Leo): fix fix_rec_fn_name for mutual definitions.
            We currently do not support meta mutual definitions. Thus, this is not currently an issue. */
@@ -260,7 +256,7 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
     bool use_conv_opt = true;
     bool is_trusted   = !meta.m_modifiers.m_is_meta;
     auto def          =
-        !val ? mk_theorem(c_real_name, to_list(lp_names), type, proof) : (kind == Theorem ?
+        !val ? mk_theorem(c_real_name, to_list(lp_names), type, proof) : (kind == decl_cmd_kind::Theorem ?
         mk_theorem(c_real_name, to_list(lp_names), type, *val) :
         mk_definition(new_env, c_real_name, to_list(lp_names), type, *val, use_conv_opt, is_trusted));
     auto cdef         = check(p, new_env, c_name, def, pos);
@@ -463,14 +459,17 @@ static environment copy_equation_lemmas(environment const & env, name const & d_
     return copy_equation_lemmas(env, d_names);
 }
 
-static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta const & meta) {
+static environment mutual_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta const & meta) {
     buffer<name> lp_names;
     buffer<expr> fns, params;
     declaration_info_scope scope(p, kind, meta.m_modifiers);
     auto header_pos = p.pos();
     /* TODO(Leo): allow a different doc string for each function in a mutual definition. */
     optional<std::string> doc_string = meta.m_doc_string;
-    expr val = parse_mutual_definition(p, lp_names, fns, params);
+    environment env = p.env();
+    private_name_scope prv_scope(meta.m_modifiers.m_is_private, env);
+    buffer<name> prv_names;
+    expr val = parse_mutual_definition(p, lp_names, fns, prv_names, params);
 
     if (meta.m_modifiers.m_is_meta) {
         throw exception("support for mutual meta definitions has not been implemented yet");
@@ -481,7 +480,7 @@ static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd
         return p.env();
 
     bool recover_from_errors = true;
-    elaborator elab(p.env(), p.get_options(), get_namespace(p.env()) + mlocal_pp_name(fns[0]), metavar_context(), local_context(), recover_from_errors);
+    elaborator elab(env, p.get_options(), get_namespace(env) + mlocal_pp_name(fns[0]), metavar_context(), local_context(), recover_from_errors);
     buffer<expr> new_params;
     elaborate_params(elab, params, new_params);
     val = replace_locals_preserving_pos_info(val, params, new_params);
@@ -492,6 +491,7 @@ static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd
         return p.env();
     }
     unsigned num_defs = get_equations_result_size(val);
+    lean_assert(num_defs == prv_names.size());
     lean_assert(fns.size() == num_defs);
     buffer<name> new_d_names;
     /* Define functions */
@@ -502,7 +502,7 @@ static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd
         environment env = elab.env();
         name c_name = mlocal_name(fns[i]);
         name c_real_name;
-        std::tie(env, c_real_name) = declare_definition(p, env, kind, lp_names, c_name,
+        std::tie(env, c_real_name) = declare_definition(p, env, kind, lp_names, c_name, prv_names[i],
                                                         curr_type, some_expr(curr), {}, meta, header_pos);
         env = add_local_ref(p, env, c_name, c_real_name, lp_names, params);
         new_d_names.push_back(c_real_name);
@@ -517,8 +517,15 @@ static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd
     return elab.env();
 }
 
-static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & params,
-                                  bool is_example, bool is_instance, bool is_meta) {
+/* Return tuple (fn, val, actual_name) where
+
+   - fn is a local constant with the user name + type
+   - val is the actual definition
+   - actual_name for the kernel declaration.
+     Note that mlocal_pp_name(fn) and actual_name are different for scoped/private declarations.
+*/
+static std::tuple<expr, expr, name> parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & params,
+                                                     bool is_example, bool is_instance, bool is_meta) {
     parser::local_scope scope1(p);
     auto header_pos = p.pos();
     declaration_name_scope scope2;
@@ -535,7 +542,7 @@ static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<ex
             expr eqn = copy_tag(val, mk_equation(fn, val));
             buffer<expr> eqns;
             eqns.push_back(eqn);
-            val = mk_equations(p, fn, scope2.get_name(), eqns, {}, header_pos);
+            val = mk_equations(p, fn, scope2.get_name(), scope2.get_actual_name(), eqns, {}, header_pos);
         } else {
             val = p.parse_expr();
         }
@@ -555,12 +562,12 @@ static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<ex
             check_valid_end_of_equations(p);
         }
         optional<expr> wf_tacs = parse_using_well_founded(p);
-        val = mk_equations(p, fn, scope2.get_name(), eqns, wf_tacs, header_pos);
+        val = mk_equations(p, fn, scope2.get_name(), scope2.get_actual_name(), eqns, wf_tacs, header_pos);
     } else {
         val = p.parser_error_or_expr({"invalid definition, '|' or ':=' expected", p.pos()});
     }
     collect_implicit_locals(p, lp_names, params, {mlocal_type(fn), val});
-    return mk_pair(fn, val);
+    return std::make_tuple(fn, val, scope2.get_actual_name());
 }
 
 static void replace_params(buffer<expr> const & params, buffer<expr> const & new_params, expr & fn, expr & val) {
@@ -579,15 +586,15 @@ static expr_pair elaborate_theorem(elaborator & elab, expr const & fn, expr val)
     return elab.elaborate_with_type(val, mk_as_is(fn_type));
 }
 
-static expr_pair elaborate_definition_core(elaborator & elab, def_cmd_kind kind, expr const & fn, expr const & val) {
-    if (kind == Theorem) {
+static expr_pair elaborate_definition_core(elaborator & elab, decl_cmd_kind kind, expr const & fn, expr const & val) {
+    if (kind == decl_cmd_kind::Theorem) {
         return elaborate_theorem(elab, fn, val);
     } else {
         return elab.elaborate_with_type(val, mlocal_type(fn));
     }
 }
 
-static expr_pair elaborate_definition(parser & p, elaborator & elab, def_cmd_kind kind, expr const & fn, expr const & val, pos_info const & pos) {
+static expr_pair elaborate_definition(parser & p, elaborator & elab, decl_cmd_kind kind, expr const & fn, expr const & val, pos_info const & pos) {
     if (p.profiling()) {
         xtimeit timer(get_profiling_threshold(p.get_options()), [&](second_duration duration) {
                 auto msg = p.mk_message(pos, INFORMATION);
@@ -765,24 +772,27 @@ static bool is_rfl_preexpr(expr const & e) {
     return is_constant(e, get_rfl_name());
 }
 
-environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta meta) {
+environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta meta) {
     buffer<name> lp_names;
     buffer<expr> params;
     expr fn, val;
     auto header_pos = p.pos();
     module::scope_pos_info scope_pos(header_pos);
     declaration_info_scope scope(p, kind, meta.m_modifiers);
-    bool is_example  = (kind == def_cmd_kind::Example);
-    bool is_instance = (kind == def_cmd_kind::Instance);
-    bool aux_lemmas  = scope.gen_aux_lemmas();
-    bool is_rfl      = false;
+    environment env   = p.env();
+    private_name_scope prv_scope(meta.m_modifiers.m_is_private, env);
+    bool is_example   = (kind == decl_cmd_kind::Example);
+    bool is_instance  = (kind == decl_cmd_kind::Instance);
+    bool aux_lemmas   = scope.gen_aux_lemmas();
+    bool is_rfl       = false;
     if (is_instance)
-        meta.m_attrs.set_attribute(p.env(), "instance");
-    std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance, meta.m_modifiers.m_is_meta);
+        meta.m_attrs.set_attribute(env, "instance");
+    name prv_name;
+    std::tie(fn, val, prv_name) = parse_definition(p, lp_names, params, is_example, is_instance, meta.m_modifiers.m_is_meta);
 
     auto begin_pos = p.cmd_pos();
     auto end_pos = p.pos();
-    scope_log_tree lt(logtree().mk_child({}, (get_namespace(p.env()) + mlocal_pp_name(fn)).to_string(),
+    scope_log_tree lt(logtree().mk_child({}, (get_namespace(env) + mlocal_pp_name(fn)).to_string(),
                                          {logtree().get_location().m_file_name, {begin_pos, end_pos}}));
 
     // skip elaboration of definitions during reparsing
@@ -790,7 +800,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
         return p.env();
 
     bool recover_from_errors = true;
-    elaborator elab(p.env(), p.get_options(), get_namespace(p.env()) + mlocal_pp_name(fn), metavar_context(), local_context(), recover_from_errors);
+    elaborator elab(env, p.get_options(), get_namespace(env) + mlocal_pp_name(fn), metavar_context(), local_context(), recover_from_errors);
     buffer<expr> new_params;
     elaborate_params(elab, params, new_params);
     elab.set_instance_fingerprint();
@@ -802,7 +812,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
         bool eqns = false;
         name c_name = mlocal_name(fn);
         pair<environment, name> env_n;
-        if (kind == Theorem) {
+        if (kind == decl_cmd_kind::Theorem) {
             is_rfl = is_rfl_preexpr(val);
             type = elab.elaborate_type(mlocal_type(fn));
             elab.ensure_no_unassigned_metavars(type);
@@ -823,8 +833,8 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
                                        new_fn, val, thm_finfo, is_rfl, type,
                                        mctx, lctx, pos_provider, use_info_manager, file_name);
             }), log_tree::ElaborationLevel);
-            env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, proof, meta, header_pos);
-        } else if (kind == Example) {
+            env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, prv_name, type, opt_val, proof, meta, header_pos);
+        } else if (kind == decl_cmd_kind::Example) {
             auto env = p.env();
             auto opts = p.get_options();
             auto lp_name_list = to_list(lp_names);
@@ -854,7 +864,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
                 val = get_equations_result(val, 0);
             }
             finalize_definition(elab, new_params, type, val, lp_names, meta.m_modifiers.m_is_meta);
-            env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, some_expr(val),
+            env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, prv_name, type, some_expr(val),
                                        {}, meta, header_pos);
         }
         environment new_env = env_n.first;
@@ -864,9 +874,9 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
         if (eqns && aux_lemmas) {
             new_env = copy_equation_lemmas(new_env, c_real_name);
         }
-        if (!eqns && !meta.m_modifiers.m_is_meta && (kind == Definition || kind == Instance)) {
+        if (!eqns && !meta.m_modifiers.m_is_meta && (kind == decl_cmd_kind::Definition || kind == decl_cmd_kind::Instance)) {
             unsigned arity = new_params.size();
-            new_env = mk_simple_equation_lemma_for(new_env, p.get_options(), meta.m_modifiers.m_is_private, c_real_name, arity);
+            new_env = mk_simple_equation_lemma_for(new_env, p.get_options(), meta.m_modifiers.m_is_private, c_name, c_real_name, arity);
         }
         /* Apply attributes last */
         return meta.m_attrs.apply(new_env, p.ios(), c_real_name);
@@ -886,7 +896,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta m
     }
 }
 
-environment definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta const & meta) {
+environment definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta const & meta) {
     if (meta.m_modifiers.m_is_mutual)
         return mutual_definition_cmd_core(p, kind, meta);
     else
diff --git a/src/frontends/lean/definition_cmds.h b/src/frontends/lean/definition_cmds.h
index 90eb58c0e1..ae51822573 100644
--- a/src/frontends/lean/definition_cmds.h
+++ b/src/frontends/lean/definition_cmds.h
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_util.h"
 namespace lean {
 
-environment definition_cmd_core(parser & p, def_cmd_kind k, cmd_meta const & meta);
+environment definition_cmd_core(parser & p, decl_cmd_kind k, cmd_meta const & meta);
 
 environment ensure_decl_namespaces(environment const & env, name const & full_n);
 }
diff --git a/src/frontends/lean/match_expr.cpp b/src/frontends/lean/match_expr.cpp
index e0cc227d62..afe4c077bc 100644
--- a/src/frontends/lean/match_expr.cpp
+++ b/src/frontends/lean/match_expr.cpp
@@ -21,8 +21,8 @@ bool is_match_binder_name(name const & n) { return n == *g_match_name; }
 /** \brief Use equations compiler infrastructure to implement match-with */
 expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
     parser::local_scope scope1(p);
-    match_definition_scope scope2;
-    equations_header header = mk_equations_header(scope2.get_name());
+    match_definition_scope scope2(p.env());
+    equations_header header = mk_equations_header(scope2.get_name(), scope2.get_actual_name());
     buffer<expr> eqns;
     buffer<expr> ts;
     try {
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index cc301c1b03..cf4d95f890 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -274,6 +274,7 @@ struct structure_cmd_fn {
     buffer<bool>                m_private_parents;
     name                        m_mk;
     name                        m_mk_short;
+    name                        m_private_prefix;
     pos_info                    m_mk_pos;
     implicit_infer_kind         m_mk_infer;
     buffer<field_decl>          m_fields;
@@ -302,6 +303,8 @@ struct structure_cmd_fn {
             throw exception("only attribute [class] accepted for structures");
     }
 
+    bool is_private() const { return m_meta_info.m_modifiers.m_is_private; }
+
     /** \brief Parse structure name and (optional) universe parameters */
     void parse_decl_name() {
         m_name_pos = m_p.pos();
@@ -313,11 +316,10 @@ struct structure_cmd_fn {
             m_explicit_universe_params = false;
         }
         m_given_name = m_p.check_decl_id_next("invalid 'structure', identifier expected");
-        if (m_meta_info.m_modifiers.m_is_private) {
-            unsigned h   = hash(m_name_pos.first, m_name_pos.second);
-            auto env_n   = add_private_name(m_env, m_given_name, optional<unsigned>(h));
-            m_env        = env_n.first;
-            m_name  = env_n.second;
+        if (is_private()) {
+            std::tie(m_env, m_private_prefix) = mk_private_prefix(m_env);
+            m_name = m_private_prefix + m_given_name;
+            m_env  = register_private_name(m_env, m_given_name, m_name);
         } else {
             m_name = m_namespace + m_given_name;
         }
@@ -1019,7 +1021,7 @@ struct structure_cmd_fn {
         levels rec_ctx_levels;
         if (!is_nil(m_ctx_levels))
             rec_ctx_levels = levels(mk_level_placeholder(), m_ctx_levels);
-        if (m_meta_info.m_modifiers.m_is_private) {
+        if (is_private()) {
             name given_rec_name = name(m_given_name, n.get_string());
             m_env = ::lean::add_alias(m_p, m_env, given_rec_name, n, rec_ctx_levels, m_ctx_locals);
         } else {
@@ -1091,6 +1093,12 @@ struct structure_cmd_fn {
                         args.push_back(local);
                 }
                 name decl_name  = name(m_name + field.get_name(), "_default");
+                name decl_prv_name;
+                if (is_private()) {
+                    decl_prv_name = name(m_private_prefix + m_given_name + field.get_name(), "_default");
+                } else {
+                    decl_prv_name = decl_name;
+                }
                 /* TODO(Leo): add helper function for adding definition.
                    It should unfold_untrusted_macros */
                 expr decl_type  = unfold_untrusted_macros(m_env, Pi(args, type));
@@ -1103,8 +1111,7 @@ struct structure_cmd_fn {
                 declaration new_decl = mk_definition_inferring_trusted(m_env, decl_name, decl_lvls,
                                                                        decl_type, decl_value, reducibility_hints::mk_abbreviation());
                 m_env = module::add(m_env, check(m_env, new_decl));
-                m_env = mk_simple_equation_lemma_for(m_env, m_p.get_options(),
-                                                     m_meta_info.m_modifiers.m_is_private, decl_name, args.size());
+                m_env = mk_simple_equation_lemma_for(m_env, m_p.get_options(), is_private(), decl_name, decl_prv_name, args.size());
                 m_env = set_reducible(m_env, decl_name, reducible_status::Reducible, true);
             }
         }
diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp
index 23c736ab48..cb62fcf7e3 100644
--- a/src/library/equations_compiler/elim_match.cpp
+++ b/src/library/equations_compiler/elim_match.cpp
@@ -1406,10 +1406,12 @@ eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_c
        congruence closure modules make them "believe" that this is
        a dependent function.
     */
-    expr fn_type = get_fn_type_from_eqns(eqns);
+    expr fn_type        = get_fn_type_from_eqns(eqns);
+    name fn_name        = head(header.m_fn_names);
+    name fn_actual_name = head(header.m_fn_actual_names);
     expr fn;
-    std::tie(env, fn) = mk_aux_definition(env, opts, mctx, lctx, header, head(header.m_fn_names), fn_type, R.m_fn);
-    name fn_name = const_name(get_app_fn(fn));
+    std::tie(env, fn) = mk_aux_definition(env, opts, mctx, lctx, header,
+                                          fn_name, fn_actual_name, fn_type, R.m_fn);
     unsigned eqn_idx     = 1;
     type_context ctx2(env, opts, mctx, lctx, transparency_mode::Semireducible);
     for (expr type : R.m_lemmas) {
@@ -1425,7 +1427,7 @@ eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_c
         buffer<expr> lhs_args;
         get_app_args(lhs, lhs_args);
         expr new_lhs = mk_app(fn, lhs_args);
-        env = mk_equation_lemma(env, opts, mctx, ctx2.lctx(), fn_name,
+        env = mk_equation_lemma(env, opts, mctx, ctx2.lctx(), fn_name, fn_actual_name,
                                 eqn_idx, header.m_is_private, locals.as_buffer(), new_lhs, rhs);
         eqn_idx++;
     }
diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp
index 266a58a1f3..aaee50ab7b 100644
--- a/src/library/equations_compiler/equations.cpp
+++ b/src/library/equations_compiler/equations.cpp
@@ -43,6 +43,7 @@ bool operator==(equations_header const & h1, equations_header const & h2) {
     return
         h1.m_num_fns == h2.m_num_fns &&
         h1.m_fn_names == h2.m_fn_names &&
+        h1.m_fn_actual_names == h2.m_fn_actual_names &&
         h1.m_is_private == h2.m_is_private &&
         h1.m_is_lemma == h2.m_is_lemma &&
         h1.m_is_meta == h2.m_is_meta &&
@@ -64,6 +65,7 @@ public:
         s << *g_equations_opcode << m_header.m_num_fns << m_header.m_is_private << m_header.m_is_meta
           << m_header.m_is_noncomputable << m_header.m_is_lemma << m_header.m_aux_lemmas;
         write_list(s, m_header.m_fn_names);
+        write_list(s, m_header.m_fn_actual_names);
     }
     virtual bool operator==(macro_definition_cell const & other) const override {
         if (auto other_ptr = dynamic_cast<equations_macro_cell const *>(&other)) {
@@ -272,6 +274,7 @@ void initialize_equations() {
                                     d >> h.m_num_fns >> h.m_is_private >> h.m_is_meta >> h.m_is_noncomputable
                                       >> h.m_is_lemma >> h.m_aux_lemmas;
                                     h.m_fn_names = read_list<name>(d);
+                                    h.m_fn_actual_names = read_list<name>(d);
                                     if (num == 0 || h.m_num_fns == 0)
                                         throw corrupted_stream_exception();
                                     if (!is_lambda_equation(args[num-1]) && !is_lambda_no_equation(args[num-1])) {
diff --git a/src/library/equations_compiler/equations.h b/src/library/equations_compiler/equations.h
index 32013d2fd4..01dad87c57 100644
--- a/src/library/equations_compiler/equations.h
+++ b/src/library/equations_compiler/equations.h
@@ -32,7 +32,8 @@ bool is_inaccessible(expr const & e);
 
 struct equations_header {
     unsigned   m_num_fns{0};              /* number of functions being defined */
-    list<name> m_fn_names;                /* names for functions */
+    list<name> m_fn_names;                /* local names for functions */
+    list<name> m_fn_actual_names;         /* Full qualified name and/or private name */
     bool       m_is_private{false};       /* if true, it must be a private definition */
     bool       m_is_lemma{false};         /* if true, equations are defining a lemma */
     bool       m_is_meta{false};          /* the auxiliary declarations should be tagged as meta */
diff --git a/src/library/equations_compiler/pack_mutual.cpp b/src/library/equations_compiler/pack_mutual.cpp
index 4bc29b13b0..5efc67ccc2 100644
--- a/src/library/equations_compiler/pack_mutual.cpp
+++ b/src/library/equations_compiler/pack_mutual.cpp
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "library/constants.h"
 #include "library/trace.h"
+#include "library/private.h"
 #include "library/app_builder.h"
 #include "library/type_context.h"
 #include "library/locals.h"
@@ -150,17 +151,25 @@ struct pack_mutual_fn {
         buffer<expr> domains;
         buffer<expr> codomains;
         level        codomains_lvl;
+        equations_header header = get_equations_header(e);
         name         new_fn_name("_mutual");
+        name         new_fn_actual_name;
+        if (header.m_is_private) {
+            new_fn_actual_name = name(*get_private_prefix(m_ctx.env(), head(header.m_fn_actual_names)), "_mutual");
+        } else {
+            new_fn_actual_name = "_mutual";
+        }
         for (unsigned fidx = 0; fidx < ues.get_num_fns(); fidx++) {
             expr const & fn = ues.get_fn(fidx);
-            new_fn_name = new_fn_name + mlocal_pp_name(fn);
+            new_fn_name        = new_fn_name + mlocal_pp_name(fn);
+            new_fn_actual_name = new_fn_actual_name + mlocal_pp_name(fn);
             lean_assert(ues.get_arity_of(fidx) == 1);
-            expr fn_type    = m_ctx.relaxed_whnf(m_ctx.infer(fn));
+            expr fn_type       = m_ctx.relaxed_whnf(m_ctx.infer(fn));
             lean_assert(is_pi(fn_type));
             domains.push_back(binding_domain(fn_type));
-            expr y          = locals.push_local("_s", binding_domain(fn_type));
-            expr c          = instantiate(binding_body(fn_type), y);
-            level c_lvl     = get_level(m_ctx, c);
+            expr y             = locals.push_local("_s", binding_domain(fn_type));
+            expr c             = instantiate(binding_body(fn_type), y);
+            level c_lvl        = get_level(m_ctx, c);
             if (fidx == 0) {
                 codomains_lvl = c_lvl;
             } else if (!m_ctx.is_def_eq(mk_sort(c_lvl), mk_sort(codomains_lvl))) {
@@ -178,8 +187,9 @@ struct pack_mutual_fn {
         trace_debug_mutual(tout() << "new function " << new_fn_name << " : " << new_fn_type << "\n";);
 
         equations_header new_header = get_equations_header(e);
-        new_header.m_fn_names = to_list(new_fn_name);
-        new_header.m_num_fns  = 1;
+        new_header.m_fn_names         = to_list(new_fn_name);
+        new_header.m_fn_actual_names  = to_list(new_fn_actual_name);
+        new_header.m_num_fns          = 1;
 
         replace_fns replacer(m_ctx, ues, new_fn);
 
diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp
index 80e996f545..066342978f 100644
--- a/src/library/equations_compiler/structural_rec.cpp
+++ b/src/library/equations_compiler/structural_rec.cpp
@@ -708,7 +708,9 @@ struct structural_rec_fn {
         } else {
             expr r;
             std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, m_header,
-                                                   head(m_header.m_fn_names), m_fn_type, new_fn);
+                                                   head(m_header.m_fn_names),
+                                                   head(m_header.m_fn_actual_names),
+                                                   m_fn_type, new_fn);
             return r;
         }
     }
@@ -926,7 +928,6 @@ struct structural_rec_fn {
     }
 
     void mk_lemmas(expr const & fn, list<expr> const & lemmas) {
-        name const & fn_name = const_name(get_app_fn(fn));
         unsigned eqn_idx     = 1;
         type_context ctx     = mk_type_context();
         for (expr type : lemmas) {
@@ -951,7 +952,9 @@ struct structural_rec_fn {
                 if (local != F)
                     new_locals.push_back(local);
             }
-            m_env = mk_equation_lemma(m_env, m_opts, m_mctx, ctx.lctx(), fn_name,
+            name const & fn_name        = head(m_header.m_fn_names);
+            name const & fn_actual_name = head(m_header.m_fn_actual_names);
+            m_env = mk_equation_lemma(m_env, m_opts, m_mctx, ctx.lctx(), fn_name, fn_actual_name,
                                       eqn_idx, m_header.m_is_private, new_locals, new_lhs, new_rhs);
             eqn_idx++;
         }
diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp
index 063f00287b..e04eae9145 100644
--- a/src/library/equations_compiler/util.cpp
+++ b/src/library/equations_compiler/util.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/scope_pos_info_provider.h"
 #include "kernel/free_vars.h"
 #include "library/util.h"
+#include "library/aliases.h"
 #include "library/trace.h"
 #include "library/app_builder.h"
 #include "library/private.h"
@@ -256,14 +257,6 @@ local_context erase_inaccessible_annotations(local_context const & lctx) {
     return r;
 }
 
-static pair<environment, name> mk_def_name(environment const & env, bool is_private, name const & c) {
-    if (is_private) {
-        return mk_private_name(env, c);
-    } else {
-        return mk_pair(env, c);
-    }
-}
-
 static void throw_mk_aux_definition_error(local_context const & lctx, name const & c, expr const & type, expr const & value, exception & ex) {
     sstream strm;
     strm << "equation compiler failed to create auxiliary declaration '" << c << "'";
@@ -274,7 +267,7 @@ static void throw_mk_aux_definition_error(local_context const & lctx, name const
 }
 
 pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
-                                          equations_header const & header, name const & c, expr const & type, expr const & value) {
+                                          equations_header const & header, name const & c, name const & actual_c, expr const & type, expr const & value) {
     lean_trace("eqn_compiler", tout() << "declaring auxiliary definition\n" << c << " : " << type << "\n";);
     environment new_env = env;
     expr new_type       = type;
@@ -284,8 +277,11 @@ pair<environment, expr> mk_aux_definition(environment const & env, options const
         new_type  = zeta_expand(lctx, new_type);
         new_value = zeta_expand(lctx, new_value);
     }
-    name new_c;
-    std::tie(new_env, new_c) = mk_def_name(env, header.m_is_private, c);
+    name new_c          = actual_c;
+    if (header.m_is_private) {
+        new_env = register_private_name(env, c, actual_c);
+        new_env = add_expr_alias(new_env, c, actual_c);
+    }
     expr r;
     try {
         std::tie(new_env, r) = header.m_is_lemma ?
@@ -330,10 +326,12 @@ static pair<environment, expr> abstract_rhs_nested_proofs(environment const & en
 }
 
 static environment add_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
-                                      bool is_private, name const & f_name, name const & eqn_name, expr const & type, expr const & value) {
+                                      bool is_private, name const & f_name, name const & eqn_name, name const & eqn_actual_name, expr const & type, expr const & value) {
     environment new_env = env;
-    name new_eqn_name;
-    std::tie(new_env, new_eqn_name) = mk_def_name(env, is_private, eqn_name);
+    name new_eqn_name   = eqn_actual_name;
+    if (is_private) {
+        new_env = register_private_name(env, eqn_name, eqn_actual_name);
+    }
     expr r;
     expr new_type  = erase_inaccessible_annotations(type);
     expr new_value = value;
@@ -701,25 +699,26 @@ static expr cleanup_equation_rhs(expr const & rhs) {
 }
 
 environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
-                              name const & f_name, unsigned eqn_idx, bool is_private,
+                              name const & f_name, name const & f_actual_name, unsigned eqn_idx, bool is_private,
                               buffer<expr> const & Hs, expr const & lhs, expr const & rhs) {
     if (!get_eqn_compiler_lemmas(opts)) return env;
     type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
-    expr proof    = prove_eqn_lemma(ctx, Hs, lhs, rhs);
-    expr new_rhs  = cleanup_equation_rhs(rhs);
-    expr type     = ctx.mk_pi(Hs, mk_eq(ctx, lhs, new_rhs));
-    name eqn_name = mk_equation_name(f_name, eqn_idx);
-    return add_equation_lemma(env, opts, mctx, lctx, is_private, f_name, eqn_name, type, proof);
+    expr proof        = prove_eqn_lemma(ctx, Hs, lhs, rhs);
+    expr new_rhs      = cleanup_equation_rhs(rhs);
+    expr type         = ctx.mk_pi(Hs, mk_eq(ctx, lhs, new_rhs));
+    name eqn_name     = mk_equation_name(f_name, eqn_idx);
+    name eqn_actual_name = mk_equation_name(f_actual_name, eqn_idx);
+    return add_equation_lemma(env, opts, mctx, lctx, is_private, f_name, eqn_name, eqn_actual_name, type, proof);
 }
 
-environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, unsigned arity) {
+environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, name const & c_actual, unsigned arity) {
     if (!env.find(get_eq_name())) return env;
     if (!get_eqn_compiler_lemmas(opts)) return env;
-    declaration d = env.get(c);
+    declaration d = env.get(c_actual);
     type_context ctx(env, transparency_mode::All);
     expr type  = d.get_type();
     expr value = d.get_value();
-    expr lhs   = mk_constant(c, param_names_to_levels(d.get_univ_params()));
+    expr lhs   = mk_constant(c_actual, param_names_to_levels(d.get_univ_params()));
     type_context::tmp_locals locals(ctx);
     for (unsigned i = 0; i < arity; i++) {
         type  = ctx.relaxed_whnf(type);
@@ -731,10 +730,11 @@ environment mk_simple_equation_lemma_for(environment const & env, options const
         type   = instantiate(binding_body(type), x);
         value  = instantiate(binding_body(value), x);
     }
-    name eqn_name  = mk_equation_name(c, 1);
-    expr eqn_type  = locals.mk_pi(mk_eq(ctx, lhs, value));
-    expr eqn_proof = locals.mk_lambda(mk_eq_refl(ctx, lhs));
-    return add_equation_lemma(env, opts, metavar_context(), ctx.lctx(), is_private, c, eqn_name, eqn_type, eqn_proof);
+    name eqn_name        = mk_equation_name(c, 1);
+    name eqn_actual_name = mk_equation_name(c_actual, 1);
+    expr eqn_type        = locals.mk_pi(mk_eq(ctx, lhs, value));
+    expr eqn_proof       = locals.mk_lambda(mk_eq_refl(ctx, lhs));
+    return add_equation_lemma(env, opts, metavar_context(), ctx.lctx(), is_private, c_actual, eqn_name, eqn_actual_name, eqn_type, eqn_proof);
 }
 
 bool is_name_value(expr const & e) {
diff --git a/src/library/equations_compiler/util.h b/src/library/equations_compiler/util.h
index a7597d7353..3e5660134e 100644
--- a/src/library/equations_compiler/util.h
+++ b/src/library/equations_compiler/util.h
@@ -82,11 +82,17 @@ bool has_inaccessible_annotation(expr const & e);
 /* See comment at library/local_context.h */
 local_context erase_inaccessible_annotations(local_context const & lctx);
 
-pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
-                                          equations_header const & header, name const & n, expr const & type, expr const & value);
+/* Create an auxiliary definition.
 
+   Remark: `n` is the local name, and `actual_n` the kernel unique name.
+   `n` and `actual_n` are different for scoped/private declarations.
+*/
+pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
+                                          equations_header const & header, name const & n, name const & actual_n, expr const & type, expr const & value);
+
+/* Create an equation lemma #eqn_idx for f_name/f_actual_name. */
 environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
-                              name const & f_name, unsigned eqn_idx, bool is_private,
+                              name const & f_name, name const & f_actual_name, unsigned eqn_idx, bool is_private,
                               buffer<expr> const & Hs, expr const & lhs, expr const & rhs);
 
 /* Create an equational lemma for definition c based on its value.
@@ -97,8 +103,13 @@ environment mk_equation_lemma(environment const & env, options const & opts, met
 
    The proof is by reflexivity.
 
-   This function is used to make sure we have equations for all definitions. */
-environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, unsigned arity);
+   This function is used to make sure we have equations for all definitions.
+
+
+   Remark: `c` is the local name, and `c_actual` the kernel unique name.
+   `c` and `c_actual` are different for scoped/private declarations.
+*/
+environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, name const & c_actual, unsigned arity);
 
 name mk_equation_name(name const & f_name, unsigned eqn_idx);
 
diff --git a/src/library/equations_compiler/wf_rec.cpp b/src/library/equations_compiler/wf_rec.cpp
index 6a9d6e9d9d..29fde8f048 100644
--- a/src/library/equations_compiler/wf_rec.cpp
+++ b/src/library/equations_compiler/wf_rec.cpp
@@ -277,7 +277,8 @@ struct wf_rec_fn {
         expr fn_type = ctx.infer(fn);
         expr r;
         std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, header,
-                                               head(header.m_fn_names), fn_type, fn);
+                                               head(header.m_fn_names), head(header.m_fn_actual_names),
+                                               fn_type, fn);
         return r;
     }
 
@@ -314,8 +315,8 @@ struct wf_rec_fn {
         return mk_lemma_rhs_fn(ctx, fn, F)(rhs);
     }
 
-    void mk_lemmas(expr const & fn, list<expr> const & lemmas) {
-        name const & fn_name = const_name(get_app_fn(fn));
+    void mk_lemmas(name const & fn_name, expr const & fn, list<expr> const & lemmas) {
+        name const & fn_prv_name = const_name(get_app_fn(fn));
         unsigned eqn_idx     = 1;
         type_context ctx     = mk_type_context();
         for (expr type : lemmas) {
@@ -331,7 +332,7 @@ struct wf_rec_fn {
             expr new_lhs = mk_app(fn, app_arg(lhs));
             expr new_rhs = mk_lemma_rhs(ctx, fn, rhs);
             trace_debug_wf_aux(tout() << "aux equation [" << eqn_idx << "]:\n" << new_lhs << "\n=\n" << new_rhs << "\n";);
-            m_env = mk_equation_lemma(m_env, m_opts, m_mctx, ctx.lctx(), fn_name,
+            m_env = mk_equation_lemma(m_env, m_opts, m_mctx, ctx.lctx(), fn_name, fn_prv_name,
                                       eqn_idx, m_header.m_is_private, locals.as_buffer(), new_lhs, new_rhs);
             eqn_idx++;
         }
@@ -427,7 +428,8 @@ struct wf_rec_fn {
     eqn_compiler_result unpack(expr const & packed_fn, expr const & eqns_before_pack,
                                list<list<expr>> const & counter_example_args) {
         equations_header const & header = get_equations_header(eqns_before_pack);
-        list<name> fn_names = header.m_fn_names;
+        list<name> fn_names     = header.m_fn_names;
+        list<name> fn_actual_names = header.m_fn_actual_names;
         type_context ctx = mk_type_context();
         buffer<expr> result_fns;
         expr packed_fn_type = ctx.relaxed_whnf(ctx.infer(packed_fn));
@@ -445,14 +447,17 @@ struct wf_rec_fn {
                 expr arg = args.push_local_from_binding(it);
                 it = instantiate(binding_body(it), arg);
             }
-            expr sigma_mk   = mk_sigma(ctx, 0, args.as_buffer()).first;
-            expr packed_arg = mk_mutual_arg(ctx, sigma_mk, fidx, num_fns, packed_domain);
-            expr fn_val     = args.mk_lambda(mk_app(packed_fn, packed_arg));
-            name fn_name    = head(fn_names);
-            fn_names        = tail(fn_names);
+            expr sigma_mk       = mk_sigma(ctx, 0, args.as_buffer()).first;
+            expr packed_arg     = mk_mutual_arg(ctx, sigma_mk, fidx, num_fns, packed_domain);
+            expr fn_val         = args.mk_lambda(mk_app(packed_fn, packed_arg));
+            name fn_name        = head(fn_names);
+            name fn_actual_name = head(fn_actual_names);
+            fn_names            = tail(fn_names);
+            fn_actual_names     = tail(fn_actual_names);
             trace_debug_wf(tout() << fn_name << " := " << fn_val << "\n";);
             expr r;
-            std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, header, fn_name, fn_type, fn_val);
+            std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, header, fn_name, fn_actual_name,
+                                                   fn_type, fn_val);
             result_fns.push_back(r);
         }
         ctx.set_env(m_env);
@@ -530,9 +535,10 @@ struct wf_rec_fn {
         if (header.m_num_fns > 1) {
             eqns = pack_mutual(eqns);
         } else {
-            equations_header new_header = header;
-            new_header.m_fn_names       = to_list(name(head(header.m_fn_names), "_pack"));
-            eqns                        = update_equations(eqns, new_header);
+            equations_header new_header   = header;
+            new_header.m_fn_names         = to_list(name(head(header.m_fn_names), "_pack"));
+            new_header.m_fn_actual_names  = to_list(name(head(header.m_fn_actual_names), "_pack"));
+            eqns                          = update_equations(eqns, new_header);
         }
 
         /* Retrieve well founded relation */
@@ -556,7 +562,9 @@ struct wf_rec_fn {
         trace_debug_wf(tout() << "after mk_fix\n" << fn << " :\n  " << mk_type_context().infer(fn) << "\n";);
         if (m_header.m_aux_lemmas) {
             lean_assert(!m_header.m_is_meta);
-            mk_lemmas(fn, r.m_lemmas);
+            equations_header const & header = get_equations_header(eqns);
+            name const & fn_name = head(header.m_fn_names);
+            mk_lemmas(fn_name, fn, r.m_lemmas);
         }
 
         return unpack(fn, before_pack, r.m_counter_examples);
diff --git a/src/library/private.cpp b/src/library/private.cpp
index d64939712b..3254ed2208 100644
--- a/src/library/private.cpp
+++ b/src/library/private.cpp
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include <string>
 #include "util/hash.h"
+#include "util/sstream.h"
 #include "library/private.h"
 #include "library/module.h"
 #include "library/fingerprint.h"
@@ -15,6 +16,9 @@ namespace lean {
 struct private_ext : public environment_extension {
     unsigned       m_counter;
     name_map<name> m_inv_map;  // map: hidden-name -> user-name
+    /* We store private prefixes to make sure register_private_name is used correctly.
+       This information does not need to be stored in .olean files. */
+    name_set       m_private_prefixes;
     private_ext():m_counter(0) {}
 };
 
@@ -60,21 +64,26 @@ struct private_modification : public modification {
     }
 };
 
-// Make sure the mapping "hidden-name r ==> user-name n" is preserved when we close sections and
-// export .olean files.
+/* Make sure the mapping "hidden-name r ==> user-name n" is preserved when we close sections and
+   export .olean files. */
 static environment preserve_private_data(environment const & env, name const & r, name const & n) {
     return module::add(env, std::make_shared<private_modification>(n, r));
 }
 
-pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
-    private_ext ext = get_extension(env);
-    unsigned h      = hash(n.hash(), ext.m_counter);
-    uint64   f      = get_fingerprint(env);
-    h               = hash(h, static_cast<unsigned>(f >> 32));
-    h               = hash(h, static_cast<unsigned>(f));
+static name mk_private_name_core(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
+    private_ext const & ext = get_extension(env);
+    unsigned h              = hash(n.hash(), ext.m_counter);
+    uint64   f              = get_fingerprint(env);
+    h                       = hash(h, static_cast<unsigned>(f >> 32));
+    h                       = hash(h, static_cast<unsigned>(f));
     if (extra_hash)
         h = hash(h, *extra_hash);
-    name r = name(*g_private, h) + n;
+    return name(*g_private, h) + n;
+}
+
+pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
+    name r          = mk_private_name_core(env, n, extra_hash);
+    private_ext ext = get_extension(env);
     ext.m_inv_map.insert(r, n);
     ext.m_counter++;
     environment new_env = update(env, ext);
@@ -82,6 +91,69 @@ pair<environment, name> add_private_name(environment const & env, name const & n
     return mk_pair(new_env, r);
 }
 
+static unsigned mk_extra_hash_using_pos() {
+    unsigned h = 31;
+    if (auto pinfo = get_pos_info_provider()) {
+        h = hash(pinfo->get_some_pos().first, pinfo->get_some_pos().second);
+        char const * fname = pinfo->get_file_name();
+        h = hash_str(strlen(fname), fname, h);
+    }
+    return h;
+}
+
+pair<environment, name> mk_private_name(environment const & env, name const & c) {
+    return add_private_name(env, c, optional<unsigned>(mk_extra_hash_using_pos()));
+}
+
+pair<environment, name> mk_private_prefix(environment const & env, optional<unsigned> const & extra_hash) {
+    name r          = mk_private_name_core(env, name(), extra_hash);
+    private_ext ext = get_extension(env);
+    ext.m_private_prefixes.insert(r);
+    ext.m_counter++;
+    environment new_env = update(env, ext);
+    return mk_pair(new_env, r);
+}
+
+pair<environment, name> mk_private_prefix(environment const & env) {
+    return mk_private_prefix(env, optional<unsigned>(mk_extra_hash_using_pos()));
+}
+
+static optional<name> get_private_prefix(private_ext const & ext, name n) {
+    while (true) {
+        if (ext.m_private_prefixes.contains(n))
+            return optional<name>(n);
+        if (n.is_atomic())
+            return optional<name>();
+        n = n.get_prefix();
+    }
+}
+
+/* Return true iff a prefix of `n` is registered as a private prefix in `ext` */
+static bool has_private_prefix(private_ext const & ext, name n) {
+    return static_cast<bool>(get_private_prefix(ext, n));
+}
+
+optional<name> get_private_prefix(environment const & env, name const & n) {
+    private_ext const & ext = get_extension(env);
+    return get_private_prefix(ext, n);
+}
+
+bool has_private_prefix(environment const & env, name const & n) {
+    private_ext const & ext = get_extension(env);
+    return has_private_prefix(ext, n);
+}
+
+environment register_private_name(environment const & env, name const & n, name const & prv_n) {
+    private_ext ext = get_extension(env);
+    if (!has_private_prefix(ext, prv_n)) {
+        /* TODO(Leo): consider using an assertion */
+        throw exception(sstream() << "failed to register private name '" << prv_n << "', prefix has not been registered");
+    }
+    ext.m_inv_map.insert(prv_n, n);
+    environment new_env = update(env, ext);
+    return preserve_private_data(new_env, prv_n, n);
+}
+
 optional<name> hidden_to_user_name(environment const & env, name const & n) {
     auto it = get_extension(env).m_inv_map.find(n);
     return it ? optional<name>(*it) : optional<name>();
@@ -91,16 +163,6 @@ bool is_private(environment const & env, name const & n) {
     return static_cast<bool>(hidden_to_user_name(env, n));
 }
 
-pair<environment, name> mk_private_name(environment const & env, name const & c) {
-    unsigned h = 31;
-    if (auto pinfo = get_pos_info_provider()) {
-        h = hash(pinfo->get_some_pos().first, pinfo->get_some_pos().second);
-        char const * fname = pinfo->get_file_name();
-        h = hash_str(strlen(fname), fname, h);
-    }
-    return add_private_name(env, c, optional<unsigned>(h));
-}
-
 void initialize_private() {
     g_ext     = new private_ext_reg();
     g_private = new name("_private");
diff --git a/src/library/private.h b/src/library/private.h
index 934374cbaf..749ae8c1fe 100644
--- a/src/library/private.h
+++ b/src/library/private.h
@@ -32,9 +32,28 @@ optional<name> hidden_to_user_name(environment const & env, name const & n);
 
 bool is_private(environment const & env, name const & n);
 
+pair<environment, name> mk_private_prefix(environment const & env, name const & n, optional<unsigned> const & base_hash);
+
 /* Create a private name based on \c c and get_pos_info_provider(), and register it using \c add_private_name */
 pair<environment, name> mk_private_name(environment const & env, name const & c);
 
+/* Create a private prefix that is going to be use to generate many private names.
+   This function registers the private prefix in the environment. */
+pair<environment, name> mk_private_prefix(environment const & env, optional<unsigned> const & extra_hash);
+
+/* Similar to the previous function, but generate an extra_hash using get_pos_info_provider */
+pair<environment, name> mk_private_prefix(environment const & env);
+
+/* Register a \c n as the name for private name \c prv_n. \c prv_n must have been constructed using
+   a prefix returned by \c mk_private_prefix. */
+environment register_private_name(environment const & env, name const & n, name const & prv_n);
+
+/* Return true iff a prefix of `n` is registered as a private prefix in the given environment. */
+bool has_private_prefix(environment const & env, name const & n);
+
+/* Return some name iff a prefix of `n` is registered as a private prefix in the given environment. */
+optional<name> get_private_prefix(environment const & env, name const & n);
+
 void initialize_private();
 void finalize_private();
 }
diff --git a/tests/lean/run/1804a.lean b/tests/lean/run/1804a.lean
new file mode 100644
index 0000000000..3c7cf69337
--- /dev/null
+++ b/tests/lean/run/1804a.lean
@@ -0,0 +1,62 @@
+section
+parameter P : match unit.star with
+| unit.star := true
+end
+
+include P
+
+example : false :=
+begin
+  dsimp [_match_1] at P,
+  guard_hyp P := true,
+  admit
+end
+end
+
+section
+parameter P : match unit.star with
+| unit.star := true
+end
+
+include P
+
+example : false :=
+begin
+  dsimp [_match_1] at P,
+  guard_hyp P := true,
+  admit
+end
+end
+
+
+section
+parameter P : match unit.star with
+| unit.star := true
+end
+
+parameter Q : match unit.star with
+| unit.star := true
+end
+
+section
+include P
+
+example : false :=
+begin
+  dsimp [_match_1] at P,
+  guard_hyp P := true,
+  admit
+end
+end
+
+section
+include Q
+example : false :=
+begin
+  dsimp [_match_2] at Q,
+  guard_hyp Q := true,
+  admit
+end
+end
+
+end
diff --git a/tests/lean/run/1804b.lean b/tests/lean/run/1804b.lean
new file mode 100644
index 0000000000..532d2fc442
--- /dev/null
+++ b/tests/lean/run/1804b.lean
@@ -0,0 +1,41 @@
+namespace bla
+
+private def foo (x : nat) : nat :=
+match x with
+| 0 := 1
+| _ := 2
+end
+
+example (a : nat) (h : a = foo 0) : a = 1 :=
+begin
+  simp [foo] at h,
+  guard_hyp h := a = 1,
+  exact h
+end
+
+example (a b : nat) (p : b = 0) (h : a = foo b) : a = 1 :=
+begin
+  simp [foo] at h,
+  simp [p] at h,
+  simp [foo._match_1] at h,
+  guard_hyp h := a = 1,
+  exact h
+end
+
+example (a b : nat) (p : b = 0) (h : a = foo b) : a = 1 :=
+begin
+  simp [foo] at h,
+  simp [p] at h,
+  simp [foo] at h,
+  guard_hyp h := a = 1,
+  exact h
+end
+
+example (a b : nat) (p : b = 0) (h : a = foo b) : a = 1 :=
+begin
+  simp [foo, p] at h,
+  guard_hyp h := a = 1,
+  exact h
+end
+
+end bla
diff --git a/tests/lean/run/let3.lean b/tests/lean/run/let3.lean
index ac3e977f10..87315a5524 100644
--- a/tests/lean/run/let3.lean
+++ b/tests/lean/run/let3.lean
@@ -1,4 +1,3 @@
-
 definition p1 := (10, 20, 30)
 
 definition v1 : nat :=
@@ -44,3 +43,9 @@ in c + d
 
 example : v3 = 50 :=
 rfl
+
+#check
+(let (a, b, c) := p1 in a + b : nat) -- We have to provide the type.
+
+#reduce
+(let (a, b, c) := p1 in a + b : nat) -- We have to provide the type.