more renamings

Author: datokrat

src/Init/Data/Array/Lex/Lemmas.lean

@@ -68,7 +68,7 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     simp only [bind_pure_comp, map_pure]
     rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
   simp only [Std.toList_roo_eq_toList_rco_of_isSome_succ? (lo := 0) (h := rfl),
-    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_Rco_succ_succ,
+    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_rco_succ_succ,
     Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil,
     Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero]
   cases lt a b

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

@@ -16,44 +16,64 @@ namespace Std.PRange.Nat
 theorem succ_eq {n : Nat} : succ n = n + 1 :=
   rfl
 
-theorem toList_Rco_succ_succ {m n : Nat} :
+theorem toList_rco_succ_succ {m n : Nat} :
     ((m+1)...(n+1)).toList = (m...n).toList.map (· + 1) := by
   simp only [← succ_eq]
   rw [Std.Rco.toList_succ_succ_eq_map]
 
-@[deprecated toList_Rco_succ_succ (since := "2025-08-22")]
-theorem ClosedOpen.toList_succ_succ {m n : Nat} :
-    ((m+1)...(n+1)).toList = (m...n).toList.map (· + 1) := toList_Rco_succ_succ
+@[deprecated toList_rco_succ_succ (since := "2025-10-30")]
+def toList_Rco_succ_succ := @toList_rco_succ_succ
+
+@[deprecated toList_rco_succ_succ (since := "2025-08-22")]
+def ClosedOpen.toList_succ_succ := @toList_rco_succ_succ
 
 @[simp]
-theorem size_Rcc {a b : Nat} :
+theorem size_rcc {a b : Nat} :
     (a...=b).size = b + 1 - a := by
   simp [Rcc.size, Rxc.HasSize.size]
 
+@[deprecated size_rcc (since := "2025-10-30")]
+def size_Rcc := @size_rcc
+
 @[simp]
-theorem size_Rco {a b : Nat} :
+theorem size_rco {a b : Nat} :
     (a...b).size = b - a := by
   simp only [Rco.size, Rxo.HasSize.size, Rxc.HasSize.size]
   omega
 
+@[deprecated size_rco (since := "2025-10-30")]
+def size_Rco := @size_rco
+
 @[simp]
-theorem size_Roc {a b : Nat} :
+theorem size_roc {a b : Nat} :
     (a<...=b).size = b - a := by
   simp [Roc.size, Rxc.HasSize.size]
 
+@[deprecated size_roc (since := "2025-10-30")]
+def size_Roc := @size_roc
+
 @[simp]
-theorem size_Roo {a b : Nat} :
+theorem size_roo {a b : Nat} :
     (a<...b).size = b - a - 1 := by
   simp [Roo.size, Rxo.HasSize.size, Rxc.HasSize.size]
 
+@[deprecated size_roo (since := "2025-10-30")]
+def size_Roo := @size_roo
+
 @[simp]
-theorem size_Ric {b : Nat} :
+theorem size_ric {b : Nat} :
     (*...=b).size = b + 1 := by
   simp [Ric.size, Rxc.HasSize.size]
 
+@[deprecated size_ric (since := "2025-10-30")]
+def size_Ric := @size_ric
+
 @[simp]
-theorem size_Rio {b : Nat} :
+theorem size_rio {b : Nat} :
     (*...b).size = b := by
   simp [Rio.size, Rxo.HasSize.size, Rxc.HasSize.size]
 
+@[deprecated size_rio (since := "2025-10-30")]
+def size_Rio := @size_rio
+
 end Std.PRange.Nat

src/Init/Data/Slice/Array/Lemmas.lean

@@ -20,7 +20,7 @@ open Std.Iterators Std.PRange
 
 namespace Std.Slice.Array
 
-theorem internalIter_Rco_eq {α : Type u} {s : Subarray α} :
+theorem internalIter_rco_eq {α : Type u} {s : Subarray α} :
     Internal.iter s = (Rco.Internal.iter (s.start...<s.stop)
       |>.attachWith (· < s.array.size)
         (fun out h => h
@@ -40,7 +40,7 @@ theorem toList_internalIter {α : Type u} {s : Subarray α} :
               |> Rco.lt_upper_of_mem
               |> (Nat.lt_of_lt_of_le · s.stop_le_array_size))
         |>.map fun i => s.array[i.1]) := by
-  rw [internalIter_Rco_eq, Iter.toList_map, Iter.toList_uLift, Iter.toList_attachWith]
+  rw [internalIter_rco_eq, Iter.toList_map, Iter.toList_uLift, Iter.toList_attachWith]
   simp [Rco.toList]
 
 public instance : LawfulSliceSize (Internal.SubarrayData α) where