diff --git a/Mathlib/Data/List/InsertIdx.lean b/Mathlib/Data/List/InsertIdx.lean
index 97beb602d1bac8..ad2325090e98a9 100644
--- a/Mathlib/Data/List/InsertIdx.lean
+++ b/Mathlib/Data/List/InsertIdx.lean
@@ -42,7 +42,7 @@ theorem getElem_insertIdx_add_succ (l : List α) (x : α) (n k : ℕ) (hk' : n +
     (hk : n + k + 1 < (insertIdx n x l).length := (by
       rwa [length_insertIdx_of_le_length (by omega), Nat.succ_lt_succ_iff])) :
     (insertIdx n x l)[n + k + 1] = l[n + k] := by
-  rw [getElem_insertIdx_of_ge (by omega)]
+  rw [getElem_insertIdx_of_gt (by omega)]
   simp only [Nat.add_one_sub_one]
 
 theorem get_insertIdx_add_succ (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length)
diff --git a/Mathlib/Tactic/Recall.lean b/Mathlib/Tactic/Recall.lean
index 29e44ac4dc6fb8..a584f7782ab5d8 100644
--- a/Mathlib/Tactic/Recall.lean
+++ b/Mathlib/Tactic/Recall.lean
@@ -67,7 +67,7 @@ elab_rules : command
         runTermElabM fun vars => do
           withAutoBoundImplicit do
             elabBinders binders.getArgs fun xs => do
-              let xs ← addAutoBoundImplicits xs
+              let xs ← addAutoBoundImplicits xs none
               let type ← elabType type
               Term.synthesizeSyntheticMVarsNoPostponing
               let type ← mkForallFVars xs type
diff --git a/Mathlib/Topology/List.lean b/Mathlib/Topology/List.lean
index b2b581ce1f8336..7a6639e8b8ac00 100644
--- a/Mathlib/Topology/List.lean
+++ b/Mathlib/Topology/List.lean
@@ -172,53 +172,51 @@ theorem continuous_prod [Monoid α] [ContinuousMul α] : Continuous (prod : List
 
 end List
 
-namespace Vector
+namespace List.Vector
 
 open List
 
-open List (Vector)
+instance (n : ℕ) : TopologicalSpace (Vector α n) := by unfold Vector; infer_instance
 
-instance (n : ℕ) : TopologicalSpace (List.Vector α n) := by unfold List.Vector; infer_instance
-
-theorem tendsto_cons {n : ℕ} {a : α} {l : List.Vector α n} :
-    Tendsto (fun p : α × List.Vector α n => p.1 ::ᵥ p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a ::ᵥ l)) := by
+theorem tendsto_cons {n : ℕ} {a : α} {l : Vector α n} :
+    Tendsto (fun p : α × Vector α n => p.1 ::ᵥ p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a ::ᵥ l)) := by
   rw [tendsto_subtype_rng, Vector.cons_val]
   exact tendsto_fst.cons (Tendsto.comp continuousAt_subtype_val tendsto_snd)
 
 theorem tendsto_insertIdx {n : ℕ} {i : Fin (n + 1)} {a : α} :
-    ∀ {l : List.Vector α n},
-      Tendsto (fun p : α × List.Vector α n => Vector.insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l)
-        (𝓝 (Vector.insertIdx a i l))
+    ∀ {l : Vector α n},
+      Tendsto (fun p : α × Vector α n => insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l)
+        (𝓝 (insertIdx a i l))
   | ⟨l, hl⟩ => by
-    rw [Vector.insertIdx, tendsto_subtype_rng]
-    simp only [Vector.insertIdx_val]
+    rw [insertIdx, tendsto_subtype_rng]
+    simp only [insertIdx_val]
     exact List.tendsto_insertIdx tendsto_fst (Tendsto.comp continuousAt_subtype_val tendsto_snd : _)
 
 @[deprecated (since := "2024-10-21")] alias tendsto_insertNth := tendsto_insertIdx'
 
 /-- Continuity of `Vector.insertIdx`. -/
 theorem continuous_insertIdx' {n : ℕ} {i : Fin (n + 1)} :
