chore: adaptations for nightly-2025-02-05 (#21490)

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>

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)

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

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

MathlibTest/TransImports.lean

@@ -3,8 +3,8 @@ import Mathlib.Util.TransImports
 /--
 info: 'MathlibTest.TransImports' has at most 1000 transitive imports
 
-3 starting with "Lean.Elab.I":
-[Lean.Elab.InfoTree, Lean.Elab.InfoTree.Main, Lean.Elab.InfoTree.Types]
+4 starting with "Lean.Elab.I":
+[Lean.Elab.InfoTree, Lean.Elab.InfoTree.InlayHints, Lean.Elab.InfoTree.Main, Lean.Elab.InfoTree.Types]
 -/
 #guard_msgs in
 #trans_imports "Lean.Elab.I" at_most 1000

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "13b6a5497059a6c2e548b7ed5d93c6cef7e00f01",
+   "rev": "6696f5243dafb27b6e310913fd9925ec9ad19068",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-02-04
+leanprover/lean4:nightly-2025-02-05