feat: Fin and Char ranges (#12058)

This PR implements iteration over ranges for `Fin` and `Char`.

To this end, we introduce machinery for pulling back lawfulness of
`UpwardEnumerable` along an injective map and study the function
`Char.ordinal : Char -> Fin Char.numCodePoints`.

src/Init/Data/Char.lean

@@ -9,3 +9,4 @@ prelude
 public import Init.Data.Char.Basic
 public import Init.Data.Char.Lemmas
 public import Init.Data.Char.Order
+public import Init.Data.Char.Ordinal

src/Init/Data/Char/Ordinal.lean

@@ -0,0 +1,242 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Fin.OverflowAware
+public import Init.Data.UInt.Basic
+public import Init.Data.Function
+import Init.Data.Char.Lemmas
+import Init.Data.Char.Order
+import Init.Grind
+
+/-!
+# Bijection between `Char` and `Fin Char.numCodePoints`
+
+In this file, we construct a bijection between `Char` and `Fin Char.numCodePoints` and show that
+it is compatible with various operations. Since `Fin` is simpler than `Char` due to being based
+on natural numbers instead of `UInt32` and not having a hole in the middle (surrogate code points),
+this is sometimes useful to simplify reasoning about `Char`.
+
+We use these declarations in the construction of `Char` ranges, see the module
+`Init.Data.Range.Polymorphic.Char`.
+-/
+
+set_option doc.verso true
+
+public section
+
+namespace Char
+
+/-- The number of surrogate code points. -/
+abbrev numSurrogates : Nat :=
+  -- 0xe000 - 0xd800
+  2048
+
+/-- The size of the {name}`Char` type. -/
+abbrev numCodePoints : Nat :=
+  -- 0x110000 - numSurrogates
+  1112064
+
+/--
+Packs {name}`Char` bijectively into {lean}`Fin Char.numCodePoints` by shifting code points which are
+greater than the surrogate code points by the number of surrogate code points.
+
+The inverse of this function is called {name (scope := "Init.Data.Char.Ordinal")}`Char.ofOrdinal`.
+-/
+def ordinal (c : Char) : Fin Char.numCodePoints :=
+  if h : c.val < 0xd800 then
+    ⟨c.val.toNat, by grind [UInt32.lt_iff_toNat_lt]⟩
+  else
+    ⟨c.val.toNat - Char.numSurrogates, by grind [UInt32.lt_iff_toNat_lt]⟩
+
+/--
+Unpacks {lean}`Fin Char.numCodePoints` bijectively to {name}`Char` by shifting code points which are
+greater than the surrogate code points by the number of surrogate code points.
+
+The inverse of this function is called {name}`Char.ordinal`.
+-/
+def ofOrdinal (f : Fin Char.numCodePoints) : Char :=
+  if h : (f : Nat) < 0xd800 then
+    ⟨UInt32.ofNatLT f (by grind), by grind [UInt32.toNat_ofNatLT]⟩
+  else
+    ⟨UInt32.ofNatLT (f + Char.numSurrogates) (by grind), by grind [UInt32.toNat_ofNatLT]⟩
+
+/--
+Computes the next {name}`Char`, skipping over surrogate code points (which are not valid
+{name}`Char`s) as necessary.
+
+This function is specified by its interaction with {name}`Char.ordinal`, see
+{name (scope := "Init.Data.Char.Ordinal")}`Char.succ?_eq`.
+-/
+def succ? (c : Char) : Option Char :=
+  if h₀ : c.val < 0xd7ff then
+    some ⟨c.val + 1, by grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_add]⟩
+  else if h₁ : c.val = 0xd7ff then
+    some ⟨0xe000, by decide⟩
+  else if h₂ : c.val < 0x10ffff then
+    some ⟨c.val + 1, by
+      simp only [UInt32.lt_iff_toNat_lt, UInt32.reduceToNat, Nat.not_lt, ← UInt32.toNat_inj,
+        UInt32.isValidChar, Nat.isValidChar, UInt32.toNat_add, Nat.reducePow] at *
+      grind⟩
+  else none
+
+/--
+Computes the {name}`m`-th next {name}`Char`, skipping over surrogate code points (which are not
+valid {name}`Char`s) as necessary.
+
+This function is specified by its interaction with {name}`Char.ordinal`, see
+{name (scope := "Init.Data.Char.Ordinal")}`Char.succMany?_eq`.
+-/
+def succMany? (m : Nat) (c : Char) : Option Char :=
+  c.ordinal.addNat? m |>.map Char.ofOrdinal
+
+@[grind =]
+theorem coe_ordinal {c : Char} :
+    (c.ordinal : Nat) =
+      if c.val < 0xd800 then
+        c.val.toNat
+      else
+        c.val.toNat - Char.numSurrogates := by
+  grind [Char.ordinal]
+
+@[simp]
+theorem ordinal_zero : '\x00'.ordinal = 0 := by
+  ext
+  simp [coe_ordinal]
+
+@[grind =]
+theorem val_ofOrdinal {f : Fin Char.numCodePoints} :
+    (Char.ofOrdinal f).val =
+      if h : (f : Nat) < 0xd800 then
+        UInt32.ofNatLT f (by grind)
+      else
+        UInt32.ofNatLT (f + Char.numSurrogates) (by grind) := by
+  grind [Char.ofOrdinal]
+
+@[simp]
+theorem ofOrdinal_ordinal {c : Char} : Char.ofOrdinal c.ordinal = c := by
+  ext
+  simp only [val_ofOrdinal, coe_ordinal, UInt32.ofNatLT_add]
+  split
+  · grind [UInt32.lt_iff_toNat_lt, UInt32.ofNatLT_toNat]
+  · rw [dif_neg]
+    · simp only [← UInt32.toNat_inj, UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+      grind [UInt32.toNat_lt, UInt32.lt_iff_toNat_lt]
+    · grind [UInt32.lt_iff_toNat_lt]
+
+@[simp]
+theorem ordinal_ofOrdinal {f : Fin Char.numCodePoints} : (Char.ofOrdinal f).ordinal = f := by
+  ext
+  simp [coe_ordinal, val_ofOrdinal]
+  split
+  · rw [if_pos, UInt32.toNat_ofNatLT]
+    simpa [UInt32.lt_iff_toNat_lt]
+  · rw [if_neg, UInt32.toNat_add, UInt32.toNat_ofNatLT, UInt32.toNat_ofNatLT, Nat.mod_eq_of_lt,
+      Nat.add_sub_cancel]
+    · grind
+    · simp only [UInt32.lt_iff_toNat_lt, UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow,
+        UInt32.reduceToNat, Nat.not_lt]
+      grind
+
+@[simp]
+theorem ordinal_comp_ofOrdinal : Char.ordinal ∘ Char.ofOrdinal = id := by
+  ext; simp
+
+@[simp]
+theorem ofOrdinal_comp_ordinal : Char.ofOrdinal ∘ Char.ordinal = id := by
+  ext; simp
+
+@[simp]
+theorem ordinal_inj {c d : Char} : c.ordinal = d.ordinal ↔ c = d :=
+  ⟨fun h => by simpa using congrArg Char.ofOrdinal h, (· ▸ rfl)⟩
+
+theorem ordinal_injective : Function.Injective Char.ordinal :=
+  fun _ _ => ordinal_inj.1
+
+@[simp]
+theorem ofOrdinal_inj {f g : Fin Char.numCodePoints} :
+    Char.ofOrdinal f = Char.ofOrdinal g ↔ f = g :=
+  ⟨fun h => by simpa using congrArg Char.ordinal h, (· ▸ rfl)⟩
+
+theorem ofOrdinal_injective : Function.Injective Char.ofOrdinal :=
+   fun _ _ => ofOrdinal_inj.1
+
+theorem ordinal_le_of_le {c d : Char} (h : c ≤ d) : c.ordinal ≤ d.ordinal := by
+  simp only [le_def, UInt32.le_iff_toNat_le] at h
+  simp only [Fin.le_def, coe_ordinal, UInt32.lt_iff_toNat_lt, UInt32.reduceToNat]
+  grind
+
+theorem ofOrdinal_le_of_le {f g : Fin Char.numCodePoints} (h : f ≤ g) :
+    Char.ofOrdinal f ≤ Char.ofOrdinal g := by
+  simp only [Fin.le_def] at h
+  simp only [le_def, val_ofOrdinal, UInt32.ofNatLT_add, UInt32.le_iff_toNat_le]
+  split
+  · simp only [UInt32.toNat_ofNatLT]
+    split
+    · simpa
+    · simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+      grind
+  · simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+    rw [dif_neg (by grind)]
+    simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+    grind
+
+theorem le_iff_ordinal_le {c d : Char} : c ≤ d ↔ c.ordinal ≤ d.ordinal :=
+  ⟨ordinal_le_of_le, fun h => by simpa using ofOrdinal_le_of_le h⟩
+
+theorem le_iff_ofOrdinal_le {f g : Fin Char.numCodePoints} :
+    f ≤ g ↔ Char.ofOrdinal f ≤ Char.ofOrdinal g :=
+  ⟨ofOrdinal_le_of_le, fun h => by simpa using ordinal_le_of_le h⟩
+
+theorem lt_iff_ordinal_lt {c d : Char} : c < d ↔ c.ordinal < d.ordinal := by
+  simp only [Std.lt_iff_le_and_not_ge, le_iff_ordinal_le]
+
+theorem lt_iff_ofOrdinal_lt {f g : Fin Char.numCodePoints} :
+    f < g ↔ Char.ofOrdinal f < Char.ofOrdinal g := by
+  simp only [Std.lt_iff_le_and_not_ge, le_iff_ofOrdinal_le]
+
+theorem succ?_eq {c : Char} : c.succ? = (c.ordinal.addNat? 1).map Char.ofOrdinal := by
+  fun_cases Char.succ? with
+  | case1 h =>
+    rw [Fin.addNat?_eq_some]
+    · simp only [coe_ordinal, Option.map_some, Option.some.injEq, Char.ext_iff, val_ofOrdinal,
+        UInt32.ofNatLT_add, UInt32.reduceOfNatLT]
+      split
+      · simp only [UInt32.ofNatLT_toNat, dite_eq_ite, left_eq_ite_iff, Nat.not_lt,
+          Nat.reduceLeDiff, UInt32.left_eq_add]
+        grind [UInt32.lt_iff_toNat_lt]
+      · grind
+    · simp [coe_ordinal]
+      grind [UInt32.lt_iff_toNat_lt]
+  | case2 =>
+    rw [Fin.addNat?_eq_some]
+    · simp [coe_ordinal, *, Char.ext_iff, val_ofOrdinal, numSurrogates]
+    · simp [coe_ordinal, *, numCodePoints]
+  | case3 =>
+    rw [Fin.addNat?_eq_some]
+    · simp only [coe_ordinal, Option.map_some, Option.some.injEq, Char.ext_iff, val_ofOrdinal,
+        UInt32.ofNatLT_add, UInt32.reduceOfNatLT]
+      split
+      · grind
+      · rw [dif_neg]
+        · simp only [← UInt32.toNat_inj, UInt32.toNat_add, UInt32.reduceToNat, Nat.reducePow,
+            UInt32.toNat_ofNatLT, Nat.mod_add_mod]
+          grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_inj]
+        · grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_inj]
+    · grind [UInt32.lt_iff_toNat_lt]
+  | case4 =>
+    rw [eq_comm]
+    grind [UInt32.lt_iff_toNat_lt]
+
+theorem map_ordinal_succ? {c : Char} : c.succ?.map ordinal = c.ordinal.addNat? 1 := by
+  simp [succ?_eq]
+
+theorem succMany?_eq {m : Nat} {c : Char} :
+    c.succMany? m = (c.ordinal.addNat? m).map Char.ofOrdinal := by
+  rfl
+
+end Char