-    Continuous fun p : α × List.Vector α n => Vector.insertIdx p.1 i p.2 :=
+    Continuous fun p : α × Vector α n => Vector.insertIdx p.1 i p.2 :=
   continuous_iff_continuousAt.mpr fun ⟨a, l⟩ => by
     rw [ContinuousAt, nhds_prod_eq]; exact tendsto_insertIdx
 
 @[deprecated (since := "2024-10-21")] alias continuous_insertNth' := continuous_insertIdx'
 
-theorem continuous_insertIdx {n : ℕ} {i : Fin (n + 1)} {f : β → α} {g : β → List.Vector α n}
+theorem continuous_insertIdx {n : ℕ} {i : Fin (n + 1)} {f : β → α} {g : β → Vector α n}
     (hf : Continuous f) (hg : Continuous g) : Continuous fun b => Vector.insertIdx (f b) i (g b) :=
   continuous_insertIdx'.comp (hf.prod_mk hg)
 
 @[deprecated (since := "2024-10-21")] alias continuous_insertNth := continuous_insertIdx
 
 theorem continuousAt_eraseIdx {n : ℕ} {i : Fin (n + 1)} :
-    ∀ {l : List.Vector α (n + 1)}, ContinuousAt (List.Vector.eraseIdx i) l
+    ∀ {l : Vector α (n + 1)}, ContinuousAt (Vector.eraseIdx i) l
   | ⟨l, hl⟩ => by
-    rw [ContinuousAt, List.Vector.eraseIdx, tendsto_subtype_rng]
+    rw [ContinuousAt, Vector.eraseIdx, tendsto_subtype_rng]
     simp only [Vector.eraseIdx_val]
     exact Tendsto.comp List.tendsto_eraseIdx continuousAt_subtype_val
 
 theorem continuous_eraseIdx {n : ℕ} {i : Fin (n + 1)} :
-    Continuous (List.Vector.eraseIdx i : List.Vector α (n + 1) → List.Vector α n) :=
+    Continuous (Vector.eraseIdx i : Vector α (n + 1) → Vector α n) :=
   continuous_iff_continuousAt.mpr fun ⟨_a, _l⟩ => continuousAt_eraseIdx
 
-end Vector
+end List.Vector
diff --git a/Test.lean b/Test.lean
new file mode 100644
index 00000000000000..00b95b3fb02470
--- /dev/null
+++ b/Test.lean
@@ -0,0 +1,3 @@
+import Mathlib
+
+#aesop_stats
diff --git a/lake-manifest.json b/lake-manifest.json
index 64eb7589737a91..49f03a5b7946eb 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -45,10 +45,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ba9a63be53f16b3b6e4043641c6bad4883e650b4",
+   "rev": "3e42c8423a3a2974015c59e2beb0e36dfffe5937",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "forward-test-master-no-precomp",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24cbb071689802fd6d3ff42198b19b125004c4e3",
+   "rev": "fcc3faa429c1ab53c0504b076e03c852512a04e3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
diff --git a/lakefile.lean b/lakefile.lean
index 501afdb02ff15c..4f377051afda84 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -7,9 +7,9 @@ open Lake DSL
 ## Mathlib dependencies on upstream projects
 -/
 
-require "leanprover-community" / "batteries" @ git "main"
+require "leanprover-community" / "batteries" @ git "nightly-testing"
 require "leanprover-community" / "Qq" @ git "master"
-require "leanprover-community" / "aesop" @ git "master"
+require "leanprover-community" / "aesop" @ git "forward-test-master-no-precomp"
 require "leanprover-community" / "proofwidgets" @ git "v0.0.52-pre" -- ProofWidgets should always be pinned to a specific version
 require "leanprover-community" / "importGraph" @ git "main"
 require "leanprover-community" / "LeanSearchClient" @ git "main"
@@ -38,7 +38,9 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   -- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
   ⟨`linter.style.missingEnd, true⟩,
   ⟨`linter.style.multiGoal, true⟩,
-  ⟨`linter.style.setOption, true⟩
+  ⟨`linter.style.setOption, true⟩,
+  ⟨`aesop.collectStats, true⟩,
+  ⟨`maxHeartbeats, .ofNat 400000⟩
 ]
 
 /-- These options are passed as `leanOptions` to building mathlib, as well as the
diff --git a/lean-toolchain b/lean-toolchain
index 3ca992cf968f8f..a854cd826809ff 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.17.0-rc1
+leanprover/lean4:nightly-2025-02-09