chore: bump Std to leanprover-community/batteries#242

Mathlib.lean

@@ -3490,7 +3490,6 @@ import Mathlib.Tactic.ToAdditive
 import Mathlib.Tactic.ToExpr
 import Mathlib.Tactic.ToLevel
 import Mathlib.Tactic.Trace
-import Mathlib.Tactic.TryThis
 import Mathlib.Tactic.TypeCheck
 import Mathlib.Tactic.TypeStar
 import Mathlib.Tactic.UnsetOption
@@ -3842,7 +3841,6 @@ import Mathlib.Util.MemoFix
 import Mathlib.Util.Qq
 import Mathlib.Util.SleepHeartbeats
 import Mathlib.Util.Superscript
-import Mathlib.Util.Syntax
 import Mathlib.Util.SynthesizeUsing
 import Mathlib.Util.Tactic
 import Mathlib.Util.TermBeta

Mathlib/Mathport/Notation.lean

@@ -6,9 +6,9 @@ Authors: Mario Carneiro, Kyle Miller
 import Mathlib.Lean.Elab.Term
 import Mathlib.Lean.PrettyPrinter.Delaborator
 import Mathlib.Tactic.ScopedNS
-import Mathlib.Util.Syntax
 import Std.Linter.UnreachableTactic
 import Std.Util.ExtendedBinder
+import Std.Lean.Syntax
 
 /-!
 # The notation3 macro, simulating Lean 3's notation.

Mathlib/Mathport/Syntax.lean

@@ -93,7 +93,6 @@ import Mathlib.Tactic.TypeCheck
 import Mathlib.Tactic.Use
 import Mathlib.Tactic.WLOG
 import Mathlib.Tactic.Zify
-import Mathlib.Util.Syntax
 import Mathlib.Util.WithWeakNamespace
 import Mathlib.Mathport.Notation
 

Mathlib/Tactic.lean

@@ -168,7 +168,6 @@ import Mathlib.Tactic.ToAdditive
 import Mathlib.Tactic.ToExpr
 import Mathlib.Tactic.ToLevel
 import Mathlib.Tactic.Trace
-import Mathlib.Tactic.TryThis
 import Mathlib.Tactic.TypeCheck
 import Mathlib.Tactic.TypeStar
 import Mathlib.Tactic.UnsetOption

Mathlib/Tactic/Common.lean

@@ -100,7 +100,6 @@ import Mathlib.Tactic.TermCongr
 import Mathlib.Tactic.ToExpr
 import Mathlib.Tactic.ToLevel
 import Mathlib.Tactic.Trace
-import Mathlib.Tactic.TryThis
 import Mathlib.Tactic.TypeCheck
 import Mathlib.Tactic.UnsetOption
 import Mathlib.Tactic.Use

Mathlib/Tactic/Observe.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.Tactic.LibrarySearch
-import Mathlib.Tactic.TryThis
+import Std.Tactic.TryThis
 
 /-!
 # The `observe` tactic.
@@ -14,7 +14,7 @@ import Mathlib.Tactic.TryThis
 
 namespace Mathlib.Tactic.LibrarySearch
 
-open Lean Meta Elab Tactic
+open Lean Meta Elab Tactic Std.Tactic.TryThis
 
 /-- `observe hp : p` asserts the proposition `p`, and tries to prove it using `exact?`.
 If no proof is found, the tactic fails.

Mathlib/Tactic/Propose.lean

@@ -9,7 +9,6 @@ import Mathlib.Lean.Meta.Basic
 import Std.Util.Cache
 import Mathlib.Tactic.Core
 import Std.Tactic.SolveByElim
-import Mathlib.Tactic.TryThis
 
 /-!
 # Propose

Mathlib/Tactic/Rewrites.lean

@@ -13,7 +13,6 @@ import Mathlib.Control.Basic
 import Mathlib.Data.MLList.Dedup
 import Mathlib.Lean.Expr.Basic
 import Mathlib.Lean.Meta.DiscrTree
-import Mathlib.Tactic.TryThis
 
 /-!
 # The `rewrites` tactic.

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096",
+   "rev": "92fb0a9f25093ddc2c99fa2b515cecf1d9e774f9",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",