diff --git a/Mathlib/Tactic/Replace.lean b/Mathlib/Tactic/Replace.lean
index fe00568ccd2ac5..671f4bfb873d08 100644
--- a/Mathlib/Tactic/Replace.lean
+++ b/Mathlib/Tactic/Replace.lean
@@ -10,8 +10,8 @@ public import Mathlib.Tactic.Have
 /-!
 # Extending `replace`
 
-This file extends the `replace` tactic from `Batteries` to allow the addition of hypotheses to
-the context without requiring their proofs to be provided immediately.
+This file extends the `replace` tactic from the standard library to allow the addition of hypotheses
+to the context without requiring their proofs to be provided immediately.
 
 As a style choice, this should not be used in mathlib; but is provided for downstream users who
 preferred the old style.
@@ -24,36 +24,12 @@ namespace Mathlib.Tactic
 open Lean Elab.Tactic
 
 /--
-Acts like `have`, but removes a hypothesis with the same name as
-this one if possible. For example, if the state is:
-
-Then after `replace h : β` the state will be:
-
-```lean
-case h
-f : α → β
-h : α
-⊢ β
-
-f : α → β
-h : β
-⊢ goal
-```
-
-whereas `have h : β` would result in:
-
-```lean
-case h
-f : α → β
-h : α
-⊢ β
-
-f : α → β
-h✝ : α
-h : β
-⊢ goal
-```
+`replace h : t`, without a subsequent proof, creates a new main goal `case h : ... ⊢ t`.
+This form is considered deprecated in Mathlib: use `replace h : t := _` instead.
 -/
+tactic_extension Lean.Parser.Tactic.replace
+
+@[tactic_alt Lean.Parser.Tactic.replace]
 syntax (name := replace') "replace" haveIdLhs' : tactic
 
 elab_rules : tactic