src/Init/Data/Fin.lean

@@ -11,3 +11,4 @@ public import Init.Data.Fin.Log2
 public import Init.Data.Fin.Iterate
 public import Init.Data.Fin.Fold
 public import Init.Data.Fin.Lemmas
+public import Init.Data.Fin.OverflowAware

src/Init/Data/Fin/OverflowAware.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Fin.Basic
+import Init.Data.Fin.Lemmas
+
+set_option doc.verso true
+
+public section
+
+namespace Fin
+
+/--
+Overflow-aware addition of a natural number to an element of {lean}`Fin n`.
+
+Examples:
+* {lean}`(2 : Fin 3).addNat? 1 = (none : Option (Fin 3))`
+* {lean}`(2 : Fin 4).addNat? 1 = (some 3 : Option (Fin 4))`
+-/
+@[inline]
+protected def addNat? (i : Fin n) (m : Nat) : Option (Fin n) :=
+  if h : i + m < n then some ⟨i + m, h⟩ else none
+
+theorem addNat?_eq_some {i : Fin n} (h : i + m < n) : i.addNat? m = some ⟨i + m, h⟩ := by
+  simp [Fin.addNat?, h]
+
+theorem addNat?_eq_some_iff {i : Fin n} :
+    i.addNat? m = some j ↔ i + m < n ∧ j = i + m := by
+  simp only [Fin.addNat?]
+  split <;> simp [Fin.ext_iff, eq_comm, *]
+
+@[simp]
+theorem addNat?_eq_none_iff {i : Fin n} : i.addNat? m = none ↔ n ≤ i + m := by
+  simp only [Fin.addNat?]
+  split <;> simp_all [Nat.not_lt]
+
+@[simp]
+theorem addNat?_zero {i : Fin n} : i.addNat? 0 = some i := by
+  simp [addNat?_eq_some_iff]
+
+@[grind =]
+theorem addNat?_eq_dif {i : Fin n} :
+    i.addNat? m = if h : i + m < n then some ⟨i + m, h⟩ else none := by
+  rfl
+
+end Fin

