diff --git a/src/Lean/Elab/Tactic/Change.lean b/src/Lean/Elab/Tactic/Change.lean
index 88676a707943..1b891415f78d 100644
--- a/src/Lean/Elab/Tactic/Change.lean
+++ b/src/Lean/Elab/Tactic/Change.lean
@@ -13,6 +13,22 @@ open Meta
 # Implementation of the `change` tactic
 -/
 
+/-- Elaborates the pattern `p` and ensures that it is defeq to `e`. -/
+def elabChange (e : Expr) (p : Term) : TacticM Expr := do
+  let mvarCounterSaved := (← getMCtx).mvarCounter
+  let p ← elabTermEnsuringType p (← inferType e) (mayPostpone := true)
+  -- Discretionary `isDefEq` before synthesizing remaining metavariables. Save the result to avoid a final `isDefEq` check if it passes.
+  let defeq ← isDefEq p e
+  Term.synthesizeSyntheticMVarsNoPostponing
+  withAssignableSyntheticOpaque do
+    unless ← pure defeq <||> isDefEq p e do
+      let (p, tgt) ← addPPExplicitToExposeDiff p e
+      throwError "\
+        'change' tactic failed, pattern{indentExpr p}\n\
+        is not definitionally equal to target{indentExpr tgt}"
+    logUnassignedAndAbort (← filterOldMVars (← getMVars p) mvarCounterSaved)
+    instantiateMVars p
+
 /-- `change` can be used to replace the main goal or its hypotheses with
 different, yet definitionally equal, goal or hypotheses.
 
