chore(Tactic): make the (deprecated) replace syntax a @[tactic_alt] (leanprover-community#37931)

This PR replaces the tactic docstring for Mathlib's version of `replace` with a `@[tactic_alt]` attribute + `tactic_extension`. Also update the module docs which did not get updated when `replace` got upstreamed to core Lean.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

Author: Vierkantor

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