diff --git a/src/Lean/Elab/Tactic/Conv/Change.lean b/src/Lean/Elab/Tactic/Conv/Change.lean
index f7f2b10c33..3930f7a997 100644
--- a/src/Lean/Elab/Tactic/Conv/Change.lean
+++ b/src/Lean/Elab/Tactic/Conv/Change.lean
@@ -11,7 +11,7 @@ open Meta
 
 @[builtinTactic Lean.Parser.Tactic.Conv.change] def evalChange : Tactic := fun stx => do
   match stx with
-  | `(conv| change $e) => do
+  | `(conv| change $e) => withMainContext do
     let lhs ← getLhs
     let mvarCounterSaved := (← getMCtx).mvarCounter
     let r ← elabTermEnsuringType e (← inferType lhs)
diff --git a/tests/lean/run/1558.lean b/tests/lean/run/1558.lean
new file mode 100644
index 0000000000..b2b7f6aa28
--- /dev/null
+++ b/tests/lean/run/1558.lean
@@ -0,0 +1,5 @@
+example : (λ (u : Nat) => u + 0) = id :=by
+  conv =>
+    lhs
+    intro u
+    change u