@@ -38,15 +54,13 @@ the main goal. -/
   | `(tactic| change $newType:term $[$loc:location]?) => do
     withLocation (expandOptLocation (Lean.mkOptionalNode loc))
       (atLocal := fun h => do
-        let hTy ← h.getType
-        -- This is a hack to get the new type to elaborate in the same sort of way that
-        -- it would for a `show` expression for the goal.
-        let mvar ← mkFreshExprMVar none
-        let (_, mvars) ← elabTermWithHoles
-                          (← `(term | show $newType from $(← Term.exprToSyntax mvar))) hTy `change
-        liftMetaTactic fun mvarId => do
-          return (← mvarId.changeLocalDecl h (← inferType mvar)) :: mvars)
-      (atTarget := evalTactic <| ← `(tactic| refine_lift show $newType from ?_))
-      (failed := fun _ => throwError "change tactic failed")
+        let hTy' ← elabChange (← h.getType) newType
+        liftMetaTactic1 fun mvarId => do
+          mvarId.changeLocalDecl h hTy')
+      (atTarget := do
+        let tgt' ← elabChange (← getMainTarget) newType
+        liftMetaTactic1 fun mvarId => do
+          mvarId.replaceTargetDefEq tgt')
+      (failed := fun _ => throwError "'change' tactic failed")
 
 end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/Tactic/Conv/Change.lean b/src/Lean/Elab/Tactic/Conv/Change.lean
index 9385d9e9cddb..ca0e5c1154a9 100644
--- a/src/Lean/Elab/Tactic/Conv/Change.lean
+++ b/src/Lean/Elab/Tactic/Conv/Change.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Change
 import Lean.Elab.Tactic.Conv.Basic
 
 namespace Lean.Elab.Tactic.Conv
@@ -14,12 +15,8 @@ open Meta
   match stx with
   | `(conv| change $e) => withMainContext do
     let lhs ← getLhs
-    let mvarCounterSaved := (← getMCtx).mvarCounter
-    let r ← elabTermEnsuringType e (← inferType lhs)
-    logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
-    unless (← isDefEqGuarded r lhs) do
-      throwError "invalid 'change' conv tactic, term{indentExpr r}\nis not definitionally equal to current left-hand-side{indentExpr lhs}"
-    changeLhs r
+    let lhs' ← elabChange lhs e
+    changeLhs lhs'
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.Conv
diff --git a/tests/lean/run/change.lean b/tests/lean/run/change.lean
index 04fa47c287b2..30ac199815f6 100644
--- a/tests/lean/run/change.lean
+++ b/tests/lean/run/change.lean
@@ -2,7 +2,19 @@
 private axiom test_sorry : ∀ {α}, α
 
 set_option linter.missingDocs false
-set_option autoImplicit true
+set_option pp.mvars false
+
+/-!
+`conv` failure
+-/
+/--
+error: 'change' tactic failed, pattern
+  m = ?_
+is not definitionally equal to target
+  n = m
+-/
+#guard_msgs in example : n = m := by
+  change m = _
 
 example : n + 2 = m := by
   change n + 1 + 1 = _
@@ -41,7 +53,6 @@ noncomputable example : Nat := by
 def foo (a b c : Nat) := if a < b then c else 0
 
 example : foo 1 2 3 = 3 := by
-  change (if _ then _ else _) = _
   change ite _ _ _ = _
   change (if _ < _ then _ else _) = _
   change _ = (if true then 3 else 4)
@@ -53,7 +64,7 @@ example (h : foo 1 2 3 = 4) : True := by
   trivial
 
 example (h : foo 1 2 3 = 4) : True := by
-  change (if _ then _ else _) = _ at h
+  change ite _ _ _ = _ at h
   guard_hyp h : (if 1 < 2 then 3 else 0) = 4
   trivial
 
@@ -65,16 +76,116 @@ example (α : Type) [LT α] (x : α) (h : x < x) : x < id x := by
   guard_target =ₛ x < x
   exact h
 
--- This example shows using named and anonymous placeholders to create a new goal.
+/-!
+`change` can create new metavariables and assign them
+-/
+/--
+info: x y z : Nat
+w : Nat := x + y
+⊢ x + y = z
+-/
+#guard_msgs in
+example (x y z : Nat) : x + y = z := by
+  change ?a = _
+  let w := ?a
+  trace_state
+  exact test_sorry
+
+/-!
+`change` is not allowed to create new goals
+-/
+/--
+error: don't know how to synthesize placeholder for argument 'e'
+context:
+case z
+x y : Nat
+h : x = y
+⊢ Nat
+---
+error: unsolved goals
+x y : Nat
+h : x = y
+⊢ True
+-/
+#guard_msgs in
 example (x y : Nat) (h : x = y) : True := by
-  change (if 1 < 2 then x else ?z + ?_) = y at h
-  rotate_left
-  · exact 4
-  · exact 37
-  guard_hyp h : (if 1 < 2 then x else 4 + 37) = y
-  · trivial
+  change (if 1 < 2 then x else ?z) = y at h
 
 example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 := by
   intro x y z -- `z` was previously erroneously marked as unused
   change _ at y
   exact z.2
+
+/-!
+`change` reorders hypotheses if necessary
+-/
+/--
+info: x y z w : Nat
+a : Nat := x + y
+h : a = z + w
+⊢ True
+-/
+#guard_msgs in
+example (x y z w : Nat) (h : x + y = z + w) : True := by
+  let a := x + y
+  change a = _ at h
+  trace_state
+  trivial
+
+/-!
+## Conv `change`
+-/
+
+/-!
+conv `change` test
+-/
+example (m n : Nat) : m + 2 = n := by
+  conv => enter [1]; change m + (1 + 1)
+  guard_target =ₛ m + (1 + 1) = n
+  exact test_sorry
+
+/-!
+conv `change` test failure
+-/
+/--
+error: 'change' tactic failed, pattern
+  m + n
+is not definitionally equal to target
+  m + 2
+-/
+#guard_msgs in
+example (m n : Nat) : m + 2 = n := by
+  conv => enter [1]; change m + n
+
+/-!
+conv `change` unsolved metavariables
+-/
+/--
+error: don't know how to synthesize placeholder for argument 'e'
+context:
+case a
+m n : Nat
+⊢ Nat
+---
+error: unsolved goals
+m n : Nat
+⊢ m + 2 = n
+-/
+#guard_msgs in
+example (m n : Nat) : m + 2 = n := by
+  conv => enter [1]; change if True then m + 2 else ?a
+
+/-!
+conv `change` to create a metavariable
+-/
+/--
+info: a b c d : Nat
+e : Nat := a + b
+⊢ a + b + c = d
+-/
+#guard_msgs in
+example (a b c d : Nat) : a + b + c = d := by
+  conv => enter [1,1]; change ?mvar
+  let e := ?mvar
+  trace_state
+  exact test_sorry
diff --git a/tests/lean/run/change_tac.lean b/tests/lean/run/change_tac.lean
deleted file mode 100644
index e8b214f18ce9..000000000000
--- a/tests/lean/run/change_tac.lean
+++ /dev/null
@@ -1,76 +0,0 @@
-private axiom test_sorry : ∀ {α}, α
-
-example : n + 2 = m := by
-  change n + 1 + 1 = _
-  guard_target =ₛ n + 1 + 1 = m
-  exact test_sorry
-
-example (h : n + 2 = m) : False := by
-  change _ + 1 = _ at h
-  guard_hyp h :ₛ n + 1 + 1 = m
-  exact test_sorry
-
-example : n + 2 = m := by
-  fail_if_success change true
-  fail_if_success change _ + 3 = _
-  fail_if_success change _ * _ = _
-  change (_ : Nat) + _ = _
-  exact test_sorry
-
--- `change ... at ...` allows placeholders to mean different things at different hypotheses
-example (h : n + 3 = m) (h' : n + 2 = m) : False := by
-  change _ + 1 = _ at h h'
-  guard_hyp h :ₛ n + 2 + 1 = m
-  guard_hyp h' :ₛ n + 1 + 1 = m
-  exact test_sorry
-
--- `change ... at ...` preserves dependencies
-example (p : n + 2 = m → Type) (h : n + 2 = m) (x : p h) : false := by
-  change _ + 1 = _ at h
-  guard_hyp x :ₛ p h
-  exact test_sorry
-
-noncomputable example : Nat := by
-  fail_if_success change Type 1
-  exact test_sorry
-
-def foo (a b c : Nat) := if a < b then c else 0
-
-example : foo 1 2 3 = 3 := by
-  change (if _ then _ else _) = _
-  change ite _ _ _ = _
-  change (if _ < _ then _ else _) = _
-  change _ = (if true then 3 else 4)
-  rfl
-
-example (h : foo 1 2 3 = 4) : True := by
-  change ite _ _ _ = _ at h
-  guard_hyp h :ₛ ite (1 < 2) 3 0 = 4
-  trivial
-
-example (h : foo 1 2 3 = 4) : True := by
-  change (if _ then _ else _) = _ at h
-  guard_hyp h : (if 1 < 2 then 3 else 0) = 4
-  trivial
-
-example (α : Type) [LT α] (x : α) (h : x < x) : x < id x := by
-  change _ < _ -- can defer LT typeclass lookup, just like `show`
-  change _ < _ at h -- can defer LT typeclass lookup at h too
-  guard_target =ₛ x < id x
-  change _ < x
-  guard_target =ₛ x < x
-  exact h
-
--- This example shows using named and anonymous placeholders to create a new goal.
-example (x y : Nat) (h : x = y) : True := by
-  change (if 1 < 2 then x else ?z + ?_) = y at h
-  rotate_left
-  · exact 4
-  · exact 37
-  guard_hyp h : (if 1 < 2 then x else 4 + 37) = y
-  · trivial
-
-example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 := by
-  intro x y z -- `z` was previously erroneously marked as unused
-  change _ at y
-  exact z.2