src/Init/Data/Option.lean

@@ -15,3 +15,4 @@ public import Init.Data.Option.Attach
 public import Init.Data.Option.List
 public import Init.Data.Option.Monadic
 public import Init.Data.Option.Array
+public import Init.Data.Option.Function

src/Init/Data/Option/Function.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Function
+import Init.Data.Option.Lemmas
+
+public section
+
+namespace Option
+
+theorem map_injective {f : α → β} (hf : Function.Injective f) :
+    Function.Injective (Option.map f) := by
+  intros a b hab
+  cases a <;> cases b
+  · simp
+  · simp at hab
+  · simp at hab
+  · simp only [map_some, some.injEq] at hab
+    simpa using hf hab
+
+end Option

src/Init/Data/Option/Lemmas.lean

@@ -307,12 +307,20 @@ theorem map_id' {x : Option α} : (x.map fun a => a) = x := congrFun map_id x
 
 theorem map_id_apply' {α : Type u} {x : Option α} : Option.map (fun (a : α) => a) x = x := by simp
 
+/-- See `Option.apply_get` for a version that can be rewritten in the reverse direction. -/
 @[simp, grind =] theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} :
     (o.map f).get h = f (o.get (by simpa using h)) := by
   cases o with
   | none => simp at h
   | some a => simp
 
