chore: add deprecations for {Extract,Lift}Lets.lean (#24871)

Automatically created by #24861. These files were removed in the toolchain bump in ##24561.

Author: grunweg

Mathlib.lean

@@ -5588,6 +5588,7 @@ import Mathlib.Tactic.Explode.Datatypes
 import Mathlib.Tactic.Explode.Pretty
 import Mathlib.Tactic.ExtendDoc
 import Mathlib.Tactic.ExtractGoal
+import Mathlib.Tactic.ExtractLets
 import Mathlib.Tactic.FBinop
 import Mathlib.Tactic.FailIfNoProgress
 import Mathlib.Tactic.FastInstance
@@ -5630,6 +5631,7 @@ import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.IrreducibleDef
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.Lift
+import Mathlib.Tactic.LiftLets
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Linarith.Datatypes
 import Mathlib.Tactic.Linarith.Frontend

Mathlib/Tactic.lean

@@ -81,6 +81,7 @@ import Mathlib.Tactic.Explode.Datatypes
 import Mathlib.Tactic.Explode.Pretty
 import Mathlib.Tactic.ExtendDoc
 import Mathlib.Tactic.ExtractGoal
+import Mathlib.Tactic.ExtractLets
 import Mathlib.Tactic.FBinop
 import Mathlib.Tactic.FailIfNoProgress
 import Mathlib.Tactic.FastInstance
@@ -123,6 +124,7 @@ import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.IrreducibleDef
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.Lift
+import Mathlib.Tactic.LiftLets
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Linarith.Datatypes
 import Mathlib.Tactic.Linarith.Frontend

Mathlib/Tactic/ExtractLets.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Mathlib.Lean.Expr.Basic
+import Mathlib.Tactic.Basic
+import Batteries.Tactic.Lint.Misc
+import Mathlib.Tactic.Linter.DeprecatedModule
+
+deprecated_module "The extract_let tactic was moved to Lean core; \
+  you can probably just remove this import" (since := "2025-05-02")

Mathlib/Tactic/LiftLets.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Mathlib.Tactic.Basic
+import Mathlib.Tactic.Linter.DeprecatedModule
+
+deprecated_module "The lift_lets tactic was moved to Lean core; \
+  you can probably just remove this import" (since := "2025-05-02")