diff --git a/Mathlib.lean b/Mathlib.lean
index 6260381c568cf..b4b1af05c1f04 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3275,7 +3275,6 @@ import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.Observe
 import Mathlib.Tactic.PPWithUniv
 import Mathlib.Tactic.Peel
-import Mathlib.Tactic.PermuteGoals
 import Mathlib.Tactic.Polyrith
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Positivity.Basic
diff --git a/Mathlib/Control/Traversable/Basic.lean b/Mathlib/Control/Traversable/Basic.lean
index 5444772ec5e0f..11f2d973974e4 100644
--- a/Mathlib/Control/Traversable/Basic.lean
+++ b/Mathlib/Control/Traversable/Basic.lean
@@ -277,10 +277,10 @@ section
 variable {F : Type u → Type v} [Applicative F]
 
 instance : Traversable Option :=
-  ⟨@Option.traverse⟩
+  ⟨Option.traverse⟩
 
 instance : Traversable List :=
-  ⟨@List.traverse⟩
+  ⟨List.traverse⟩
 
 end
 
diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean
index a9049ff5256af..77b3d4e67a050 100644
--- a/Mathlib/Data/List/Defs.lean
+++ b/Mathlib/Data/List/Defs.lean
@@ -446,15 +446,7 @@ def mapDiagM' {m} [Monad m] {α} (f : α → α → m Unit) : List α → m Unit
 --   | h :: t => (f h h >> t.mapM' (f h)) >> t.mapDiagM'
 #align list.mmap'_diag List.mapDiagM'
 
-/-- Map each element of a `List` to an action, evaluate these actions in order,
-    and collect the results.
--/
-protected def traverse {F : Type u → Type v} [Applicative F]
-    {α : Type*} {β : Type u} (f : α → F β) : List α → F (List β)
-  | [] => pure []
-  | x :: xs => List.cons <$> f x <*> List.traverse f xs
 #align list.traverse List.traverse
-
 #align list.get_rest List.getRest
 #align list.slice List.dropSlice
 
diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index 09f1db9f370ab..5d8d5c74da67e 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -9,7 +9,6 @@ import Mathlib.Data.Bool.Basic
 import Mathlib.Init.Data.Bool.Lemmas
 import Mathlib.Init.ZeroOne
 import Mathlib.Tactic.Cases
-import Mathlib.Tactic.PermuteGoals
 
 #align_import init.data.nat.bitwise from "leanprover-community/lean"@"53e8520d8964c7632989880372d91ba0cecbaf00"
 
diff --git a/Mathlib/Lean/Expr/Basic.lean b/Mathlib/Lean/Expr/Basic.lean
index cd63ffc56a8e5..35237f7db112b 100644
--- a/Mathlib/Lean/Expr/Basic.lean
+++ b/Mathlib/Lean/Expr/Basic.lean
@@ -182,18 +182,10 @@ namespace Expr
 
 /-! ### Declarations about `Expr` -/
 
-/-- If the expression is a constant, return that name. Otherwise return `Name.anonymous`. -/
-def constName (e : Expr) : Name :=
-  e.constName?.getD Name.anonymous
-
 def bvarIdx? : Expr → Option Nat
   | bvar idx => some idx
   | _        => none
 
-/-- Return the function (name) and arguments of an application. -/
-def getAppFnArgs (e : Expr) : Name × Array Expr :=
-  withApp e λ e a => (e.constName, a)
-
 /-- Invariant: `i : ℕ` should be less than the size of `as : Array Expr`. -/
 private def getAppAppsAux : Expr → Array Expr → Nat → Array Expr
   | .app f a, as, i => getAppAppsAux f (as.set! i (.app f a)) (i-1)
diff --git a/Mathlib/Mathport/Syntax.lean b/Mathlib/Mathport/Syntax.lean
index 5c828882af5a6..69cd1979c88fc 100644
--- a/Mathlib/Mathport/Syntax.lean
+++ b/Mathlib/Mathport/Syntax.lean
@@ -64,7 +64,6 @@ import Mathlib.Tactic.Monotonicity
 import Mathlib.Tactic.Nontriviality
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.NthRewrite
-import Mathlib.Tactic.PermuteGoals
 import Mathlib.Tactic.Polyrith
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.PushNeg
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index 79d9f59c83cbc..4651cd33cb5a7 100644
--- a/Mathlib/Tactic.lean
+++ b/Mathlib/Tactic.lean
@@ -114,7 +114,6 @@ import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.Observe
 import Mathlib.Tactic.PPWithUniv
 import Mathlib.Tactic.Peel
-import Mathlib.Tactic.PermuteGoals
 import Mathlib.Tactic.Polyrith
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Positivity.Basic
diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean
index 2ea7d0b2ead39..d3bc61458fa11 100644
--- a/Mathlib/Tactic/Common.lean
+++ b/Mathlib/Tactic/Common.lean
@@ -57,7 +57,6 @@ import Mathlib.Tactic.MkIffOfInductiveProp
 -- import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.Observe
-import Mathlib.Tactic.PermuteGoals
 import Mathlib.Tactic.ProjectionNotation
 import Mathlib.Tactic.Propose
 import Mathlib.Tactic.PushNeg
diff --git a/Mathlib/Tactic/Lift.lean b/Mathlib/Tactic/Lift.lean
index 5980adbac0eda..32c2093e91f6d 100644
--- a/Mathlib/Tactic/Lift.lean
+++ b/Mathlib/Tactic/Lift.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 import Mathlib.Tactic.Cases
-import Mathlib.Tactic.PermuteGoals
 import Mathlib.Init.Data.Int.Order
 
 /-!
diff --git a/Mathlib/Tactic/PermuteGoals.lean b/Mathlib/Tactic/PermuteGoals.lean
deleted file mode 100644
index 999a7b06ee669..0000000000000
--- a/Mathlib/Tactic/PermuteGoals.lean
+++ /dev/null
@@ -1,61 +0,0 @@
-/-
-Copyright (c) 2022 Arthur Paulino. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Arthur Paulino, Mario Carneiro
--/
-
-import Lean
-import Std.Data.List.Basic
-import Mathlib.Init.Data.Nat.Notation
-
-namespace Mathlib.Tactic
-
-open Lean Elab.Tactic
-
-/--
-If the current goals are `g₁ ⋯ gᵢ ⋯ gₙ`, `splitGoalsAndGetNth i` returns
-`(gᵢ, [g₁, ⋯, gᵢ₋₁], [gᵢ₊₁, ⋯, gₙ])`.
-
-If `reverse` is passed as `true`, the `i`-th goal is picked by counting backwards.
-For instance, `splitGoalsAndGetNth 1 true` puts the last goal in the first component
-of the returned term.
--/
-def splitGoalsAndGetNth (nth : ℕ) (reverse : Bool := false) :
-    TacticM (MVarId × List MVarId × List MVarId) := do
-  if nth = 0 then throwError "goals are 1-indexed"
-  let goals ← getGoals
-  let nGoals := goals.length
-  if nth > nGoals then throwError "goal index out of bounds"
-  let n := if ¬reverse then nth - 1 else nGoals - nth
-  let (gl, g :: gr) := goals.splitAt n | throwNoGoalsToBeSolved
-  pure (g, gl, gr)
-
-/--
-`pick_goal n` will move the `n`-th goal to the front.
-
-`pick_goal -n` will move the `n`-th goal (counting from the bottom) to the front.
-
-See also `Tactic.rotate_goals`, which moves goals from the front to the back and vice-versa.
--/
-elab "pick_goal " reverse:"-"? n:num : tactic => do
-  let (g, gl, gr) ← splitGoalsAndGetNth n.1.toNat !reverse.isNone
-  setGoals $ g :: (gl ++ gr)
-
-/-- `swap` is a shortcut for `pick_goal 2`, which interchanges the 1st and 2nd goals. -/
-macro "swap" : tactic => `(tactic| pick_goal 2)
-
-/--
-`on_goal n => tacSeq` creates a block scope for the `n`-th goal and tries the sequence
-of tactics `tacSeq` on it.
-
-`on_goal -n => tacSeq` does the same, but the `n`-th goal is chosen by counting from the
-bottom.
-
-The goal is not required to be solved and any resulting subgoals are inserted back into the
-list of goals, replacing the chosen goal.
--/
-elab "on_goal " reverse:"-"? n:num " => " seq:tacticSeq : tactic => do
-  let (g, gl, gr) ← splitGoalsAndGetNth n.1.toNat !reverse.isNone
-  setGoals [g]
-  evalTactic seq
-  setGoals $ gl ++ (← getUnsolvedGoals) ++ gr
diff --git a/lake-manifest.json b/lake-manifest.json
index 60c615bc87b01..3af38ac3f3dcd 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50",
+   "rev": "d2d9ea14f353d177d4ac9d781b78191b206daa24",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
index 0829ee748c84d..a0dba87cb5b61 100644
--- a/scripts/style-exceptions.txt
+++ b/scripts/style-exceptions.txt
@@ -112,7 +112,6 @@ Mathlib/Tactic/Expect.lean : line 9 : ERR_MOD : Module docstring missing, or too
 Mathlib/Tactic/Have.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 Mathlib/Tactic/LeftRight.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 Mathlib/Tactic/NormCast/Tactic.lean : line 13 : ERR_MOD : Module docstring missing, or too late
-Mathlib/Tactic/PermuteGoals.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 Mathlib/Tactic/PrintPrefix.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 Mathlib/Tactic/PushNeg.lean : line 13 : ERR_MOD : Module docstring missing, or too late
 Mathlib/Tactic/Recover.lean : line 10 : ERR_MOD : Module docstring missing, or too late
diff --git a/test/PermuteGoals.lean b/test/PermuteGoals.lean
deleted file mode 100644
index 16fd2a23eb894..0000000000000
--- a/test/PermuteGoals.lean
+++ /dev/null
@@ -1,44 +0,0 @@
-import Std.Tactic.GuardExpr
-import Mathlib.Tactic.PermuteGoals
-
-example (p q r : Prop) : p → q → r → p ∧ q ∧ r := by
-  intros
-  constructor
-  on_goal 2 =>
-    guard_target = q ∧ r
-    constructor
-    assumption
-    -- Note that we have not closed all the subgoals here.
-  guard_target = p
-  assumption
-  guard_target = r
-  assumption
-
-example (p q r : Prop) : p → q → r → p ∧ q ∧ r := by
-  intros a b c
-  constructor
-  fail_if_success on_goal -3 => unreachable!
-  fail_if_success on_goal -1 => exact a
-  fail_if_success on_goal 0 => unreachable!
-  fail_if_success on_goal 2 => exact a
-  fail_if_success on_goal 3 => unreachable!
-  on_goal 1 => exact a
-  constructor
-  swap
-  exact c
-  exact b
-
-example (p q : Prop) : p → q → p ∧ q := by
-  intros a b
-  constructor
-  fail_if_success pick_goal -3
-  fail_if_success pick_goal 0
-  fail_if_success pick_goal 3
-  pick_goal -1
-  exact b
-  exact a
-
-example (p : Prop) : p → p := by
-  intros
-  fail_if_success swap -- can't swap with a single goal
-  assumption
diff --git a/test/classical.lean b/test/classical.lean
index 5e57be62097fc..e21b12543e239 100644
--- a/test/classical.lean
+++ b/test/classical.lean
@@ -1,5 +1,5 @@
 import Mathlib.Tactic.Classical
-import Mathlib.Tactic.PermuteGoals
+import Std.Tactic.PermuteGoals
 import Std.Tactic.GuardExpr
 
 noncomputable def foo : Bool := by
diff --git a/test/lift.lean b/test/lift.lean
index a04dfb3cecd15..38f73f10e09bd 100644
--- a/test/lift.lean
+++ b/test/lift.lean
@@ -1,5 +1,5 @@
 import Mathlib.Tactic.Lift
-import Mathlib.Tactic.PermuteGoals
+import Std.Tactic.PermuteGoals
 import Mathlib.Tactic.Coe
 import Mathlib.Init.Set
 import Mathlib.Order.Basic
diff --git a/test/solve_by_elim/basic.lean b/test/solve_by_elim/basic.lean
index f8c2c1620b182..137b1d595ff52 100644
--- a/test/solve_by_elim/basic.lean
+++ b/test/solve_by_elim/basic.lean
@@ -7,7 +7,7 @@ import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Init.Logic
 import Std.Tactic.RCases
 import Mathlib.Tactic.Constructor
-import Mathlib.Tactic.PermuteGoals
+import Std.Tactic.PermuteGoals
 import Mathlib.Tactic.SolveByElim
 import Std.Test.Internal.DummyLabelAttr