+/-- See `Option.get_map` for a version that can be rewritten in the reverse direction. -/
+theorem apply_get {f : α → β} {o : Option α} {h} :
+    f (o.get h) = (o.map f).get (by simp [h]) := by
+  cases o
+  · simp at h
+  · simp
+
 @[simp] theorem map_map (h : β → γ) (g : α → β) (x : Option α) :
     (x.map g).map h = x.map (h ∘ g) := by
   cases x <;> simp only [map_none, map_some, ·∘·]
@@ -732,6 +740,11 @@ theorem get_merge {o o' : Option α} {f : α → α → α} {i : α} [Std.Lawful
 theorem elim_guard : (guard p a).elim b f = if p a then f a else b := by
   cases h : p a <;> simp [*, guard]
 
+@[simp]
+theorem Option.elim_map {f : α → β} {g' : γ} {g : β → γ} (o : Option α) :
+    (o.map f).elim g' g = o.elim g' (g ∘ f) := by
+  cases o <;> simp
+
 -- I don't see how to construct a good grind pattern to instantiate this.
 @[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) :
   (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl

src/Init/Data/Range/Polymorphic.lean

@@ -10,7 +10,10 @@ public import Init.Data.Range.Polymorphic.Basic
 public import Init.Data.Range.Polymorphic.Iterators
 public import Init.Data.Range.Polymorphic.Stream
 public import Init.Data.Range.Polymorphic.Lemmas
+public import Init.Data.Range.Polymorphic.Map
 
+public import Init.Data.Range.Polymorphic.Fin
+public import Init.Data.Range.Polymorphic.Char
 public import Init.Data.Range.Polymorphic.Nat
 public import Init.Data.Range.Polymorphic.Int
 public import Init.Data.Range.Polymorphic.BitVec

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

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Char.Ordinal
+public import Init.Data.Range.Polymorphic.Fin
+import Init.Data.Range.Polymorphic.Lemmas
+import Init.Data.Range.Polymorphic.Map
+import Init.Data.Char.Order
+
+open Std Std.PRange Std.PRange.UpwardEnumerable
+
+namespace Char
+
+public instance : UpwardEnumerable Char where
+  succ?
+  succMany?
+
+@[simp]
+public theorem pRangeSucc?_eq : PRange.succ? (α := Char) = Char.succ? := rfl
+
+@[simp]
+public theorem pRangeSuccMany?_eq : PRange.succMany? (α := Char) = Char.succMany? := rfl
+
+public instance : Rxc.HasSize Char where
+  size lo hi := Rxc.HasSize.size lo.ordinal hi.ordinal
+
+public instance : Rxo.HasSize Char where
+  size lo hi := Rxo.HasSize.size lo.ordinal hi.ordinal
+
+public instance : Rxi.HasSize Char where
+  size hi := Rxi.HasSize.size hi.ordinal
+
+public instance : Least? Char where
+  least? := some '\x00'
+
+@[simp]
+public theorem least?_eq : Least?.least? (α := Char) = some '\x00' := rfl
+
+def map : Map Char (Fin Char.numCodePoints) where
+  toFun := Char.ordinal
+  injective := ordinal_injective
+  succ?_toFun := by simp [succ?_eq]
+  succMany?_toFun := by simp [succMany?_eq]
+
+@[simp]
+theorem toFun_map : map.toFun = Char.ordinal := rfl
+
+instance : Map.PreservesLE map where
+  le_iff := by simp [le_iff_ordinal_le]
+
+instance : Map.PreservesRxcSize map where
+  size_eq := rfl
+
+instance : Map.PreservesRxoSize map where
+  size_eq := rfl
+
+instance : Map.PreservesRxiSize map where
+  size_eq := rfl
+
+instance : Map.PreservesLeast? map where
+  map_least? := by simp
+
+public instance : LawfulUpwardEnumerable Char := .ofMap map
+public instance : LawfulUpwardEnumerableLE Char := .ofMap map
+public instance : LawfulUpwardEnumerableLT Char := .ofMap map
+public instance : LawfulUpwardEnumerableLeast? Char := .ofMap map
+public instance : Rxc.LawfulHasSize Char := .ofMap map
+public instance : Rxc.IsAlwaysFinite Char := .ofMap map
+public instance : Rxo.LawfulHasSize Char := .ofMap map
+public instance : Rxo.IsAlwaysFinite Char := .ofMap map
+public instance : Rxi.LawfulHasSize Char := .ofMap map
+public instance : Rxi.IsAlwaysFinite Char := .ofMap map
+
+end Char

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

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Range.Polymorphic.Instances
+public import Init.Data.Fin.OverflowAware
+import Init.Grind
+
+public section
+
+open Std Std.PRange
+
+namespace Fin
+
+instance : UpwardEnumerable (Fin n) where
+  succ? i := i.addNat? 1
+  succMany? m i := i.addNat? m
+
+@[simp, grind =]
+theorem pRangeSucc?_eq : PRange.succ? (α := Fin n) = (·.addNat? 1) := rfl
+
+@[simp, grind =]
+theorem pRangeSuccMany?_eq : PRange.succMany? m (α := Fin n) = (·.addNat? m) :=
+  rfl
+
+instance : LawfulUpwardEnumerable (Fin n) where
+  ne_of_lt a b := by grind [UpwardEnumerable.LT]
+  succMany?_zero a := by simp
+  succMany?_add_one m a := by grind
+
+instance : LawfulUpwardEnumerableLE (Fin n) where
+  le_iff x y := by
+    simp only [le_def, UpwardEnumerable.LE, pRangeSuccMany?_eq, Fin.addNat?_eq_dif,
+      Option.dite_none_right_eq_some, Option.some.injEq, ← val_inj, exists_prop]
+    exact ⟨fun h => ⟨y - x, by grind⟩, by grind⟩
+
+instance : Least? (Fin 0) where
+  least? := none
+
+instance : LawfulUpwardEnumerableLeast? (Fin 0) where
+  least?_le a := False.elim (Nat.not_lt_zero _ a.isLt)
+
+@[simp]
+theorem least?_eq_of_zero : Least?.least? (α := Fin 0) = none := rfl
+
+instance [NeZero n] : Least? (Fin n) where
+  least? := some 0
+
+instance [NeZero n] : LawfulUpwardEnumerableLeast? (Fin n) where
+  least?_le a := ⟨0, rfl, (LawfulUpwardEnumerableLE.le_iff 0 a).1 (Fin.zero_le _)⟩
+
+@[simp]
+theorem least?_eq [NeZero n] : Least?.least? (α := Fin n) = some 0 := rfl
+
+instance : LawfulUpwardEnumerableLT (Fin n) := inferInstance
+
+instance : Rxc.HasSize (Fin n) where
+  size lo hi := hi + 1 - lo
+
+@[grind =]
+theorem rxcHasSize_eq :
+    Rxc.HasSize.size (α := Fin n) = fun (lo hi : Fin n) => (hi + 1 - lo : Nat) := rfl
+
+instance : Rxc.LawfulHasSize (Fin n) where
+  size_eq_zero_of_not_le bound x := by grind
+  size_eq_one_of_succ?_eq_none lo hi := by grind
+  size_eq_succ_of_succ?_eq_some lo hi x := by grind
+
+instance : Rxc.IsAlwaysFinite (Fin n) := inferInstance
+
+instance : Rxo.HasSize (Fin n) := .ofClosed
+instance : Rxo.LawfulHasSize (Fin n) := inferInstance
+instance : Rxo.IsAlwaysFinite (Fin n) := inferInstance
+
+instance : Rxi.HasSize (Fin n) where
+  size lo := n - lo
+
+@[grind =]
+theorem rxiHasSize_eq :
+    Rxi.HasSize.size (α := Fin n) = fun (lo : Fin n) => (n - lo : Nat) := rfl
+
+instance : Rxi.LawfulHasSize (Fin n) where
+  size_eq_one_of_succ?_eq_none x := by grind
+  size_eq_succ_of_succ?_eq_some lo lo' := by grind
+
+instance : Rxi.IsAlwaysFinite (Fin n) := inferInstance
+
+end Fin

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

@@ -0,0 +1,195 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Range.Polymorphic.Instances
+public import Init.Data.Function
+import Init.Data.Order.Lemmas
+import Init.Data.Option.Function
+
+public section
+
+/-!
+# Mappings between `UpwardEnumerable` types
+
+In this file we build machinery for pulling back lawfulness properties for `UpwardEnumerable` along
+injective functions that commute with the relevant operations.
+-/
+
+namespace Std
+
+namespace PRange
+
+namespace UpwardEnumerable
+
+/--
+An injective mapping between two types implementing `UpwardEnumerable` that commutes with `succ?`
+and `succMany?`.
+
+Having such a mapping means that all of the `Prop`-valued lawfulness classes around
+`UpwardEnumerable` can be pulled back.
+-/
+structure Map (α : Type u) (β : Type v) [UpwardEnumerable α] [UpwardEnumerable β] where
+  toFun : α → β
+  injective : Function.Injective toFun
+  succ?_toFun (a : α) : succ? (toFun a) = (succ? a).map toFun
+  succMany?_toFun (n : Nat) (a : α) : succMany? n (toFun a) = (succMany? n a).map toFun
+
+namespace Map
+
+variable [UpwardEnumerable α] [UpwardEnumerable β]
+
+theorem succ?_eq_none_iff (f : Map α β) {a : α} :
+    succ? a = none ↔ succ? (f.toFun a) = none := by
+  rw [← (Option.map_injective f.injective).eq_iff, Option.map_none, ← f.succ?_toFun]
+
+theorem succ?_eq_some_iff (f : Map α β) {a b : α} :
+    succ? a = some b ↔ succ? (f.toFun a) = some (f.toFun b) := by
+  rw [← (Option.map_injective f.injective).eq_iff, Option.map_some, ← f.succ?_toFun]
+
+theorem le_iff (f : Map α β) {a b : α} :
+    UpwardEnumerable.LE a b ↔ UpwardEnumerable.LE (f.toFun a) (f.toFun b) := by
+  simp only [UpwardEnumerable.LE, f.succMany?_toFun, Option.map_eq_some_iff]
+  refine ⟨fun ⟨n, hn⟩ => ⟨n, b, by simp [hn]⟩, fun ⟨n, c, hn⟩ => ⟨n, ?_⟩⟩
+  rw [hn.1, Option.some_inj, f.injective hn.2]
+
+theorem lt_iff (f : Map α β) {a b : α} :
+    UpwardEnumerable.LT a b ↔ UpwardEnumerable.LT (f.toFun a) (f.toFun b) := by
+  simp only [UpwardEnumerable.LT, f.succMany?_toFun, Option.map_eq_some_iff]
+  refine ⟨fun ⟨n, hn⟩ => ⟨n, b, by simp [hn]⟩, fun ⟨n, c, hn⟩ => ⟨n, ?_⟩⟩
+  rw [hn.1, Option.some_inj, f.injective hn.2]
+
+theorem succ?_toFun' (f : Map α β) : succ? ∘ f.toFun = Option.map f.toFun ∘ succ? := by
+  ext
+  simp [f.succ?_toFun]
+
+/-- Compatibility class for `Map` and `≤`. -/
+class PreservesLE [LE α] [LE β] (f : Map α β) where
+  le_iff : a ≤ b ↔ f.toFun a ≤ f.toFun b
+
+/-- Compatibility class for `Map` and `<`. -/
+class PreservesLT [LT α] [LT β] (f : Map α β) where
+  lt_iff : a < b ↔ f.toFun a < f.toFun b
+
+/-- Compatibility class for `Map` and `Rxc.HasSize`. -/
+class PreservesRxcSize [Rxc.HasSize α] [Rxc.HasSize β] (f : Map α β) where
+  size_eq : Rxc.HasSize.size a b = Rxc.HasSize.size (f.toFun a) (f.toFun b)
+
+/-- Compatibility class for `Map` and `Rxo.HasSize`. -/
+class PreservesRxoSize [Rxo.HasSize α] [Rxo.HasSize β] (f : Map α β) where
+  size_eq : Rxo.HasSize.size a b = Rxo.HasSize.size (f.toFun a) (f.toFun b)
+
+/-- Compatibility class for `Map` and `Rxi.HasSize`. -/
+class PreservesRxiSize [Rxi.HasSize α] [Rxi.HasSize β] (f : Map α β) where
+  size_eq : Rxi.HasSize.size b = Rxi.HasSize.size (f.toFun b)
+
+/-- Compatibility class for `Map` and `Least?`. -/
+class PreservesLeast? [Least? α] [Least? β] (f : Map α β) where
+  map_least? : Least?.least?.map f.toFun = Least?.least?
+
+end UpwardEnumerable.Map
+
+open UpwardEnumerable
+
+variable [UpwardEnumerable α] [UpwardEnumerable β]
+
+theorem LawfulUpwardEnumerable.ofMap [LawfulUpwardEnumerable β] (f : Map α β) :
+    LawfulUpwardEnumerable α where
+  ne_of_lt a b := by
+    simpa only [f.lt_iff, ← f.injective.ne_iff] using LawfulUpwardEnumerable.ne_of_lt _ _
+  succMany?_zero a := by
+    apply Option.map_injective f.injective
+    simpa [← f.succMany?_toFun] using LawfulUpwardEnumerable.succMany?_zero _
+  succMany?_add_one n a := by
+    apply Option.map_injective f.injective
+    rw [← f.succMany?_toFun, LawfulUpwardEnumerable.succMany?_add_one,
+      f.succMany?_toFun, Option.bind_map, Map.succ?_toFun', Option.map_bind]
+
+instance [LE α] [LT α] [LawfulOrderLT α] [LE β] [LT β] [LawfulOrderLT β] (f : Map α β)
+    [f.PreservesLE] : f.PreservesLT where
+  lt_iff := by simp [lt_iff_le_and_not_ge, Map.PreservesLE.le_iff (f := f)]
+
+theorem LawfulUpwardEnumerableLE.ofMap [LE α] [LE β] [LawfulUpwardEnumerableLE β] (f : Map α β)
+    [f.PreservesLE] : LawfulUpwardEnumerableLE α where
+  le_iff := by simp [Map.PreservesLE.le_iff (f := f), f.le_iff, LawfulUpwardEnumerableLE.le_iff]
+
+theorem LawfulUpwardEnumerableLT.ofMap [LT α] [LT β] [LawfulUpwardEnumerableLT β] (f : Map α β)
+    [f.PreservesLT] : LawfulUpwardEnumerableLT α where
+  lt_iff := by simp [Map.PreservesLT.lt_iff (f := f), f.lt_iff, LawfulUpwardEnumerableLT.lt_iff]
+
+theorem LawfulUpwardEnumerableLeast?.ofMap [Least? α] [Least? β] [LawfulUpwardEnumerableLeast? β]
+    (f : Map α β) [f.PreservesLeast?] : LawfulUpwardEnumerableLeast? α where
+  least?_le a := by
+    obtain ⟨l, hl, hl'⟩ := LawfulUpwardEnumerableLeast?.least?_le (f.toFun a)
+    have : (Least?.least? (α := α)).isSome := by
+      rw [← Option.isSome_map (f := f.toFun), Map.PreservesLeast?.map_least?,
+        hl, Option.isSome_some]
+    refine ⟨Option.get _ this, by simp, ?_⟩
+    rw [f.le_iff, Option.apply_get (f := f.toFun)]
+    simpa [Map.PreservesLeast?.map_least?, hl] using hl'
+
+end PRange
+
+open PRange PRange.UpwardEnumerable
+
+variable [UpwardEnumerable α] [UpwardEnumerable β]
+
+theorem Rxc.LawfulHasSize.ofMap [LE α] [LE β] [Rxc.HasSize α] [Rxc.HasSize β] [Rxc.LawfulHasSize β]
+    (f : Map α β) [f.PreservesLE] [f.PreservesRxcSize] : Rxc.LawfulHasSize α where
+  size_eq_zero_of_not_le a b := by
+    simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f)] using
+      Rxc.LawfulHasSize.size_eq_zero_of_not_le _ _
+  size_eq_one_of_succ?_eq_none lo hi := by
+    simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f),
+        f.succ?_eq_none_iff] using
+      Rxc.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _
+  size_eq_succ_of_succ?_eq_some lo hi lo' := by
+    simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f),
+        f.succ?_eq_some_iff] using
+      Rxc.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _
+
+theorem Rxo.LawfulHasSize.ofMap [LT α] [LT β] [Rxo.HasSize α] [Rxo.HasSize β] [Rxo.LawfulHasSize β]
+    (f : Map α β) [f.PreservesLT] [f.PreservesRxoSize] : Rxo.LawfulHasSize α where
+  size_eq_zero_of_not_le a b := by
+    simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f)] using
+      Rxo.LawfulHasSize.size_eq_zero_of_not_le _ _
+  size_eq_one_of_succ?_eq_none lo hi := by
+    simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f),
+        f.succ?_eq_none_iff] using
+      Rxo.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _
+  size_eq_succ_of_succ?_eq_some lo hi lo' := by
+    simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f),
+        f.succ?_eq_some_iff] using
+      Rxo.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _
+
+theorem Rxi.LawfulHasSize.ofMap [Rxi.HasSize α] [Rxi.HasSize β] [Rxi.LawfulHasSize β]
+    (f : Map α β) [f.PreservesRxiSize] : Rxi.LawfulHasSize α where
+  size_eq_one_of_succ?_eq_none lo := by
+    simpa [Map.PreservesRxiSize.size_eq (f := f), f.succ?_eq_none_iff] using
+      Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none _
+  size_eq_succ_of_succ?_eq_some lo lo' := by
+    simpa [Map.PreservesRxiSize.size_eq (f := f), f.succ?_eq_some_iff] using
+      Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _
+
+theorem Rxc.IsAlwaysFinite.ofMap [LE α] [LE β] [Rxc.IsAlwaysFinite β] (f : Map α β)
+    [f.PreservesLE] : Rxc.IsAlwaysFinite α where
+  finite init hi := by
+    obtain ⟨n, hn⟩ := Rxc.IsAlwaysFinite.finite (f.toFun init) (f.toFun hi)
+    exact ⟨n, by simpa [f.succMany?_toFun, Map.PreservesLE.le_iff (f := f)] using hn⟩
+
+theorem Rxo.IsAlwaysFinite.ofMap [LT α] [LT β] [Rxo.IsAlwaysFinite β] (f : Map α β)
+    [f.PreservesLT] : Rxo.IsAlwaysFinite α where
+  finite init hi := by
+    obtain ⟨n, hn⟩ := Rxo.IsAlwaysFinite.finite (f.toFun init) (f.toFun hi)
+    exact ⟨n, by simpa [f.succMany?_toFun, Map.PreservesLT.lt_iff (f := f)] using hn⟩
+
+theorem Rxi.IsAlwaysFinite.ofMap [Rxi.IsAlwaysFinite β] (f : Map α β) : Rxi.IsAlwaysFinite α where
+  finite init := by
+    obtain ⟨n, hn⟩ := Rxi.IsAlwaysFinite.finite (f.toFun init)
+    exact ⟨n, by simpa [f.succMany?_toFun] using hn⟩
+
+end Std

