diff --git a/src/Lean/Elab/Tactic/Conv/Delta.lean b/src/Lean/Elab/Tactic/Conv/Delta.lean
index 2761d93828..c018b33ebb 100644
--- a/src/Lean/Elab/Tactic/Conv/Delta.lean
+++ b/src/Lean/Elab/Tactic/Conv/Delta.lean
@@ -11,7 +11,7 @@ open Meta
 
 @[builtinTactic Lean.Parser.Tactic.Conv.delta] def evalDelta : Tactic := fun stx => withMainContext do
   let declName ← resolveGlobalConstNoOverload stx[1]
-  let lhsNew ← deltaExpand (← getLhs) (· == declName)
+  let lhsNew ← deltaExpand (← instantiateMVars (← getLhs)) (· == declName)
   changeLhs lhsNew
 
 end Lean.Elab.Tactic.Conv