diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
index 9f52fe3546..ecb83fefef 100644
--- a/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -51,7 +51,7 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
         let term := rule[1]
         let processId (id : Syntax) : TacticM Unit := do
           -- See if we can interpret `id` as a hypothesis first.
-          if (← optional <| getFVarId id).isSome then
+          if (← withMainContext <| Term.isLocalIdent? id).isSome then
             x symm term
           else
             -- Try to get equation theorems for `id`.
@@ -62,8 +62,8 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
             let rec go : List Name →  TacticM Unit
               | [] => throwError "failed to rewrite using equation theorems for '{declName}'.{hint}"
               | eqThm::eqThms => (x symm (mkCIdentFrom id eqThm)) <|> go eqThms
-            go eqThms.toList
             discard <| Term.addTermInfo id (← mkConstWithFreshMVarLevels declName) (lctx? := ← getLCtx)
+            go eqThms.toList
         match term with
         | `($id:ident)  => processId id
         | `(@$id:ident) => processId id
diff --git a/tests/lean/interactive/rwElabConst.lean b/tests/lean/interactive/rwElabConst.lean
new file mode 100644
index 0000000000..beec4acb25
--- /dev/null
+++ b/tests/lean/interactive/rwElabConst.lean
@@ -0,0 +1,21 @@
+import Lean
+
+/-!
+Previously, `rw [my_lemma]` would elaborate `my_lemma` twice, both times generating new universe metavariables.
+This caused the "Expected type" to contain a universe metavariable that wasn't in the metavariable context.
+
+This test verifies that the generated universe level is in the metavariable context.
+-/
+
+open Lean PrettyPrinter Delaborator SubExpr
+/-- No-op delaborator that checks that the universe level is in the metavariable context -/
+@[delab app.Eq]
+def checkUniv : Delab := do
+  let .const _ [.mvar u] := (← getExpr).getAppFn | failure
+  _ ← u.getLevel -- if `u` isn't in the metavariable context, this throws an error during elaboration
+  failure
+
+example : True := by
+  try rw [eq_self]
+          --^ $/lean/plainTermGoal
+  trivial
diff --git a/tests/lean/interactive/rwElabConst.lean.expected.out b/tests/lean/interactive/rwElabConst.lean.expected.out
new file mode 100644
index 0000000000..b49a64f1da
--- /dev/null
+++ b/tests/lean/interactive/rwElabConst.lean.expected.out
@@ -0,0 +1,5 @@
+{"textDocument": {"uri": "file:///rwElabConst.lean"},
+ "position": {"line": 18, "character": 12}}
+{"range":
+ {"start": {"line": 18, "character": 10}, "end": {"line": 18, "character": 17}},
+ "goal": "⊢ ∀ {α : Sort ?u} (a : α), (a = a) = True"}