refactor: improve naming in the range API (#10537)

This PR renames some declarations in the range API for better
consistency and readability. For example,
`UpwardEnumerable.succMany?_succ?` is now called `succMany?_add_one`, in
order to (a) correct the erroneous use of `succ?` instead of `succ`
(=`Nat.succ`) and (b) distinguish the successor of natural numbers
(`add_one`) from the successor of the upward-enumerable type (`succ?` or
`succ`).

src/Init/Data/Range/Polymorphic/BitVec.lean

@@ -59,7 +59,7 @@ instance : LawfulUpwardEnumerable (BitVec n) where
     simp +contextual [UpwardEnumerable.LT, ← BitVec.toNat_inj, succMany?] at ⊢
     omega
   succMany?_zero := by simp [UpwardEnumerable.succMany?, BitVec.toNat_lt_twoPow_of_le]
-  succMany?_succ? a b := by
+  succMany?_add_one a b := by
     simp +contextual [← BitVec.toNat_inj, succMany?, succ?]
     split <;> split
     · rename_i h

src/Init/Data/Range/Polymorphic/Instances.lean

@@ -51,15 +51,15 @@ instance [LE α] [Total (α := α) (· ≤ ·)] [UpwardEnumerable α] [LawfulUpw
       cases n
       · simpa [succMany?_zero] using hn
       · exfalso
-        rw [succMany?_succ?_eq_succ?_bind_succMany?, hab,
-          ← succMany?_succ?_eq_succ?_bind_succMany?] at hn
+        rw [succMany?_add_one_eq_succ?_bind_succMany?, hab,
+          ← succMany?_add_one_eq_succ?_bind_succMany?] at hn
         exact UpwardEnumerable.lt_irrefl ⟨_, hn⟩
     · obtain ⟨n, hn⟩ := h
       cases n
       · simpa [succMany?_zero] using hn.symm
       · exfalso
-        rw [succMany?_succ?_eq_succ?_bind_succMany?, hab.symm,
-          ← succMany?_succ?_eq_succ?_bind_succMany?] at hn
+        rw [succMany?_add_one_eq_succ?_bind_succMany?, hab.symm,
+          ← succMany?_add_one_eq_succ?_bind_succMany?] at hn
         exact UpwardEnumerable.lt_irrefl ⟨_, hn⟩
 
 namespace Rxc
@@ -76,7 +76,7 @@ instance instIsAlwaysFiniteOfLawfulHasSize [LE α] [UpwardEnumerable α]
       simp [succMany?_zero, hn]
     | succ =>
       rename_i n ih
-      rw [succMany?_succ?_eq_succ?_bind_succMany?]
+      rw [succMany?_add_one_eq_succ?_bind_succMany?]
       match hs : succ? lo with
       | none => simp
       | some a =>
@@ -120,7 +120,7 @@ instance LawfulHasSize.of_closed [UpwardEnumerable α] [LE α] [DecidableLE α]
     exfalso
     simp only [UpwardEnumerable.lt_iff] at h
     obtain ⟨n, hn⟩ := h
-    simp [succMany?_succ?_eq_succ?_bind_succMany?, h'] at hn
+    simp [succMany?_add_one_eq_succ?_bind_succMany?, h'] at hn
   size_eq_succ_of_succ?_eq_some bound a a' h h' := by
     simp only [HasSize.size, Nat.pred_eq_succ_iff]
     rw [Rxc.LawfulHasSize.size_eq_succ_of_succ?_eq_some (h := le_of_lt h) (h' := h')]
@@ -130,7 +130,7 @@ instance LawfulHasSize.of_closed [UpwardEnumerable α] [LE α] [DecidableLE α]
       rw [UpwardEnumerable.le_iff]
       rw [UpwardEnumerable.lt_iff] at h
       refine ⟨h.choose, ?_⟩
-      simpa [succMany?_succ?_eq_succ?_bind_succMany?, h'] using h.choose_spec
+      simpa [succMany?_add_one_eq_succ?_bind_succMany?, h'] using h.choose_spec
 
 /--
 Creates a {lean}`HasSize α` from a {lean}`HasSize α` instance. If the latter is lawful
@@ -151,7 +151,7 @@ instance instIsAlwaysFiniteOfLawfulHasSize [LT α] [UpwardEnumerable α]
       simp [succMany?_zero, hn]
     | succ =>
       rename_i n ih
-      rw [succMany?_succ?_eq_succ?_bind_succMany?]
+      rw [succMany?_add_one_eq_succ?_bind_succMany?]
       match hs : succ? lo with
       | none => simp
       | some a =>
@@ -176,7 +176,7 @@ instance instIsAlwaysFiniteOfLawfulHasSize [LT α] [UpwardEnumerable α]
       simp [Nat.ne_of_gt size_pos] at hn
     | succ =>
       rename_i n ih
-      rw [succMany?_succ?_eq_succ?_bind_succMany?]
+      rw [succMany?_add_one_eq_succ?_bind_succMany?]
       match hs : succ? lo with
       | none => simp
       | some a =>

src/Init/Data/Range/Polymorphic/Int.lean

@@ -24,7 +24,7 @@ instance : LawfulUpwardEnumerable Int where
     simp only [UpwardEnumerable.LT, UpwardEnumerable.succMany?, Option.some.injEq]
     omega
   succMany?_zero := by simp [UpwardEnumerable.succMany?]
-  succMany?_succ? := by
+  succMany?_add_one := by
     simp only [UpwardEnumerable.succMany?, UpwardEnumerable.succ?,
       Option.bind_some, Option.some.injEq]
     omega
@@ -37,7 +37,6 @@ instance : LawfulUpwardEnumerableLE Int where
     simp [UpwardEnumerable.LE, UpwardEnumerable.succMany?, Int.le_def, Int.nonneg_def,
       Int.sub_eq_iff_eq_add', eq_comm (a := y)]
 
-instance : LawfulOrderLT Int := inferInstance
 instance : LawfulUpwardEnumerableLT Int := inferInstance
 instance : LawfulUpwardEnumerableLT Int := inferInstance
 

src/Init/Data/Range/Polymorphic/Iterators.lean

@@ -62,12 +62,11 @@ namespace Rcc
 
 variable {α : Type u}
 
--- TODO: Replace the `lit` role with a `module` role?
 /--
 Internal function that constructs an iterator for a closed range {lit}`lo...=hi`.
 This is an internal function.
 Use {name (scope := "Std.Data.Iterators.Producers.Range")}`Rcc.iter` instead, which requires
-importing {lit}`Std.Data.Iterators`.
+importing {module -checked}`Std.Data.Iterators`.
 -/
 @[always_inline, inline]
 def Internal.iter [UpwardEnumerable α] (r : Rcc α) : Iter (α := Rxc.Iterator α) α :=
@@ -149,12 +148,11 @@ namespace Rco
 
 variable {α : Type u}
 
--- TODO: Replace the `lit` role with a `module` role?
 /--
 Internal function that constructs an iterator for a closed range {lit}`lo...hi`.
 This is an internal function.
 Use {name (scope := "Std.Data.Iterators.Producers.Range")}`Rco.iter` instead, which requires
-importing {lit}`Std.Data.Iterators`.
+importing {module -checked}`Std.Data.Iterators`.
 -/
 @[always_inline, inline]
 def Internal.iter [UpwardEnumerable α] (r : Rco α) : Iter (α := Rxo.Iterator α) α :=
@@ -236,12 +234,11 @@ namespace Rci
 
 variable {α : Type u}
 
--- TODO: Replace the `lit` role with a `module` role?
 /--
 Internal function that constructs an iterator for a closed range {lit}`lo...*`.
 This is an internal function.
 Use {name (scope := "Std.Data.Iterators.Producers.Range")}`Rcc.iter` instead, which requires
-importing {lit}`Std.Data.Iterators`.
+importing {module -checked}`Std.Data.Iterators`.
 -/
 @[always_inline, inline]
 def Internal.iter [UpwardEnumerable α] (r : Rci α) : Iter (α := Rxi.Iterator α) α :=
@@ -322,12 +319,11 @@ namespace Roc
 
 variable {α : Type u}
 
--- TODO: Replace the `lit` role with a `module` role?
 /--
 Internal function that constructs an iterator for a left-open right-closed range {lit}`lo<...=hi`.
 This is an internal function.
 Use {name (scope := "Std.Data.Iterators.Producers.Range")}`Roc.iter` instead, which requires
-importing {lit}`Std.Data.Iterators`.
+importing {module -checked}`Std.Data.Iterators`.
 -/
 @[always_inline, inline]
 def Internal.iter [UpwardEnumerable α] (r : Roc α) : Iter (α := Rxc.Iterator α) α :=
@@ -380,7 +376,7 @@ theorem Internal.isPlausibleIndirectOutput_iter_iff
     rw [LawfulUpwardEnumerableLT.lt_iff] at hl
     obtain ⟨n, hn⟩ := hl
     exact ⟨n,
-      by simp [Internal.iter, hn, ← UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?], hu⟩
+      by simp [Internal.iter, hn, ← UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?], hu⟩
 
 @[no_expose]
 instance {m} [UpwardEnumerable α]
@@ -402,12 +398,11 @@ namespace Roo
 
 variable {α : Type u}
 
--- TODO: Replace the `lit` role with a `module` role?
 /--
 Internal function that constructs an iterator for an open range {lit}`lo<...hi`.
 This is an internal function.
 Use {name (scope := "Std.Data.Iterators.Producers.Range")}`Roo.iter` instead, which requires
-importing {lit}`Std.Data.Iterators`.
+importing {module -checked}`Std.Data.Iterators`.
 -/
 @[always_inline, inline]
 def Internal.iter [UpwardEnumerable α] (r : Roo α) : Iter (α := Rxo.Iterator α) α :=
@@ -459,7 +454,7 @@ theorem Internal.isPlausibleIndirectOutput_iter_iff
     rw [LawfulUpwardEnumerableLT.lt_iff] at hl
     obtain ⟨n, hn⟩ := hl
     exact ⟨n,
-      by simp [Internal.iter, hn, ← UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?], hu⟩
+      by simp [Internal.iter, hn, ← UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?], hu⟩
 
 @[no_expose]
 instance {m} [UpwardEnumerable α]
@@ -481,12 +476,11 @@ namespace Roi
 
 variable {α : Type u}
 
--- TODO: Replace the `lit` role with a `module` role?
 /--
 Internal function that constructs an iterator for a closed range {lit}`lo<...*`.
 This is an internal function.
 Use {name (scope := "Std.Data.Iterators.Producers.Range")}`Roi.iter` instead, which requires
-importing {lit}`Std.Data.Iterators`.
+importing {module -checked}`Std.Data.Iterators`.
 -/
 @[always_inline, inline]
 def Internal.iter [UpwardEnumerable α] (r : Roi α) : Iter (α := Rxi.Iterator α) α :=
@@ -535,7 +529,7 @@ theorem Internal.isPlausibleIndirectOutput_iter_iff
     simp only [Membership.mem, LawfulUpwardEnumerableLT.lt_iff] at hl
     obtain ⟨n, hn⟩ := hl
     exact ⟨n,
-      by simp [Internal.iter, hn, ← UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?]⟩
+      by simp [Internal.iter, hn, ← UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?]⟩
 
 @[no_expose]
 instance {m} [UpwardEnumerable α]
@@ -556,12 +550,11 @@ namespace Ric
 
 variable {α : Type u}
 
--- TODO: Replace the `lit` role with a `module` role?
 /--
 Internal function that constructs an iterator for a left-unbounded right-closed range {lit}`*...=hi`.
 This is an internal function.
 Use {name (scope := "Std.Data.Iterators.Producers.Range")}`Ric.iter` instead, which requires
-importing {lit}`Std.Data.Iterators`.
+importing {module -checked}`Std.Data.Iterators`.
 -/
 @[always_inline, inline]
 def Internal.iter [Least? α] (r : Ric α) : Iter (α := Rxc.Iterator α) α :=
@@ -630,12 +623,11 @@ namespace Rio
 
 variable {α : Type u}
 
--- TODO: Replace the `lit` role with a `module` role?
 /--
 Internal function that constructs an iterator for a left-unbounded right-open range {lit}`*...hi`.
 This is an internal function.
 Use {name (scope := "Std.Data.Iterators.Producers.Range")}`Rio.iter` instead, which requires
-importing {lit}`Std.Data.Iterators`.
+importing {module -checked}`Std.Data.Iterators`.
 -/
 @[always_inline, inline]
 def Internal.iter [UpwardEnumerable α] [Least? α] (r : Rio α) : Iter (α := Rxo.Iterator α) α :=
@@ -703,12 +695,11 @@ namespace Rii
 
 variable {α : Type u}
 
--- TODO: Replace the `lit` role with a `module` role?
 /--
 Internal function that constructs an iterator for the full range {lean}`*...*`.
 This is an internal function.
 Use {name (scope := "Std.Data.Iterators.Producers.Range")}`Rio.iter` instead, which requires
-importing {lit}`Std.Data.Iterators`.
+importing {module -checked}`Std.Data.Iterators`.
 -/
 @[always_inline, inline]
 def Internal.iter [UpwardEnumerable α] [Least? α] (_ : Rii α) : Iter (α := Rxi.Iterator α) α :=

src/Init/Data/Range/Polymorphic/Lemmas.lean

@@ -507,7 +507,7 @@ public theorem Rxc.Iterator.pairwise_toList_upwardEnumerableLt [LE α] [Decidabl
     simp only at ha
     have : UpwardEnumerable.LT a ha.choose := by
       refine ⟨0, ?_⟩
-      simp only [succMany?_succ?, succMany?_zero,
+      simp only [succMany?_add_one, succMany?_zero,
         Option.bind_some]
       exact ha.choose_spec.1
     exact UpwardEnumerable.lt_of_lt_of_le this ha.choose_spec.2
@@ -530,7 +530,7 @@ public theorem Rxo.Iterator.pairwise_toList_upwardEnumerableLt [LT α] [Decidabl
     simp only at ha
     have : UpwardEnumerable.LT a ha.choose := by
       refine ⟨0, ?_⟩
-      simp only [succMany?_succ?, succMany?_zero,
+      simp only [succMany?_add_one, succMany?_zero,
         Option.bind_some]
       exact ha.choose_spec.1
     exact UpwardEnumerable.lt_of_lt_of_le this ha.choose_spec.2
@@ -553,7 +553,7 @@ public theorem Rxi.Iterator.pairwise_toList_upwardEnumerableLt
     simp only at ha
     have : UpwardEnumerable.LT a ha.choose := by
       refine ⟨0, ?_⟩
-      simp only [succMany?_succ?, succMany?_zero,
+      simp only [succMany?_add_one, succMany?_zero,
         Option.bind_some]
       exact ha.choose_spec.1
     exact UpwardEnumerable.lt_of_lt_of_le this ha.choose_spec.2
@@ -1300,7 +1300,7 @@ public theorem toList_eq_nil_iff [LE α] [DecidableLE α] [LT α] [UpwardEnumera
   split <;> rename_i heq <;>
     simp [UpwardEnumerable.lt_iff, UpwardEnumerable.lt_iff_exists,
       UpwardEnumerable.le_iff, UpwardEnumerable.le_iff_exists,
-      UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?, heq]
+      UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?, heq]
 
 public theorem toArray_eq_empty_iff [LE α] [DecidableLE α] [LT α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
@@ -1681,7 +1681,7 @@ public theorem isEmpty_iff_forall_not_mem [LT α] [DecidableLT α] [UpwardEnumer
   · rintro h a ⟨hl, hu⟩
     simp only [UpwardEnumerable.lt_iff, UpwardEnumerable.lt_iff] at h hl hu
     obtain ⟨n, hn⟩ := hl
-    simp only [succMany?_succ?_eq_succ?_bind_succMany?, Option.bind_eq_some_iff] at hn
+    simp only [succMany?_add_one_eq_succ?_bind_succMany?, Option.bind_eq_some_iff] at hn
     obtain ⟨a', ha', hn⟩ := hn
     exact h a' ha' (UpwardEnumerable.lt_of_le_of_lt ⟨n, hn⟩ hu)
   · intro h a ha
@@ -1882,7 +1882,7 @@ public theorem isEmpty_iff_forall_not_mem [LT α] [DecidableLT α] [UpwardEnumer
     UpwardEnumerable.lt_iff_exists, not_exists]
   constructor
   · intro h a n hs
-    simp [UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?, h] at hs
+    simp [UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?, h] at hs
   · simp only [Option.eq_none_iff_forall_ne_some]
     intro h a
     simpa [UpwardEnumerable.succMany?_one] using h a 0
@@ -2692,7 +2692,7 @@ theorem getElem?_toList_eq [LE α] [DecidableLE α] [UpwardEnumerable α] [Lawfu
   · rename_i n ih
     rw [toList_eq_match]
     split
-    · simp only [List.getElem?_cons_succ, succMany?_succ?_eq_succ?_bind_succMany?]
+    · simp only [List.getElem?_cons_succ, succMany?_add_one_eq_succ?_bind_succMany?]
       cases hs : UpwardEnumerable.succ? r.lower
       · rw [Roc.toList_eq_match]
         simp [hs]
@@ -2784,10 +2784,10 @@ theorem getElem?_toList_eq [LE α] [DecidableLE α] [UpwardEnumerable α] [Lawfu
     r.toList[i]? = (UpwardEnumerable.succMany? (i + 1) r.lower).filter (· ≤ r.upper) := by
   match h : UpwardEnumerable.succ? r.lower with
   | none =>
-    simp [toList_eq_match, h, UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?]
+    simp [toList_eq_match, h, UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?]
   | some next =>
     rw [toList_Roc_eq_toList_Rcc_of_isSome_succ? (by simp [h]), Rcc.getElem?_toList_eq]
-    simp [succMany?_succ?_eq_succ?_bind_succMany?, h]
+    simp [succMany?_add_one_eq_succ?_bind_succMany?, h]
 
 theorem getElem?_toArray_eq [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i} :
@@ -2960,7 +2960,7 @@ theorem getElem?_toList_eq [LT α] [DecidableLT α] [UpwardEnumerable α]
   · rename_i n ih
     rw [toList_eq_if]
     split
-    · simp only [List.getElem?_cons_succ, succMany?_succ?_eq_succ?_bind_succMany?]
+    · simp only [List.getElem?_cons_succ, succMany?_add_one_eq_succ?_bind_succMany?]
       cases hs : UpwardEnumerable.succ? r.lower
       · rw [Roo.toList_eq_match]
         simp [hs]
@@ -3052,10 +3052,10 @@ theorem getElem?_toList_eq [LT α] [DecidableLT α] [UpwardEnumerable α] [Lawfu
     r.toList[i]? = (UpwardEnumerable.succMany? (i + 1) r.lower).filter (· < r.upper) := by
   match h : UpwardEnumerable.succ? r.lower with
   | none =>
-    simp [toList_eq_match, h, UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?]
+    simp [toList_eq_match, h, UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?]
   | some next =>
     rw [toList_Roo_eq_toList_Rco_of_isSome_succ? (by simp [h]), Rco.getElem?_toList_eq]
-    simp [succMany?_succ?_eq_succ?_bind_succMany?, h]
+    simp [succMany?_add_one_eq_succ?_bind_succMany?, h]
 
 theorem getElem?_toArray_eq [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i} :
@@ -3224,7 +3224,7 @@ theorem getElem?_toList_eq [UpwardEnumerable α]
   · simp [toList_eq_toList_Roi, UpwardEnumerable.succMany?_zero]
   · rename_i n ih
     rw [toList_eq_toList_Roi]
-    simp only [List.getElem?_cons_succ, succMany?_succ?_eq_succ?_bind_succMany?]
+    simp only [List.getElem?_cons_succ, succMany?_add_one_eq_succ?_bind_succMany?]
     cases hs : UpwardEnumerable.succ? r.lower
     · rw [Roi.toList_eq_match]
       simp [hs]
@@ -3308,10 +3308,10 @@ theorem getElem?_toList_eq [LT α] [DecidableLT α] [UpwardEnumerable α] [Lawfu
     r.toList[i]? = UpwardEnumerable.succMany? (i + 1) r.lower := by
   match h : UpwardEnumerable.succ? r.lower with
   | none =>
-    simp [toList_eq_match, h, UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?]
+    simp [toList_eq_match, h, UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?]
   | some next =>
     rw [toList_Roi_eq_toList_Rci_of_isSome_succ? (by simp [h]), Rci.getElem?_toList_eq]
-    simp [succMany?_succ?_eq_succ?_bind_succMany?, h]
+    simp [succMany?_add_one_eq_succ?_bind_succMany?, h]
 
 theorem getElem?_toArray_eq [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i} :

src/Init/Data/Range/Polymorphic/Nat.lean

@@ -43,7 +43,7 @@ instance : LawfulUpwardEnumerableLE Nat where
 
 instance : LawfulUpwardEnumerable Nat where
   succMany?_zero := by simp [UpwardEnumerable.succMany?]
-  succMany?_succ? := by simp [UpwardEnumerable.succMany?, UpwardEnumerable.succ?, Nat.add_assoc]
+  succMany?_add_one := by simp [UpwardEnumerable.succMany?, UpwardEnumerable.succ?, Nat.add_assoc]
   ne_of_lt a b hlt := by
     have hn := hlt.choose_spec
     simp only [UpwardEnumerable.succMany?, Option.some.injEq] at hn
@@ -79,11 +79,10 @@ instance : LinearlyUpwardEnumerable Nat := inferInstance
 
 end PRange
 
--- TODO: Replace the `lit` role with a `module` role?
 /-!
 The following instances are used for the implementation of array slices a.k.a.
 {name (scope := "Init.Data.Array.Subarray")}`Subarray`.
-See also {lit}`Init.Data.Slice.Array`.
+See also {module -checked}`Init.Data.Slice.Array`.
 -/
 
 instance : Roo.HasRcoIntersection Nat where

src/Init/Data/Range/Polymorphic/RangeIterator.lean

@@ -265,7 +265,7 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LE α] [Decid
       | succ n ih =>
         constructor
         rintro it'
-        simp only [succMany?_succ?_eq_succ?_bind_succMany?] at hn
+        simp only [succMany?_add_one_eq_succ?_bind_succMany?] at hn
         match hs : succ? init with
         | none =>
           simp only [hs]
@@ -346,7 +346,7 @@ instance Iterator.instIteratorAccess [UpwardEnumerable α] [LE α] [DecidableLE
           · apply IterM.IsPlausibleNthOutputStep.done
             simp only [Monadic.isPlausibleStep_iff, Monadic.step, heq']
           · rename_i out
-            simp only [heq', Option.bind_some, succMany?_succ?_eq_succ?_bind_succMany?] at heq
+            simp only [heq', Option.bind_some, succMany?_add_one_eq_succ?_bind_succMany?] at heq
             specialize ih ⟨⟨UpwardEnumerable.succ? out, it.internalState.upperBound⟩⟩
             simp only [heq] at ih
             by_cases heq'' : out ≤ it.internalState.upperBound
@@ -362,7 +362,7 @@ instance Iterator.instIteratorAccess [UpwardEnumerable α] [LE α] [DecidableLE
           rename_i out
           simp only [heq', Option.bind_some] at heq
           have hle : UpwardEnumerable.LE out _ := ⟨n + 1, heq⟩
-          simp only [succMany?_succ?_eq_succ?_bind_succMany?] at heq
+          simp only [succMany?_add_one_eq_succ?_bind_succMany?] at heq
           specialize ih ⟨⟨UpwardEnumerable.succ? out, it.internalState.upperBound⟩⟩
           simp only [heq] at ih
           by_cases hout : out ≤ it.internalState.upperBound
@@ -403,7 +403,7 @@ theorem Iterator.Monadic.isPlausibleIndirectOutput_iff
       obtain ⟨n, hn⟩ := ih
       obtain ⟨a, ha, h₁, h₂, h₃⟩ := h
       refine ⟨n + 1, ?_⟩
-      simp [ha, ← h₃, hn.2, succMany?_succ?_eq_succ?_bind_succMany?, h₂, hn]
+      simp [ha, ← h₃, hn.2, succMany?_add_one_eq_succ?_bind_succMany?, h₂, hn]
   · rintro ⟨n, hn, hu⟩
     induction n generalizing it
     case zero =>
@@ -416,7 +416,7 @@ theorem Iterator.Monadic.isPlausibleIndirectOutput_iff
       rename_i a
       simp only [hn', Option.bind_some] at hn
       have hle : UpwardEnumerable.LE a out := ⟨_, hn⟩
-      rw [succMany?_succ?_eq_succ?_bind_succMany?] at hn
+      rw [succMany?_add_one_eq_succ?_bind_succMany?] at hn
       cases hn' : succ? a
       · simp only [hn', Option.bind_none, reduceCtorEq] at hn
       rename_i a'
@@ -546,7 +546,7 @@ theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α] [LE α] [Decidab
                 (by
                   refine UpwardEnumerable.le_trans hl ?_
                   simp only [Monadic.isPlausibleIndirectOutput_iff, it',
-                    ← succMany?_succ?_eq_succ?_bind_succMany?] at h
+                    ← succMany?_add_one_eq_succ?_bind_succMany?] at h
                   exact ⟨h.choose + 1, h.choose_spec.1⟩)
                 (by
                   simp only [Monadic.isPlausibleIndirectOutput_iff, it'] at h
@@ -842,7 +842,7 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LT α] [Decid
       | succ n ih =>
         constructor
         rintro it'
-        simp only [succMany?_succ?_eq_succ?_bind_succMany?] at hn
+        simp only [succMany?_add_one_eq_succ?_bind_succMany?] at hn
         match hs : succ? init with
         | none =>
           simp only [hs]
@@ -923,7 +923,7 @@ instance Iterator.instIteratorAccess [UpwardEnumerable α] [LT α] [DecidableLT
           · apply IterM.IsPlausibleNthOutputStep.done
             simp only [Monadic.isPlausibleStep_iff, Monadic.step, heq']
           · rename_i out
-            simp only [heq', Option.bind_some, succMany?_succ?_eq_succ?_bind_succMany?] at heq
+            simp only [heq', Option.bind_some, succMany?_add_one_eq_succ?_bind_succMany?] at heq
             specialize ih ⟨⟨UpwardEnumerable.succ? out, it.internalState.upperBound⟩⟩
             simp only [heq] at ih
             by_cases heq'' : out < it.internalState.upperBound
@@ -939,7 +939,7 @@ instance Iterator.instIteratorAccess [UpwardEnumerable α] [LT α] [DecidableLT
           rename_i out
           simp only [heq', Option.bind_some] at heq
           have hlt : UpwardEnumerable.LT out _ := ⟨n, heq⟩
-          simp only [succMany?_succ?_eq_succ?_bind_succMany?] at heq
+          simp only [succMany?_add_one_eq_succ?_bind_succMany?] at heq
           specialize ih ⟨⟨UpwardEnumerable.succ? out, it.internalState.upperBound⟩⟩
           simp only [heq] at ih
           by_cases hout : out < it.internalState.upperBound
@@ -980,7 +980,7 @@ theorem Iterator.Monadic.isPlausibleIndirectOutput_iff
       obtain ⟨n, hn⟩ := ih
       obtain ⟨a, ha, h₁, h₂, h₃⟩ := h
       refine ⟨n + 1, ?_⟩
-      simp [ha, ← h₃, hn.2, succMany?_succ?_eq_succ?_bind_succMany?, h₂, hn]
+      simp [ha, ← h₃, hn.2, succMany?_add_one_eq_succ?_bind_succMany?, h₂, hn]
   · rintro ⟨n, hn, hu⟩
     induction n generalizing it
     case zero =>
@@ -993,7 +993,7 @@ theorem Iterator.Monadic.isPlausibleIndirectOutput_iff
       rename_i a
       simp only [hn', Option.bind_some] at hn
       have hlt : UpwardEnumerable.LT a out := ⟨_, hn⟩
-      rw [succMany?_succ?_eq_succ?_bind_succMany?] at hn
+      rw [succMany?_add_one_eq_succ?_bind_succMany?] at hn
       cases hn' : succ? a
       · simp only [hn', Option.bind_none, reduceCtorEq] at hn
       rename_i a'
@@ -1123,7 +1123,7 @@ theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α] [LT α] [Decidab
                 (by
                   refine UpwardEnumerable.le_trans hl ?_
                   simp only [Monadic.isPlausibleIndirectOutput_iff, it',
-                    ← succMany?_succ?_eq_succ?_bind_succMany?] at h
+                    ← succMany?_add_one_eq_succ?_bind_succMany?] at h
                   exact ⟨h.choose + 1, h.choose_spec.1⟩)
                 (by
                   simp only [Monadic.isPlausibleIndirectOutput_iff, it'] at h
@@ -1365,7 +1365,7 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α]
       | succ n ih =>
         constructor
         rintro it'
-        simp only [succMany?_succ?_eq_succ?_bind_succMany?] at hn
+        simp only [succMany?_add_one_eq_succ?_bind_succMany?] at hn
         match hs : succ? init with
         | none =>
           simp only [hs]
@@ -1433,7 +1433,7 @@ instance Iterator.instIteratorAccess [UpwardEnumerable α]
           · apply IterM.IsPlausibleNthOutputStep.done
             simp only [Monadic.isPlausibleStep_iff, Monadic.step, heq']
           · rename_i out
-            simp only [heq', Option.bind_some, succMany?_succ?_eq_succ?_bind_succMany?] at heq
+            simp only [heq', Option.bind_some, succMany?_add_one_eq_succ?_bind_succMany?] at heq
             specialize ih ⟨⟨UpwardEnumerable.succ? out⟩⟩
             simp only [heq] at ih
             · apply IterM.IsPlausibleNthOutputStep.yield
@@ -1446,7 +1446,7 @@ instance Iterator.instIteratorAccess [UpwardEnumerable α]
           rename_i out
           simp only [heq', Option.bind_some] at heq
           have hlt : UpwardEnumerable.LT out _ := ⟨n, heq⟩
-          simp only [succMany?_succ?_eq_succ?_bind_succMany?] at heq
+          simp only [succMany?_add_one_eq_succ?_bind_succMany?] at heq
           specialize ih ⟨⟨UpwardEnumerable.succ? out⟩⟩
           simp only [heq] at ih
           · apply IterM.IsPlausibleNthOutputStep.yield
@@ -1475,7 +1475,7 @@ theorem Iterator.Monadic.isPlausibleIndirectOutput_iff
       obtain ⟨n, hn⟩ := ih
       obtain ⟨a, ha, h⟩ := h
       refine ⟨n + 1, ?_⟩
-      simp [ha, succMany?_succ?_eq_succ?_bind_succMany?, hn, h]
+      simp [ha, succMany?_add_one_eq_succ?_bind_succMany?, hn, h]
   · rintro ⟨n, hn⟩
     induction n generalizing it
     case zero =>
@@ -1488,7 +1488,7 @@ theorem Iterator.Monadic.isPlausibleIndirectOutput_iff
       rename_i a
       simp only [hn', Option.bind_some] at hn
       have hlt : UpwardEnumerable.LT a out := ⟨_, hn⟩
-      rw [succMany?_succ?_eq_succ?_bind_succMany?] at hn
+      rw [succMany?_add_one_eq_succ?_bind_succMany?] at hn
       cases hn' : succ? a
       · simp only [hn', Option.bind_none, reduceCtorEq] at hn
       rename_i a'
@@ -1599,7 +1599,7 @@ theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α]
                 (by
                   refine UpwardEnumerable.le_trans hl ?_
                   simp only [Monadic.isPlausibleIndirectOutput_iff, it',
-                    ← succMany?_succ?_eq_succ?_bind_succMany?] at h
+                    ← succMany?_add_one_eq_succ?_bind_succMany?] at h
                   exact ⟨h.choose + 1, h.choose_spec⟩)
                 c)
         | ⟨.done c, _⟩ => return c) := by

src/Init/Data/Range/Polymorphic/UInt.lean

@@ -46,9 +46,9 @@ instance : LawfulUpwardEnumerable UInt8 where
   succMany?_zero x := by
     cases x
     simpa [succMany?_ofBitVec] using succMany?_zero
-  succMany?_succ? n x := by
+  succMany?_add_one n x := by
     cases x
-    simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def,
+    simp [succMany?_ofBitVec, succMany?_add_one, Option.bind_map, Function.comp_def,
       succ?_ofBitVec]
 
 instance : LawfulUpwardEnumerableLE UInt8 where
@@ -136,9 +136,9 @@ instance : LawfulUpwardEnumerable UInt16 where
   succMany?_zero x := by
     cases x
     simpa [succMany?_ofBitVec] using succMany?_zero
-  succMany?_succ? n x := by
+  succMany?_add_one n x := by
     cases x
-    simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def,
+    simp [succMany?_ofBitVec, succMany?_add_one, Option.bind_map, Function.comp_def,
       succ?_ofBitVec]
 
 instance : LawfulUpwardEnumerableLE UInt16 where
@@ -226,9 +226,9 @@ instance : LawfulUpwardEnumerable UInt32 where
   succMany?_zero x := by
     cases x
     simpa [succMany?_ofBitVec] using succMany?_zero
-  succMany?_succ? n x := by
+  succMany?_add_one n x := by
     cases x
-    simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def,
+    simp [succMany?_ofBitVec, succMany?_add_one, Option.bind_map, Function.comp_def,
       succ?_ofBitVec]
 
 instance : LawfulUpwardEnumerableLE UInt32 where
@@ -316,9 +316,9 @@ instance : LawfulUpwardEnumerable UInt64 where
   succMany?_zero x := by
     cases x
     simpa [succMany?_ofBitVec] using succMany?_zero
-  succMany?_succ? n x := by
+  succMany?_add_one n x := by
     cases x
-    simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def,
+    simp [succMany?_ofBitVec, succMany?_add_one, Option.bind_map, Function.comp_def,
       succ?_ofBitVec]
 
 instance : LawfulUpwardEnumerableLE UInt64 where
@@ -406,9 +406,9 @@ instance : LawfulUpwardEnumerable USize where
   succMany?_zero x := by
     cases x
     simpa [succMany?_ofBitVec] using succMany?_zero
-  succMany?_succ? n x := by
+  succMany?_add_one n x := by
     cases x
-    simp [succMany?_ofBitVec, succMany?_succ?, Option.bind_map, Function.comp_def,
+    simp [succMany?_ofBitVec, succMany?_add_one, Option.bind_map, Function.comp_def,
       succ?_ofBitVec]
 
 instance : LawfulUpwardEnumerableLE USize where

src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean

@@ -102,27 +102,33 @@ class LawfulUpwardEnumerable (α : Type u) [UpwardEnumerable α] where
   The `n + 1`-th successor of `a` is the successor of the `n`-th successor, given that said
   successors actually exist.
   -/
-  succMany?_succ? (n : Nat) (a : α) :
+  succMany?_add_one (n : Nat) (a : α) :
     succMany? (n + 1) a = (succMany? n a).bind succ?
 
 theorem UpwardEnumerable.succMany?_zero [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a : α} :
     succMany? 0 a = some a :=
   LawfulUpwardEnumerable.succMany?_zero a
 
+theorem UpwardEnumerable.succMany?_add_one [UpwardEnumerable α] [LawfulUpwardEnumerable α]
+    {n : Nat} {a : α} :
+    succMany? (n + 1) a = (succMany? n a).bind succ? :=
+  LawfulUpwardEnumerable.succMany?_add_one n a
+
+@[deprecated succMany?_add_one (since := "2025-09-03")]
 theorem UpwardEnumerable.succMany?_succ? [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     {n : Nat} {a : α} :
     succMany? (n + 1) a = (succMany? n a).bind succ? :=
-  LawfulUpwardEnumerable.succMany?_succ? n a
+  succMany?_add_one
 
-@[deprecated succMany?_succ? (since := "2025-09-03")]
+@[deprecated succMany?_add_one (since := "2025-09-03")]
 theorem UpwardEnumerable.succMany?_succ [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     {n : Nat} {a : α} :
     succMany? (n + 1) a = (succMany? n a).bind succ? :=
-  succMany?_succ?
+  succMany?_add_one
 
 theorem UpwardEnumerable.succMany?_one [UpwardEnumerable α] [LawfulUpwardEnumerable α] {a : α} :
     succMany? 1 a = succ? a := by
-  simp [succMany?_succ?, succMany?_zero]
+  simp [succMany?_add_one, succMany?_zero]
 
 theorem UpwardEnumerable.succMany?_add [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     {m n : Nat} {a : α} :
@@ -130,25 +136,33 @@ theorem UpwardEnumerable.succMany?_add [UpwardEnumerable α] [LawfulUpwardEnumer
   induction n
   case zero => simp [succMany?_zero]
   case succ n ih =>
-    rw [← Nat.add_assoc, succMany?_succ?, ih, Option.bind_assoc]
-    simp [succMany?_succ?]
+    rw [← Nat.add_assoc, succMany?_add_one, ih, Option.bind_assoc]
+    simp [succMany?_add_one]
 
-theorem UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?
+theorem UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?
     [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     {n : Nat} {a : α} :
     succMany? (n + 1) a = (succ? a).bind (succMany? n ·) := by
   rw [Nat.add_comm]
-  simp [succMany?_add, succMany?_succ?, succMany?_zero]
+  simp [succMany?_add, succMany?_add_one, succMany?_zero]
 
-@[deprecated UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany? (since := "2025-09-03")]
+@[deprecated UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany? (since := "2025-09-03")]
+theorem UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?
+    [UpwardEnumerable α] [LawfulUpwardEnumerable α]
+    (n : Nat) (a : α) :
+    succMany? (n + 1) a = (succ? a).bind (succMany? n ·) :=
+  UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?
+
+@[deprecated UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany? (since := "2025-09-03")]
 theorem LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?
     [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     (n : Nat) (a : α) :
     succMany? (n + 1) a = (succ? a).bind (succMany? n ·) :=
-  UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?
+  UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?
 
-export UpwardEnumerable (succMany?_zero succMany?_succ? succMany?_one succMany?_add
-                         succMany?_succ?_eq_succ?_bind_succMany?)
+export UpwardEnumerable (succMany?_zero succMany?_succ? succMany?_add_one succMany?_one
+                         succMany?_add succMany?_succ?_eq_succ?_bind_succMany?
+                         succMany?_add_one_eq_succ?_bind_succMany?)
 
 protected theorem UpwardEnumerable.le_refl {α : Type u} [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] (a : α) : UpwardEnumerable.LE a a :=
@@ -293,7 +307,7 @@ theorem UpwardEnumerable.isSome_succMany? {α : Type u} [UpwardEnumerable α]
   induction n
   · simp [succMany?_zero]
   · rename_i ih
-    simp only [succMany?_succ?]
+    simp only [succMany?_add_one]
     rw [← Option.some_get ih, Option.bind_some]
     apply InfinitelyUpwardEnumerable.isSome_succ?
 
@@ -340,12 +354,12 @@ theorem UpwardEnumerable.succMany_one {α : Type u} [UpwardEnumerable α]
 theorem UpwardEnumerable.succMany_succ {α : Type u} [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} :
     succMany (n + 1) a = succ (succMany n a) := by
-  simp [succMany_eq_get, succMany?_succ?]
+  simp [succMany_eq_get, succMany?_add_one]
 
 theorem UpwardEnumerable.succMany_add_one_eq_succMany_succ {α : Type u} [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} :
     succMany (n + 1) a = (succMany n (succ a)) := by
-  simp [succMany_eq_get, succMany?_succ?_eq_succ?_bind_succMany?]
+  simp [succMany_eq_get, succMany?_add_one_eq_succ?_bind_succMany?]
 
 theorem UpwardEnumerable.succMany_succ_eq_succ_succMany {α : Type u} [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [InfinitelyUpwardEnumerable α] {a : α} :