diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 1e2ca7f84..2c75929f7 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -400,10 +400,11 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
         if (p.curr_is_token(get_with_tk())) {
             while (p.curr_is_token(get_with_tk())) {
                 p.next();
+                auto pos = p.pos();
                 name g_name = p.check_id_next("invalid declaration, identifier expected");
                 p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
                 expr g_type = p.parse_expr();
-                expr g      = mk_local(g_name, g_type);
+                expr g      = p.save_pos(mk_local(g_name, g_type), pos);
                 auxs.push_back(g_name);
                 fns.push_back(g);
             }
@@ -435,13 +436,14 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
             }
             validate_equation_lhs(p, lhs, locals);
             lhs = merge_equation_lhs_vars(lhs, locals);
+            auto assign_pos = p.pos();
             p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
             {
                 parser::local_scope scope2(p);
                 for (expr const & local : locals)
                     p.add_local(local);
                 expr rhs = p.parse_expr();
-                eqns.push_back(Fun(fns, Fun(locals, mk_equation(lhs, rhs), p)));
+                eqns.push_back(Fun(fns, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p)));
             }
             if (!p.curr_is_token(get_comma_tk()))
                 break;
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index cf7efcf30..3ffd57193 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1058,7 +1058,7 @@ expr elaborator::visit_equation(expr const & eq, constraint_seq & cs) {
     pair<expr, constraint_seq> new_rhs_cs = ensure_has_type(new_rhs, rhs_type, lhs_type, j, m_relax_main_opaque);
     new_rhs = new_rhs_cs.first;
     cs     += new_rhs_cs.second;
-    return mk_equation(new_lhs, new_rhs);
+    return copy_tag(eq, mk_equation(new_lhs, new_rhs));
 }
 
 expr elaborator::visit_inaccessible(expr const & e, constraint_seq & cs) {