src/Init/Prelude.lean

@@ -2810,6 +2810,8 @@ structure Char where
   /-- The value must be a legal scalar value. -/
   valid : val.isValidChar
 
+grind_pattern Char.valid => self.val
+
 private theorem isValidChar_UInt32 {n : Nat} (h : n.isValidChar) : LT.lt n UInt32.size :=
   match h with
   | Or.inl h      => Nat.lt_trans h (of_decide_eq_true rfl)

tests/lean/run/charrange.lean

@@ -0,0 +1,29 @@
+module
+
+def s₁ : String := Id.run do
+  let mut ans := ""
+  for c in 'a'...='z' do
+    ans := ans.push c
+  return ans
+
+/-- info: "abcdefghijklmnopqrstuvwxyz" -/
+#guard_msgs in
+#eval s₁
+
+def s₂ : String := Id.run do
+  let mut ans := ""
+  for c in 'a'...'z' do
+    ans := ans.push c
+  return ans
+
+/-- info: "abcdefghijklmnopqrstuvwxy" -/
+#guard_msgs in
+#eval s₂
+
+/-- info: 122 -/
+#guard_msgs in
+#eval (*...'z').size
+
+/-- info: 1112064 -/
+#guard_msgs in
+#eval (*...* : Std.Rii Char).size