diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index e002da543..d596a399c 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2395,7 +2395,7 @@ static expr translate_local_name(environment const & env,
 */
 static expr translate(environment const & env, list<expr> const & ctx, expr const & e) {
     auto fn = [&](expr const & e) {
-        if (is_placeholder(e) || is_by(e)) {
+        if (is_placeholder(e) || is_by(e) || is_by_plus(e)) {
             return some_expr(e); // ignore placeholders
         } else if (is_constant(e)) {
             expr new_e = copy_tag(e, translate_local_name(env, ctx, const_name(e), e));
diff --git a/tests/lean/run/982.lean b/tests/lean/run/982.lean
new file mode 100644
index 000000000..1f1271ecf
--- /dev/null
+++ b/tests/lean/run/982.lean
@@ -0,0 +1,18 @@
+import data.nat
+open nat
+
+constant P : nat → Prop
+
+example (Hex : ∃ n, P n) : true :=
+  obtain n Hn, from Hex,
+  begin+
+    note Hn2 := Hn,
+    exact trivial
+  end
+
+example (Hex : ∃ n, P n) : true :=
+  obtain n Hn, from Hex,
+  begin+
+    have H : n ≥ 0, from sorry,
+    exact trivial
+  end