From 860e1564d5fe45d2ea76ae9457e382eb908b2d47 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 1 Dec 2025 11:09:05 +0100
Subject: [PATCH 1/5] move Std.Range to Std.Legacy.Range

---
 src/Init/Data/Range/Basic.lean                | 14 ++++++-----
 src/Init/Data/Range/Lemmas.lean               | 20 ++++++++--------
 src/Init/Data/Stream.lean                     |  4 ++--
 .../PrettyPrinter/Delaborator/Builtins.lean   |  4 ++--
 src/Std/Do/Triple/SpecLemmas.lean             | 16 ++++++-------
 tests/lean/run/delabStdRange.lean             | 24 +++++++++----------
 tests/lean/run/grind_lint_std_misc.lean       |  2 +-
 7 files changed, 43 insertions(+), 41 deletions(-)

diff --git a/src/Init/Data/Range/Basic.lean b/src/Init/Data/Range/Basic.lean
index 4c9c3e96eef6..2afea6339567 100644
--- a/src/Init/Data/Range/Basic.lean
+++ b/src/Init/Data/Range/Basic.lean
@@ -10,7 +10,7 @@ public import Init.Omega
 
 public section
 
-namespace Std
+namespace Std.Legacy
 -- We put `Range` in `Init` because we want the notation `[i:j]`  without importing `Std`
 -- We don't put `Range` in the top-level namespace to avoid collisions with user defined types
 structure Range where
@@ -74,15 +74,17 @@ macro_rules
   | `([ : $stop : $step ]) => `({ stop := $stop, step := $step, step_pos := by decide : Range })
 
 end Range
-end Std
+end Std.Legacy
 
-theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop := h.2.1
+@[deprecated "use the new range notation `a...b` instead of `[a:b]` and `Std.Rco.lt_upper_of_mem`" (since := "2025-12-01")]
+theorem Membership.mem.upper {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) : i < r.stop := h.2.1
 
-theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i := h.1
+@[deprecated "use the new range notation `a...b` instead of `[a:b]` and `Std.Rco.lower_le_of_mem`" (since := "2025-12-01")]
+theorem Membership.mem.lower {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) : r.start ≤ i := h.1
 
-theorem Membership.mem.step {i : Nat} {r : Std.Range} (h : i ∈ r) : (i - r.start) % r.step = 0 := h.2.2
+theorem Membership.mem.step {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) : (i - r.start) % r.step = 0 := h.2.2
 
-theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) :
+theorem Membership.get_elem_helper {i n : Nat} {r : Std.Legacy.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) :
     i < n := h₂ ▸ h₁.2.1
 
 macro_rules
diff --git a/src/Init/Data/Range/Lemmas.lean b/src/Init/Data/Range/Lemmas.lean
index feb58fc78c41..8f4b8733b0f1 100644
--- a/src/Init/Data/Range/Lemmas.lean
+++ b/src/Init/Data/Range/Lemmas.lean
@@ -15,12 +15,12 @@ public import Init.Data.Nat.Div.Lemmas
 public section
 
 /-!
-# Lemmas about `Std.Range`
+# Lemmas about `Std.Legacy.Range`
 
-We provide lemmas rewriting for loops over `Std.Range` in terms of `List.range'`.
+We provide lemmas rewriting for loops over `Std.Legacy.Range` in terms of `List.range'`.
 -/
 
-namespace Std.Range
+namespace Std.Legacy.Range
 
 /-- Generalization of `mem_of_mem_range'` used in `forIn'_loop_eq_forIn'_range'` below. -/
 private theorem mem_of_mem_range'_aux {r : Range} {a : Nat} (w₁ : (i - r.start) % r.step = 0)
@@ -37,7 +37,7 @@ theorem mem_of_mem_range' {r : Range} (h : x ∈ List.range' r.start r.size r.st
   unfold size at h
   apply mem_of_mem_range'_aux (by simp) (by simp) h
 
