diff --git a/src/Lean/Elab/Tactic/Conv/Rewrite.lean b/src/Lean/Elab/Tactic/Conv/Rewrite.lean
index 009b10f408..9f8803b35c 100644
--- a/src/Lean/Elab/Tactic/Conv/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Conv/Rewrite.lean
@@ -16,6 +16,7 @@ def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx =>
       let e ← elabTerm term none true
       let r ← rewrite (← getMainGoal) (← getLhs) e symm (mode := mode)
       updateLhs r.eNew r.eqProof
+      replaceMainGoal ((← getMainGoal) :: r.mvarIds)
 
 @[builtinTactic Lean.Parser.Tactic.Conv.rewrite] def evalRewrite : Tactic :=
   evalRewriteCore TransparencyMode.instances