From 6143cb66182636d7472d8ad7a865e9706ece57d2 Mon Sep 17 00:00:00 2001
From: Francisco Giordano <fg@frang.io>
Date: Sat, 23 May 2026 19:22:21 -0300
Subject: [PATCH] Move replace tactic next to have

---
 Manual/Tactics.lean           | 3 +++
 Manual/Tactics/Reference.lean | 3 ---
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean
index a98a167cd..874d9e8b3 100644
--- a/Manual/Tactics.lean
+++ b/Manual/Tactics.lean
@@ -866,6 +866,9 @@ Generally speaking, {tactic}`have` should be used when proving an intermediate l
 :::tactic Lean.Parser.Tactic.tacticHave'
 :::
 
+:::tactic "replace"
+:::
+
 :::tactic Lean.Parser.Tactic.tacticLet__ (show := "let")
 :::
 
diff --git a/Manual/Tactics/Reference.lean b/Manual/Tactics/Reference.lean
index e37302993..73e3b2de9 100644
--- a/Manual/Tactics/Reference.lean
+++ b/Manual/Tactics/Reference.lean
@@ -319,9 +319,6 @@ tag := "tactic-ref-rw"
 Implemented by {name}`Lean.Elab.Tactic.evalUnfold`.
 :::
 
-:::tactic "replace"
-:::
-
 :::tactic "delta"
 :::