diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index c890e64adeb8d..558cb2f998488 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -296,7 +296,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.6.0-rc1
+          git checkout toolchain/v4.6.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index b5d6feef871c7..4732ab2cca7a0 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -303,7 +303,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.6.0-rc1
+          git checkout toolchain/v4.6.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .
diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
index 752fb6e527345..89839f422004d 100644
--- a/.github/workflows/build.yml.in
+++ b/.github/workflows/build.yml.in
@@ -282,7 +282,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.6.0-rc1
+          git checkout toolchain/v4.6.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .
diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
index fe620850f17fa..27b0d1a7cee1e 100644
--- a/.github/workflows/build_fork.yml
+++ b/.github/workflows/build_fork.yml
@@ -300,7 +300,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.6.0-rc1
+          git checkout toolchain/v4.6.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .
diff --git a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
index 92c0295fdded1..c5f87d32ab74a 100644
--- a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
+++ b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
@@ -308,7 +308,6 @@ theorem coeff_eq_zero : p.coeff n = 0 ↔ p n = 0 := by
   rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.mkPiRing_eq_zero_iff]
 #align formal_multilinear_series.coeff_eq_zero FormalMultilinearSeries.coeff_eq_zero
 
-@[simp]
 theorem apply_eq_pow_smul_coeff : (p n fun _ => z) = z ^ n • p.coeff n := by simp
 #align formal_multilinear_series.apply_eq_pow_smul_coeff FormalMultilinearSeries.apply_eq_pow_smul_coeff
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 7171942f6304b..5d32f4eecf227 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "cbc437aed076ea3aeb83f318d572f8b6de38265d",
+   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -22,19 +22,19 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "82ac8cce559c3da0ade17cee3e275111fb7f1920",
+   "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "f5b2b6ff817890d85ffd8ed47637e36fcac544a6",
+   "rev": "16cae05860b208925f54e5581ec5fd264823440c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.28",
+   "inputRev": "v0.0.29",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
diff --git a/lakefile.lean b/lakefile.lean
index 8517285689ec6..55b33ee33ea42 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -26,10 +26,10 @@ package mathlib 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/leanprover/std4" @ "v4.6.0"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
-require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
-require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.28"
+require aesop from git "https://github.com/leanprover-community/aesop" @ "v4.6.0"
+require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.29"
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
 require importGraph from git "https://github.com/leanprover-community/import-graph.git" @ "main"
 
diff --git a/lean-toolchain b/lean-toolchain
index cfcdd3277d4a2..50262040deb9a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.0-rc1
+leanprover/lean4:v4.6.0