chore: bump to std4#242

Mathlib.lean

@@ -3009,7 +3009,6 @@ import Mathlib.Tactic.CategoryTheory.Reassoc
 import Mathlib.Tactic.CategoryTheory.Slice
 import Mathlib.Tactic.Change
 import Mathlib.Tactic.Choose
-import Mathlib.Tactic.Classical
 import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
@@ -3099,7 +3098,6 @@ import Mathlib.Tactic.NormNum.Prime
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.Observe
 import Mathlib.Tactic.PPWithUniv
-import Mathlib.Tactic.PermuteGoals
 import Mathlib.Tactic.Polyrith
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Positivity.Basic

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/Mathport/Syntax.lean

@@ -24,7 +24,6 @@ import Mathlib.Tactic.CasesM
 import Mathlib.Tactic.CategoryTheory.Elementwise
 import Mathlib.Tactic.CategoryTheory.Slice
 import Mathlib.Tactic.Choose
-import Mathlib.Tactic.Classical
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
@@ -60,7 +59,6 @@ import Mathlib.Tactic.Nontriviality
 import Mathlib.Tactic.NormCast
 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

@@ -18,7 +18,6 @@ import Mathlib.Tactic.CategoryTheory.Reassoc
 import Mathlib.Tactic.CategoryTheory.Slice
 import Mathlib.Tactic.Change
 import Mathlib.Tactic.Choose
-import Mathlib.Tactic.Classical
 import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
@@ -108,7 +107,6 @@ import Mathlib.Tactic.NormNum.Prime
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.Observe
 import Mathlib.Tactic.PPWithUniv
-import Mathlib.Tactic.PermuteGoals
 import Mathlib.Tactic.Polyrith
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Positivity.Basic

Mathlib/Tactic/Common.lean

@@ -28,7 +28,6 @@ import Mathlib.Tactic.ByContra
 import Mathlib.Tactic.Cases
 import Mathlib.Tactic.CasesM
 import Mathlib.Tactic.Choose
-import Mathlib.Tactic.Classical
 import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
@@ -68,7 +67,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.PrintPrefix
 import Mathlib.Tactic.ProjectionNotation
 import Mathlib.Tactic.Propose

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

Mathlib/Tactic/Tauto.lean

@@ -5,8 +5,8 @@ Authors: Simon Hudon, David Renshaw
 -/
 
 import Lean
+import Std.Tactic.Classical
 import Mathlib.Tactic.CasesM
-import Mathlib.Tactic.Classical
 import Mathlib.Tactic.Core
 import Mathlib.Tactic.SolveByElim
 import Qq

lake-manifest.json

@@ -34,10 +34,10 @@
     "inputRev?": "master",
     "inherited": false}},
   {"git":
-   {"url": "https://github.com/leanprover/std4",
+   {"url": "https://github.com/semorrison/std4",
     "subDir?": null,
-    "rev": "e8c27f7d90ee71470558efd1bc197fe55068c748",
+    "rev": "ce98ff6f235b6670b0a2e31c8a8144dc52351547",
     "opts": {},
     "name": "std",
-    "inputRev?": "main",
+    "inputRev?": "classical",
     "inherited": false}}]}

lakefile.lean

@@ -42,7 +42,7 @@ lean_exe checkYaml where
 meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
-require std from git "https://github.com/leanprover/std4" @ "main"
+require std from git "https://github.com/semorrison/std4" @ "classical"
 require Qq from git "https://github.com/gebner/quote4" @ "master"
 require aesop from git "https://github.com/JLimperg/aesop" @ "master"
 require Cli from git "https://github.com/mhuisi/lean4-cli.git" @ "nightly"

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/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 Mathlib.Util.DummyLabelAttr