chore: deprecate memoFix and replaceRec (leanprover-community#34384)

This deprecation was requested by Floris van Doorn in leanprover-community#33236

Author: JovanGerb

Mathlib/Lean/Expr.lean

@@ -6,4 +6,6 @@ Authors: Mario Carneiro, Simon Hudon, Kim Morrison, Keeley Hoek, Robert Y. Lewis
 module
 
 public import Mathlib.Lean.Expr.Basic
-public import Mathlib.Lean.Expr.ReplaceRec
+public import Mathlib.Tactic.Linter.DeprecatedModule
+
+deprecated_module (since := "2026-01-27")

Mathlib/Lean/Expr/ReplaceRec.lean

@@ -8,6 +8,7 @@ module
 
 public import Lean.Expr
 public import Mathlib.Util.MemoFix
+public import Mathlib.Tactic.Linter.DeprecatedModule
 
 /-!
 # ReplaceRec
@@ -16,6 +17,10 @@ We define a more flexible version of `Expr.replace` where we can use recursive c
 replacing a subexpression. We completely mimic the implementation of `Expr.replace`.
 -/
 
+deprecated_module (since := "2026-01-26")
+
+set_option linter.deprecated false
+
 @[expose] public section
 
 namespace Lean.Expr
@@ -29,6 +34,7 @@ If you wish to recursively replace things in the implementation of `f?`, you can
 
 The function is also memoised, which means that if the
 same expression (by reference) is encountered the cached replacement is used. -/
+@[deprecated "use `MonadCacheT`  and `checkCache`" (since := "2026-01-24")]
 def replaceRec (f? : (Expr → Expr) → Expr → Option Expr) : Expr → Expr :=
   memoFix fun r e ↦
     match f? r e with

Mathlib/Tactic/Linter/DirectoryDependency.lean

@@ -647,7 +647,7 @@ public def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array Me
     -- `ImportGraph`, `ProofWidgets` or `LeanSearchClient` (as these are imported in Tactic.Common).
     -- We also allow transitive imports of Mathlib.Init, as well as Mathlib.Init itself.
     let initImports := (← findImports ("Mathlib" / "Init.lean")).append
-      #[`Mathlib.Init, `Mathlib.Tactic.DeclarationNames]
+      #[`Mathlib.Init, `Mathlib.Tactic.DeclarationNames, `Mathlib.Tactic.Linter.DeprecatedModule]
     let exclude := [
       `Init, `Std, `Lean,
       `Aesop, `Qq, `Plausible, `ImportGraph, `ProofWidgets, `LeanSearchClient

Mathlib/Util/MemoFix.lean

@@ -15,9 +15,11 @@ public import Mathlib.Init
 
 variable {α β : Type}
 
-@[noinline]
+@[noinline, deprecated "deprecated without replacement" (since := "2026-01-24")]
 def injectIntoBaseIO {α : Type} (a : α) : BaseIO α := pure a
 
+set_option linter.deprecated false in
+@[deprecated "deprecated without replacement" (since := "2026-01-24")]
 unsafe def memoFixImpl [Nonempty β] (f : (α → β) → (α → β)) : α → β := unsafeBaseIO do
   let cache : IO.Ref (Lean.PtrMap α β) ← ST.mkRef Lean.mkPtrMap
   let rec fix (a) : β := unsafeBaseIO do
@@ -34,5 +36,6 @@ Hashing makes use of a pointer hash.
 This is useful for implementing tree traversal functions where
 subtrees may be referenced in multiple places.
 -/
-@[implemented_by memoFixImpl]
+@[implemented_by memoFixImpl,
+deprecated "use `MonadCacheT`  and `checkCache`" (since := "2026-01-24")]
 public opaque memoFix [Nonempty β] (f : (α → β) → (α → β)) : α → β