chore: bump for std4#241 (#6975)

- [x] depends on: leanprover-community/batteries#241



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

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

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
 

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
 

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"
 

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)

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

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

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

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
 
 /-!

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",

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

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

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

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