-private theorem size_eq (r : Std.Range) (h : i < r.stop) :
+private theorem size_eq (r : Range) (h : i < r.stop) :
     (r.stop - i + r.step - 1) / r.step =
       (r.stop - (i + r.step) + r.step - 1) / r.step + 1 := by
   have w := r.step_pos
@@ -57,7 +57,7 @@ private theorem size_eq (r : Std.Range) (h : i < r.stop) :
       rw [Nat.div_eq_iff] <;> omega
     omega
 
-private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Std.Range)
+private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Range)
     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) (i) (w₁) (w₂) :
     forIn'.loop r f init i w₁ w₂ =
       forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init
@@ -75,7 +75,7 @@ private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Std.Range)
       rw [Nat.div_eq_iff] <;> omega
     simp [this]
 
-@[simp] theorem forIn'_eq_forIn'_range' [Monad m] (r : Std.Range)
+@[simp] theorem forIn'_eq_forIn'_range' [Monad m] (r : Range)
     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
     forIn' r init f =
       forIn' (List.range' r.start r.size r.step) init (fun a h => f a (mem_of_mem_range' h)) := by
@@ -83,12 +83,12 @@ private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Std.Range)
   simp only [size]
   rw [forIn'_loop_eq_forIn'_range']
 
-@[simp] theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
+@[simp] theorem forIn_eq_forIn_range' [Monad m] (r : Range)
     (init : β) (f : Nat → β → m (ForInStep β)) :
     forIn r init f = forIn (List.range' r.start r.size r.step) init f := by
   simp only [forIn, forIn'_eq_forIn'_range']
 
-private theorem forM_loop_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) :
+private theorem forM_loop_eq_forM_range' [Monad m] (r : Range) (f : Nat → m PUnit) :
     forM.loop r f i = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f := by
   have w := r.step_pos
   rw [forM.loop]
@@ -101,8 +101,8 @@ private theorem forM_loop_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat →
       rw [Nat.div_eq_iff] <;> omega
     simp [this]
 
-@[simp] theorem forM_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) :
+@[simp] theorem forM_eq_forM_range' [Monad m] (r : Range) (f : Nat → m PUnit) :
     forM r f = forM (List.range' r.start r.size r.step) f := by
   simp only [forM, Range.forM, forM_loop_eq_forM_range', size]
 
-end Std.Range
+end Std.Legacy.Range
diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean
index 623c9f2e956c..029989c80ba8 100644
--- a/src/Init/Data/Stream.lean
+++ b/src/Init/Data/Stream.lean
@@ -82,7 +82,7 @@ instance : ToStream (Subarray α) (Subarray α) where
 instance : ToStream String Substring.Raw where
   toStream s := s.toRawSubstring
 
-instance : ToStream Std.Range Std.Range where
+instance : ToStream Std.Legacy.Range Std.Legacy.Range where
   toStream r := r
 
 instance [Stream ρ α] [Stream γ β] : Stream (ρ × γ) (α × β) where
@@ -108,7 +108,7 @@ instance : Stream (Subarray α) α where
     else
       none
 
-instance : Stream Std.Range Nat where
+instance : Stream Std.Legacy.Range Nat where
   next? r :=
     if r.start < r.stop then
       some (r.start, { r with start := r.start + r.step })
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index ec3d92bb3342..ae00cacc434b 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -1291,9 +1291,9 @@ def delabPProdMk : Delab := delabPProdMkCore ``PProd.mk
 @[builtin_delab app.MProd.mk]
 def delabMProdMk : Delab := delabPProdMkCore ``MProd.mk
 
-@[builtin_delab app.Std.Range.mk]
+@[builtin_delab app.Std.Legacy.Range.mk]
 def delabRange : Delab := whenPPOption getPPNotation do
-  -- Std.Range.mk : (start : Nat) → (stop : Nat) → (step : Nat) → 0 < step → Std.Range
+  -- Std.Legacy.Range.mk : (start : Nat) → (stop : Nat) → (step : Nat) → 0 < step → Std.Legacy.Range
   guard <| (← getExpr).getAppNumArgs == 4
   -- `none` if the start is `0`
   let start? ← withNaryArg 0 do
diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean
index 42de98cf8fbe..281a49731b3f 100644
--- a/src/Std/Do/Triple/SpecLemmas.lean
+++ b/src/Std/Do/Triple/SpecLemmas.lean
@@ -26,15 +26,15 @@ set_option linter.missingDocs true
 This module contains Hoare triple specifications for some functions in Core.
 -/
 
-namespace Std.Range
+namespace Std.Legacy.Range
 
 /--
 Converts a range to the list of all numbers in the range.
 -/
-abbrev toList (r : Std.Range) : List Nat :=
+abbrev toList (r : Std.Legacy.Range) : List Nat :=
   List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step
 
-end Std.Range
+end Std.Legacy.Range
 
 namespace List
 
@@ -765,23 +765,23 @@ theorem Spec.foldlM_list_const_inv
 @[spec]
 theorem Spec.forIn'_range {β : Type u} {m : Type u → Type v} {ps : PostShape}
     [Monad m] [WPMonad m ps]
-    {xs : Std.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)}
+    {xs : Std.Legacy.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)}
     (inv : Invariant xs.toList β ps)
     (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
       Triple
-        (f cur (by simp [Std.Range.mem_of_mem_range', h]) b)
+        (f cur (by simp [Std.Legacy.Range.mem_of_mem_range', h]) b)
         (inv.1 (⟨pref, cur::suff, h.symm⟩, b))
         (fun r => match r with
           | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
           | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) :
     Triple (forIn' xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by
-  simp only [Std.Range.forIn'_eq_forIn'_range', Std.Range.size, Std.Range.size.eq_1]
+  simp only [Std.Legacy.Range.forIn'_eq_forIn'_range', Std.Legacy.Range.size, Std.Legacy.Range.size.eq_1]
   apply Spec.forIn'_list inv (fun c hcur b => step c hcur b)
 
 @[spec]
 theorem Spec.forIn_range {β : Type u} {m : Type u → Type v} {ps : PostShape}
     [Monad m] [WPMonad m ps]
-    {xs : Std.Range} {init : β} {f : Nat → β → m (ForInStep β)}
+    {xs : Std.Legacy.Range} {init : β} {f : Nat → β → m (ForInStep β)}
     (inv : Invariant xs.toList β ps)
     (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
       Triple
@@ -791,7 +791,7 @@ theorem Spec.forIn_range {β : Type u} {m : Type u → Type v} {ps : PostShape}
           | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
           | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) :
     Triple (forIn xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by
-  simp only [Std.Range.forIn_eq_forIn_range', Std.Range.size]
+  simp only [Std.Legacy.Range.forIn_eq_forIn_range', Std.Legacy.Range.size]
   apply Spec.forIn_list inv step
 
 open Std.PRange in
diff --git a/tests/lean/run/delabStdRange.lean b/tests/lean/run/delabStdRange.lean
index eb9db0ad6f8d..e51ab65e2bbb 100644
--- a/tests/lean/run/delabStdRange.lean
+++ b/tests/lean/run/delabStdRange.lean
@@ -1,40 +1,40 @@
 /-!
-# Tests for delaborators for Std.Range and Std.PRange
+# Tests for delaborators for Std.Legacy.Range and Std.PRange
 -/
 
 /-!
-## Tests for `Std.Range`
+## Tests for `Std.Legacy.Range`
 -/
 
 /-!
 Default lower bound and step
 -/
-/-- info: [:10] : Std.Range -/
-#guard_msgs in #check Std.Range.mk 0 10 1 (by grind)
+/-- info: [:10] : Std.Legacy.Range -/
+#guard_msgs in #check Std.Legacy.Range.mk 0 10 1 (by grind)
 
 /-!
 Default step
 -/
-/-- info: [5:10] : Std.Range -/
-#guard_msgs in #check Std.Range.mk 5 10 1 (by grind)
+/-- info: [5:10] : Std.Legacy.Range -/
+#guard_msgs in #check Std.Legacy.Range.mk 5 10 1 (by grind)
 
 /-!
 Default lower bound
 -/
-/-- info: [:10:2] : Std.Range -/
-#guard_msgs in #check Std.Range.mk 0 10 2 (by grind)
+/-- info: [:10:2] : Std.Legacy.Range -/
+#guard_msgs in #check Std.Legacy.Range.mk 0 10 2 (by grind)
 
 /-!
 No defaults
 -/
-/-- info: [5:10:2] : Std.Range -/
-#guard_msgs in #check Std.Range.mk 5 10 2 (by grind)
+/-- info: [5:10:2] : Std.Legacy.Range -/
+#guard_msgs in #check Std.Legacy.Range.mk 5 10 2 (by grind)
 
 /-!
 Disable notation
 -/
-/-- info: { stop := 10, step_pos := _check._proof_1 } : Std.Range -/
-#guard_msgs in set_option pp.notation false in #check Std.Range.mk 0 10 1 (by grind)
+/-- info: { stop := 10, step_pos := _check._proof_1 } : Std.Legacy.Range -/
+#guard_msgs in set_option pp.notation false in #check Std.Legacy.Range.mk 0 10 1 (by grind)
 
 /-!
 ## Tests for `Std.PRange`
diff --git a/tests/lean/run/grind_lint_std_misc.lean b/tests/lean/run/grind_lint_std_misc.lean
index 2f3871696310..5f349b83cc5d 100644
--- a/tests/lean/run/grind_lint_std_misc.lean
+++ b/tests/lean/run/grind_lint_std_misc.lean
@@ -4,4 +4,4 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 /-! Check remaining Std sub-namespaces: -/
 
 #guard_msgs in
-#grind_lint check (min := 20) in Std.Do Std.Range Std.Tactic
+#grind_lint check (min := 20) in Std.Do Std.Legacy.Range Std.Tactic

From e683d322505b38f6a801b6fdd190e51214524c4c Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 1 Dec 2025 11:14:39 +0100
Subject: [PATCH 2/5] undo deprecations

---
 src/Init/Data/Range/Basic.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Init/Data/Range/Basic.lean b/src/Init/Data/Range/Basic.lean
index 2afea6339567..1ca1e8dc8019 100644
--- a/src/Init/Data/Range/Basic.lean
+++ b/src/Init/Data/Range/Basic.lean
@@ -76,10 +76,8 @@ macro_rules
 end Range
 end Std.Legacy
 
-@[deprecated "use the new range notation `a...b` instead of `[a:b]` and `Std.Rco.lt_upper_of_mem`" (since := "2025-12-01")]
 theorem Membership.mem.upper {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) : i < r.stop := h.2.1
 
-@[deprecated "use the new range notation `a...b` instead of `[a:b]` and `Std.Rco.lower_le_of_mem`" (since := "2025-12-01")]
 theorem Membership.mem.lower {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) : r.start ≤ i := h.1
 
 theorem Membership.mem.step {i : Nat} {r : Std.Legacy.Range} (h : i ∈ r) : (i - r.start) % r.step = 0 := h.2.2

From 6e2954eca62746eff9f2edc81a5f245a3583d504 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 1 Dec 2025 11:51:36 +0100
Subject: [PATCH 3/5] fix test 6332

---
 tests/lean/run/6332.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/6332.lean b/tests/lean/run/6332.lean
index 3fb60200ebc3..6579406404c9 100644
--- a/tests/lean/run/6332.lean
+++ b/tests/lean/run/6332.lean
@@ -3,7 +3,7 @@ Regression test for #6332
 -/
 
 open Function (uncurry)
-open Std (Range)
+open Std.Legacy (Range)
 
 section Matrix
 

From bd30453ef19e5c8a44ab96e6b794f8471bded3d2 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 2 Dec 2025 10:04:32 +0100
Subject: [PATCH 4/5] retrigger CI for mathlib


From c7d73af6d59dd3819537c3a4d35cef1f438b6f9a Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sat, 13 Dec 2025 11:56:06 +0100
Subject: [PATCH 5/5] trigger mathlib CI