From ae682ed2257b4ddef3791e451da48955b29a4c0f Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 12 Sep 2025 09:14:28 +0200
Subject: [PATCH] feat: more iterator/range lemmas about `toList` and `toArray`
 (#10244)

This PR adds more lemmas about the `toList` and `toArray` functions on
ranges and iterators. It also renames `Array.mem_toArray` into
`List.mem_toArray`.
---
 src/Init/Data/Array/Attach.lean               |   6 +-
 src/Init/Data/Array/Basic.lean                |   6 +-
 src/Init/Data/Array/Erase.lean                |   2 +-
 src/Init/Data/Array/Lemmas.lean               |  10 +-
 src/Init/Data/Array/Monadic.lean              |   2 +-
 src/Init/Data/Array/Range.lean                |   2 +-
 src/Init/Data/Iterators/Consumers/Loop.lean   |   2 +-
 .../Lemmas/Combinators/Monadic/Attach.lean    |   2 +-
 .../Iterators/Lemmas/Combinators/ULift.lean   |   2 +-
 .../Iterators/Lemmas/Consumers/Collect.lean   |   2 +
 .../Data/Iterators/Lemmas/Consumers/Loop.lean | 108 +++++++++
 .../Lemmas/Consumers/Monadic/Collect.lean     |   6 +-
 .../Lemmas/Consumers/Monadic/Loop.lean        |  40 ++++
 .../Data/Range/Polymorphic/Iterators.lean     |  14 +-
 src/Init/Data/Range/Polymorphic/Lemmas.lean   | 211 ++++++++++++++++++
 .../Data/Range/Polymorphic/NatLemmas.lean     |  13 ++
 16 files changed, 410 insertions(+), 18 deletions(-)

diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean
index e4aed84db2..f17502c1eb 100644
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -121,7 +121,7 @@ theorem pmap_eq_map {p : α → Prop} {f : α → β} {xs : Array α} (H) :
 theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (xs : Array α) {H₁ H₂}
     (h : ∀ a ∈ xs, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f xs H₁ = pmap g xs H₂ := by
   cases xs
-  simp only [mem_toArray] at h
+  simp only [List.mem_toArray] at h
   simp only [List.pmap_toArray, mk.injEq]
   rw [List.pmap_congr_left _ h]
 
@@ -346,7 +346,7 @@ theorem foldl_attach {xs : Array α} {f : β → α → β} {b : β} :
     xs.attach.foldl (fun acc t => f acc t.1) b = xs.foldl f b := by
   rcases xs with ⟨xs⟩
   simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
-    List.foldl_toArray', mem_toArray, List.foldl_subtype]
+    List.foldl_toArray', List.mem_toArray, List.foldl_subtype]
   congr
   ext
   simpa using fun a => List.mem_of_getElem? a
@@ -365,7 +365,7 @@ theorem foldr_attach {xs : Array α} {f : α → β → β} {b : β} :
     xs.attach.foldr (fun t acc => f t.1 acc) b = xs.foldr f b := by
   rcases xs with ⟨xs⟩
   simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
-    List.foldr_toArray', mem_toArray, List.foldr_subtype]
+    List.foldr_toArray', List.mem_toArray, List.foldr_subtype]
   congr
   ext
   simpa using fun a => List.mem_of_getElem? a
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 1173d7602f..8a17862c47 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -108,9 +108,13 @@ instance : Membership α (Array α) where
 theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
-@[simp, grind =] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+@[simp, grind =] theorem _root_.List.mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [mem_def]
 
+@[deprecated List.mem_toArray (since := "2025-09-04")]
+theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l :=
+  List.mem_toArray
+
 @[simp] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
diff --git a/src/Init/Data/Array/Erase.lean b/src/Init/Data/Array/Erase.lean
index 2773f41e12..083f47cfc3 100644
--- a/src/Init/Data/Array/Erase.lean
+++ b/src/Init/Data/Array/Erase.lean
@@ -271,7 +271,7 @@ theorem erase_append [LawfulBEq α] {a : α} {xs ys : Array α} :
     (xs ++ ys).erase a = if a ∈ xs then xs.erase a ++ ys else xs ++ ys.erase a := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.erase_toArray, List.erase_append, mem_toArray]
+  simp only [List.append_toArray, List.erase_toArray, List.erase_append, List.mem_toArray]
   split <;> simp
 
 @[grind =]
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index f19730f92f..57364dac39 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -88,7 +88,7 @@ theorem eq_empty_iff_size_eq_zero : xs = #[] ↔ xs.size = 0 :=
 
 theorem size_pos_of_mem {a : α} {xs : Array α} (h : a ∈ xs) : 0 < xs.size := by
   cases xs
-  simp only [mem_toArray] at h
+  simp only [List.mem_toArray] at h
   simpa using List.length_pos_of_mem h
 
 grind_pattern size_pos_of_mem => a ∈ xs, xs.size
@@ -465,7 +465,7 @@ theorem mem_singleton_self (a : α) : a ∈ #[a] := by simp
 
 theorem mem_of_mem_push_of_mem {a b : α} {xs : Array α} : a ∈ xs.push b → b ∈ xs → a ∈ xs := by
   cases xs
-  simp only [List.push_toArray, mem_toArray, List.mem_append, List.mem_singleton]
+  simp only [List.push_toArray, List.mem_toArray, List.mem_append, List.mem_singleton]
   rintro (h | rfl)
   · intro _
     exact h
@@ -2423,7 +2423,7 @@ abbrev mkArray_succ' := @replicate_succ'
 
 @[simp, grind =] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
   unfold replicate
-  simp only [mem_toArray, List.mem_replicate]
+  simp only [List.mem_toArray, List.mem_replicate]
 
 @[deprecated mem_replicate (since := "2025-03-18")]
 abbrev mem_mkArray := @mem_replicate
@@ -4214,7 +4214,7 @@ variable [LawfulBEq α]
     (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
   rcases xs with ⟨xs⟩
   simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, take_eq_extract,
-    List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, mem_toArray]
+    List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, List.mem_toArray]
 
 theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
     (xs.replace a b)[i]? = xs[i]? := by
@@ -4235,7 +4235,7 @@ theorem getElem_replace_of_ne {xs : Array α} {i : Nat} {h : i < xs.size} (h' :
     (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.replace_toArray, List.replace_append, mem_toArray]
+  simp only [List.append_toArray, List.replace_toArray, List.replace_append, List.mem_toArray]
   split <;> simp
 
 @[grind =] theorem replace_push {xs : Array α} {a b c : α} :
diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean
index 614629bcb4..2f50afcb2b 100644
--- a/src/Init/Data/Array/Monadic.lean
+++ b/src/Init/Data/Array/Monadic.lean
@@ -167,7 +167,7 @@ theorem foldrM_filter [Monad m] [LawfulMonad m] {p : α → Bool} {g : α → β
     (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
     forIn' as b f = forIn' bs b' g := by
   cases as <;> cases bs
-  simp only [mk.injEq, mem_toArray, List.forIn'_toArray] at w h ⊢
+  simp only [mk.injEq, List.mem_toArray, List.forIn'_toArray] at w h ⊢
   exact List.forIn'_congr w hb h
 
 /--
diff --git a/src/Init/Data/Array/Range.lean b/src/Init/Data/Array/Range.lean
index b6ea55ad39..0a8c03f2d5 100644
--- a/src/Init/Data/Array/Range.lean
+++ b/src/Init/Data/Array/Range.lean
@@ -116,7 +116,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
 @[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
     (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
   rw [← List.toArray_range']
-  simp only [List.find?_toArray, mem_toArray]
+  simp only [List.find?_toArray, List.mem_toArray]
   simp [List.find?_range'_eq_some]
 
 @[simp] theorem find?_range'_eq_none {s n : Nat} {p : Nat → Bool} :
diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean
index a5d6268e98..4bfb754de2 100644
--- a/src/Init/Data/Iterators/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Loop.lean
@@ -139,7 +139,7 @@ def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id
     (init : γ) (it : Iter.Partial (α := α) β) : γ :=
   ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
 
-@[always_inline, inline, inherit_doc IterM.size]
+@[always_inline, inline, expose, inherit_doc IterM.size]
 def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
     (it : Iter (α := α) β) : Nat :=
   (IteratorSize.size it.toIterM).run.down
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean
index 071de3052f..90f41a0523 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean
@@ -57,6 +57,6 @@ theorem IterM.map_unattach_toArray_attachWith [Iterator α m β] [Monad m] [Mona
     [LawfulMonad m] [LawfulIteratorCollect α m m] :
     (·.map Subtype.val) <$> (it.attachWith P hP).toArray = it.toArray := by
   rw [← toArray_toList, ← toArray_toList, ← map_unattach_toList_attachWith (it := it) (hP := hP)]
-  simp [-map_unattach_toList_attachWith]
+  simp [-map_unattach_toList_attachWith, -IterM.toArray_toList]
 
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean
index d504f55c86..9be2bf5e7c 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean
@@ -53,6 +53,6 @@ theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β}
     [LawfulIteratorCollect α Id Id] :
     it.uLift.toArray = it.toArray.map ULift.up := by
   rw [← toArray_toList, ← toArray_toList, toList_uLift]
-  simp
+  simp [-toArray_toList]
 
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
index 95490ec822..56927df870 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
@@ -44,11 +44,13 @@ theorem IterM.toListRev_toIter {α β} [Iterator α Id β] [Finite α Id]
     it.toIter.toListRev = it.toListRev.run :=
   (rfl)
 
+@[simp]
 theorem Iter.toList_toArray {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.toArray.toList = it.toList := by
   simp [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toList_toArray]
 
+@[simp]
 theorem Iter.toArray_toList {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.toList.toArray = it.toArray := by
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
index b6e289d8bc..940dc5d9c0 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -14,6 +14,7 @@ public import Init.Data.Iterators.Consumers.Loop
 import all Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Consumers.Monadic.Collect
 import all Init.Data.Iterators.Consumers.Monadic.Collect
+import Init.Data.Array.Monadic
 
 public section
 
@@ -43,6 +44,20 @@ theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
             f out acc) := by
   simp [ForIn.forIn, forIn'_eq, -forIn'_eq_forIn]
 
+@[congr] theorem Iter.forIn'_congr {α β : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+    {ita itb : Iter (α := α) β} (w : ita = itb)
+    {b b' : γ} (hb : b = b')
+    {f : (a' : β) → _ → γ → Id (ForInStep γ)}
+    {g : (a' : β) → _ → γ → Id (ForInStep γ)}
+    (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
+    letI : ForIn' Id (Iter (α := α) β) β _ := Iter.instForIn'
+    forIn' ita b f = forIn' itb b' g := by
+  subst_eqs
+  simp only [← funext_iff] at h
+  rw [← h]
+  rfl
+
 theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
@@ -188,6 +203,13 @@ theorem Iter.mem_toList_iff_isPlausibleIndirectOutput {α β} [Iterator α Id β
         obtain ⟨step, h₁, rfl⟩ := h₁
         simp [heq, IterStep.successor] at h₁
 
+theorem Iter.mem_toArray_iff_isPlausibleIndirectOutput {α β} [Iterator α Id β]
+    [IteratorCollect α Id Id] [Finite α Id]
+    [LawfulIteratorCollect α Id Id] [LawfulDeterministicIterator α Id]
+    {it : Iter (α := α) β} {out : β} :
+    out ∈ it.toArray ↔ it.IsPlausibleIndirectOutput out := by
+  rw [← Iter.toArray_toList, List.mem_toArray, mem_toList_iff_isPlausibleIndirectOutput]
+
 theorem Iter.forIn'_toList {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
@@ -222,6 +244,17 @@ theorem Iter.forIn'_toList {α β : Type w} [Iterator α Id β]
     simp only [ihs h (f := fun out h acc => f out (this ▸ h) acc)]
   · simp
 
+theorem Iter.forIn'_toArray {α β : Type w} [Iterator α Id β]
+    [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    [LawfulDeterministicIterator α Id]
+    {γ : Type x} {it : Iter (α := α) β} {init : γ}
+    {f : (out : β) → _ → γ → m (ForInStep γ)} :
+    letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
+    ForIn'.forIn' it.toArray init f = ForIn'.forIn' it init (fun out h acc => f out (Iter.mem_toArray_iff_isPlausibleIndirectOutput.mpr h) acc) := by
+  simp only [← Iter.toArray_toList (it := it), List.forIn'_toArray, Iter.forIn'_toList]
+
 theorem Iter.forIn'_eq_forIn'_toList {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
@@ -234,6 +267,18 @@ theorem Iter.forIn'_eq_forIn'_toList {α β : Type w} [Iterator α Id β]
   simp only [forIn'_toList]
   congr
 
+theorem Iter.forIn'_eq_forIn'_toArray {α β : Type w} [Iterator α Id β]
+    [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    [LawfulDeterministicIterator α Id]
+    {γ : Type x} {it : Iter (α := α) β} {init : γ}
+    {f : (out : β) → _ → γ → m (ForInStep γ)} :
+    letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
+    ForIn'.forIn' it init f = ForIn'.forIn' it.toArray init (fun out h acc => f out (Iter.mem_toArray_iff_isPlausibleIndirectOutput.mp h) acc) := by
+  simp only [forIn'_toArray]
+  congr
+
 theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
@@ -260,6 +305,15 @@ theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
     rw [ihs h]
   · simp
 
+theorem Iter.forIn_toArray {α β : Type w} [Iterator α Id β]
+    [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {γ : Type x} {it : Iter (α := α) β} {init : γ}
+    {f : β → γ → m (ForInStep γ)} :
+    ForIn.forIn it.toArray init f = ForIn.forIn it init f := by
+  simp only [← Iter.toArray_toList, List.forIn_toArray, forIn_toList]
+
 theorem Iter.foldM_eq_forIn {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
     {m : Type x → Type x'} [Monad m] [IteratorLoop α Id m] {f : γ → β → m γ}
     {init : γ} {it : Iter (α := α) β} :
@@ -301,6 +355,14 @@ theorem Iter.foldlM_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [F
   rw [Iter.foldM_eq_forIn, ← Iter.forIn_toList]
   simp only [List.forIn_yield_eq_foldlM, id_map']
 
+theorem Iter.foldlM_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
+    {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
+    [LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {f : γ → β → m γ} {init : γ} {it : Iter (α := α) β} :
+    it.toArray.foldlM (init := init) f = it.foldM (init := init) f := by
+  rw [Iter.foldM_eq_forIn, ← Iter.forIn_toArray]
+  simp only [Array.forIn_yield_eq_foldlM, id_map']
+
 theorem IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
@@ -324,6 +386,12 @@ theorem Iter.fold_eq_foldM {α β : Type w} {γ : Type x} [Iterator α Id β]
     it.fold (init := init) f = (it.foldM (m := Id) (init := init) (pure <| f · ·)).run := by
   simp [foldM_eq_forIn, fold_eq_forIn]
 
+theorem Iter.fold_eq_fold_toIterM {α β : Type w} {γ : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
+    it.fold (init := init) f = (it.toIterM.fold (init := init) f).run := by
+  rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM]
+
 @[simp]
 theorem Iter.forIn_pure_yield_eq_fold {α β : Type w} {γ : Type x} [Iterator α Id β]
     [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : β → γ → γ} {init : γ}
@@ -344,6 +412,38 @@ theorem Iter.fold_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id 
   generalize it.step = step
   cases step using PlausibleIterStep.casesOn <;> simp
 
+-- The argument `f : γ₁ → γ₂` is intentionally explicit, as it is sometimes not found by unification.
+theorem Iter.fold_hom [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β}
+    (f : γ₁ → γ₂) {g₁ : γ₁ → β → γ₁} {g₂ : γ₂ → β → γ₂} {init : γ₁}
+    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) :
+    it.fold g₂ (f init) = f (it.fold g₁ init) := by
+  -- We cannot reduce to `IterM.fold_hom` because `IterM.fold` is necessarily more restrictive
+  -- w.r.t. the universe of the output.
+  induction it using Iter.inductSteps generalizing init with | step it ihy ihs =>
+  rw [fold_eq_match_step, fold_eq_match_step]
+  split
+  · rw [H, ihy ‹_›]
+  · rw [ihs ‹_›]
+  · simp
+
+theorem Iter.toList_eq_fold {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} :
+    it.toList = it.fold (init := []) (fun l out => l ++ [out]) := by
+  rw [Iter.toList_eq_toList_toIterM, IterM.toList_eq_fold, Iter.fold_eq_fold_toIterM]
+
+theorem Iter.toArray_eq_fold {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} :
+    it.toArray = it.fold (init := #[]) (fun xs out => xs.push out) := by
+  simp only [← toArray_toList, toList_eq_fold]
+  rw [← fold_hom (List.toArray)]
+  simp
+
 @[simp]
 theorem Iter.foldl_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
@@ -352,6 +452,14 @@ theorem Iter.foldl_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [Fi
     it.toList.foldl (init := init) f = it.fold (init := init) f := by
   rw [fold_eq_foldM, List.foldl_eq_foldlM, ← Iter.foldlM_toList]
 
+@[simp]
+theorem Iter.foldl_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
+    it.toArray.foldl (init := init) f = it.fold (init := init) f := by
+  rw [fold_eq_foldM, Array.foldl_eq_foldlM, ← Iter.foldlM_toArray]
+
 @[simp]
 theorem Iter.size_toArray_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
index 87e5445400..c27e8e49f0 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
@@ -67,15 +67,17 @@ theorem IterM.toArray_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
   rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
   simp [bind_pure_comp, pure_bind]
 
+@[simp]
 theorem IterM.toList_toArray [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m]
     {it : IterM (α := α) m β} :
     Array.toList <$> it.toArray = it.toList := by
   simp [IterM.toList]
 
+@[simp]
 theorem IterM.toArray_toList [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] {it : IterM (α := α) m β} :
     List.toArray <$> it.toList = it.toArray := by
-  simp [IterM.toList]
+  simp [IterM.toList, -toList_toArray]
 
 theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM (α := α) m β} :
@@ -153,6 +155,6 @@ theorem LawfulIteratorCollect.toList_eq {α β : Type w} {m : Type w → Type w'
     [hl : LawfulIteratorCollect α m m]
     {it : IterM (α := α) m β} :
     it.toList = (letI : IteratorCollect α m m := .defaultImplementation; it.toList) := by
-  simp [IterM.toList, toArray_eq]
+  simp [IterM.toList, toArray_eq, -IterM.toList_toArray]
 
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
index 370b8442ce..549850054b 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
@@ -60,6 +60,20 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
         IteratorLoop.wellFounded_of_finite it init _ (fun _ => id) (fun out _ acc => (⟨·, .intro⟩) <$> f out acc) := by
   simp only [ForIn.forIn, forIn'_eq]
 
+@[congr] theorem IterM.forIn'_congr {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m m]
+    {ita itb : IterM (α := α) m β} (w : ita = itb)
+    {b b' : γ} (hb : b = b')
+    {f : (a' : β) → _ → γ → m (ForInStep γ)}
+    {g : (a' : β) → _ → γ → m (ForInStep γ)}
+    (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
+    letI : ForIn' m (IterM (α := α) m β) β _ := IterM.instForIn'
+    forIn' ita b f = forIn' itb b' g := by
+  subst_eqs
+  simp only [← funext_iff] at h
+  rw [← h]
+  rfl
+
 theorem IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n]
     [IteratorLoop α m n] [LawfulIteratorLoop α m n]
@@ -200,6 +214,23 @@ theorem IterM.fold_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [I
   intro step
   cases step using PlausibleIterStep.casesOn <;> simp
 
+-- The argument `f : γ₁ → γ₂` is intentionally explicit, as it is sometimes not found by unification.
+theorem IterM.fold_hom {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β}
+    (f : γ₁ → γ₂) {g₁ : γ₁ → β → γ₁} {g₂ : γ₂ → β → γ₂} {init : γ₁}
+    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) :
+    it.fold g₂ (f init) = f <$> (it.fold g₁ init) := by
+  induction it using IterM.inductSteps generalizing init with | step it ihy ihs =>
+  rw [fold_eq_match_step, fold_eq_match_step, map_eq_pure_bind, bind_assoc]
+  apply bind_congr
+  intro step
+  rw [bind_pure_comp]
+  split
+  · rw [H, ihy ‹_›]
+  · rw [ihs ‹_›]
+  · simp
+
 theorem IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m]
@@ -223,6 +254,15 @@ theorem IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator
     simp [ihs h]
   · simp
 
+theorem IterM.toArray_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {it : IterM (α := α) m β} :
+    it.toArray = it.fold (init := #[]) (fun xs out => xs.push out) := by
+  simp only [← toArray_toList, toList_eq_fold]
+  rw [← fold_hom]
+  simp
+
 theorem IterM.drain_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     [Monad m] [IteratorLoop α m m] {it : IterM (α := α) m β} :
     it.drain = it.fold (init := PUnit.unit) (fun _ _ => .unit) :=
diff --git a/src/Init/Data/Range/Polymorphic/Iterators.lean b/src/Init/Data/Range/Polymorphic/Iterators.lean
index a2016c750b..e731d282ed 100644
--- a/src/Init/Data/Range/Polymorphic/Iterators.lean
+++ b/src/Init/Data/Range/Polymorphic/Iterators.lean
@@ -27,7 +27,7 @@ def Internal.iter {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl 
 
 /--
 Returns the elements of the given range as a list in ascending order, given that ranges of the given
-type and shape support this function and the range is finite.
+type and shape are finite and support this function.
 -/
 @[always_inline, inline, expose]
 def toList {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
@@ -37,6 +37,18 @@ def toList {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
     [IteratorCollect (RangeIterator su α) Id Id] : List α :=
   PRange.Internal.iter r |>.toList
 
+/--
+Returns the elements of the given range as an array in ascending order, given that ranges of the
+given type and shape are finite and support this function.
+-/
+@[always_inline, inline, expose]
+def toArray {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    [SupportsUpperBound su α]
+    (r : PRange ⟨sl, su⟩ α)
+    [Iterator (RangeIterator su α) Id α] [Finite (RangeIterator su α) Id]
+    [IteratorCollect (RangeIterator su α) Id Id] : Array α :=
+  PRange.Internal.iter r |>.toArray
+
 /--
 Iterators for ranges implementing `RangeSize` support the `size` function.
 -/
diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean
index 005b4254ca..ec4c325754 100644
--- a/src/Init/Data/Range/Polymorphic/Lemmas.lean
+++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean
@@ -16,6 +16,7 @@ public import Init.Data.Range.Polymorphic.Iterators
 import all Init.Data.Range.Polymorphic.Iterators
 public import Init.Data.Iterators.Consumers.Loop
 import all Init.Data.Iterators.Consumers.Loop
+import Init.Data.Array.Monadic
 
 public section
 
@@ -44,6 +45,12 @@ private theorem Internal.toList_eq_toList_iter {sl su} [UpwardEnumerable α]
     r.toList = (Internal.iter r).toList := by
   rfl
 
+private theorem Internal.toArray_eq_toArray_iter {sl su} [UpwardEnumerable α]
+    [BoundedUpwardEnumerable sl α] [SupportsUpperBound su α] [HasFiniteRanges su α]
+    [LawfulUpwardEnumerable α] {r : PRange ⟨sl, su⟩ α} :
+    r.toArray = (Internal.iter r).toArray := by
+  rfl
+
 public theorem RangeIterator.toList_eq_match {su} [UpwardEnumerable α]
     [SupportsUpperBound su α] [HasFiniteRanges su α]
     [LawfulUpwardEnumerable α]
@@ -61,6 +68,35 @@ public theorem RangeIterator.toList_eq_match {su} [UpwardEnumerable α]
   · simp [*]
   · split <;> rename_i heq' <;> simp [*]
 
+public theorem RangeIterator.toArray_eq_match {su} [UpwardEnumerable α]
+    [SupportsUpperBound su α] [HasFiniteRanges su α]
+    [LawfulUpwardEnumerable α]
+    {it : Iter (α := RangeIterator su α) α} :
+    it.toArray =  match it.internalState.next with
+      | none => #[]
+      | some a => if SupportsUpperBound.IsSatisfied it.internalState.upperBound a then
+          #[a] ++ (⟨⟨UpwardEnumerable.succ? a, it.internalState.upperBound⟩⟩ : Iter (α := RangeIterator su α) α).toArray
+        else
+          #[] := by
+  rw [← Iter.toArray_toList, toList_eq_match]
+  split
+  · rfl
+  · split <;> simp
+
+@[simp]
+public theorem toList_toArray {sl su} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    [SupportsUpperBound su α] [HasFiniteRanges su α] [LawfulUpwardEnumerable α]
+    {r : PRange ⟨sl, su⟩ α} :
+    r.toArray.toList = r.toList := by
+  simp [Internal.toArray_eq_toArray_iter, Internal.toList_eq_toList_iter]
+
+@[simp]
+public theorem toArray_toList {sl su} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    [SupportsUpperBound su α] [HasFiniteRanges su α] [LawfulUpwardEnumerable α]
+    {r : PRange ⟨sl, su⟩ α} :
+    r.toList.toArray = r.toArray := by
+  simp [Internal.toArray_eq_toArray_iter, Internal.toList_eq_toList_iter]
+
 public theorem toList_eq_match {sl su} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
     [SupportsUpperBound su α] [HasFiniteRanges su α]
     [LawfulUpwardEnumerable α]
@@ -73,6 +109,18 @@ public theorem toList_eq_match {sl su} [UpwardEnumerable α] [BoundedUpwardEnume
         [] := by
   rw [Internal.toList_eq_toList_iter, RangeIterator.toList_eq_match]; rfl
 
+public theorem toArray_eq_match {sl su} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    [SupportsUpperBound su α] [HasFiniteRanges su α]
+    [LawfulUpwardEnumerable α]
+    {r : PRange ⟨sl, su⟩ α} :
+    r.toArray = match init? r.lower with
+      | none => #[]
+      | some a => if SupportsUpperBound.IsSatisfied r.upper a then
+        #[a] ++ (PRange.mk (shape := ⟨.open, su⟩) a r.upper).toArray
+      else
+        #[] := by
+  rw [Internal.toArray_eq_toArray_iter, RangeIterator.toArray_eq_match]; rfl
+
 public theorem toList_Rox_eq_toList_Rcx_of_isSome_succ? {su} [UpwardEnumerable α]
     [SupportsUpperBound su α] [HasFiniteRanges su α]
     [LawfulUpwardEnumerable α]
@@ -90,6 +138,14 @@ public theorem toList_open_eq_toList_closed_of_isSome_succ? {su} [UpwardEnumerab
       (PRange.mk (shape := ⟨.closed, su⟩) (UpwardEnumerable.succ? lo |>.get h) hi).toList :=
   toList_Rox_eq_toList_Rcx_of_isSome_succ? h
 
+public theorem toArray_Rox_eq_toList_Rcx_of_isSome_succ? {su} [UpwardEnumerable α]
+    [SupportsUpperBound su α] [HasFiniteRanges su α]
+    [LawfulUpwardEnumerable α]
+    {lo : Bound .open α} {hi} (h : (UpwardEnumerable.succ? lo).isSome) :
+    (PRange.mk (shape := ⟨.open, su⟩) lo hi).toArray =
+      (PRange.mk (shape := ⟨.closed, su⟩) (UpwardEnumerable.succ? lo |>.get h) hi).toArray := by
+  simp [Internal.toArray_eq_toArray_iter, Internal.iter_Rox_eq_iter_Rcx_of_isSome_succ?, h]
+
 public theorem toList_eq_nil_iff {sl su} [UpwardEnumerable α]
     [SupportsUpperBound su α] [HasFiniteRanges su α] [BoundedUpwardEnumerable sl α]
     [LawfulUpwardEnumerable α]
@@ -101,6 +157,14 @@ public theorem toList_eq_nil_iff {sl su} [UpwardEnumerable α]
   simp only
   split <;> rename_i heq <;> simp [heq]
 
+public theorem toArray_eq_empty_iff {sl su} [UpwardEnumerable α]
+    [SupportsUpperBound su α] [HasFiniteRanges su α] [BoundedUpwardEnumerable sl α]
+    [LawfulUpwardEnumerable α]
+    {r : PRange ⟨sl, su⟩ α} :
+    r.toArray = #[] ↔
+      ¬ (∃ a, init? r.lower = some a ∧ SupportsUpperBound.IsSatisfied r.upper a) := by
+  rw [← toArray_toList, List.toArray_eq_iff, Array.toList_empty, toList_eq_nil_iff]
+
 public theorem mem_toList_iff_mem {sl su} [UpwardEnumerable α]
     [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
     [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
@@ -110,6 +174,15 @@ public theorem mem_toList_iff_mem {sl su} [UpwardEnumerable α]
   rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
     Internal.isPlausibleIndirectOutput_iter_iff]
 
+public theorem mem_toArray_iff_mem {sl su} [UpwardEnumerable α]
+    [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
+    [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
+    {r : PRange ⟨sl, su⟩ α}
+    {a : α} : a ∈ r.toArray ↔ a ∈ r := by
+  rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
+    Internal.isPlausibleIndirectOutput_iter_iff]
+
 public theorem BoundedUpwardEnumerable.init?_succ?_closed [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] {lower lower' : Bound .closed α}
     (h : UpwardEnumerable.succ? lower = some lower') :
@@ -301,6 +374,17 @@ public theorem ClosedOpen.toList_succ_succ_eq_map [UpwardEnumerable α] [Support
       (lower...upper).toList.map succ :=
   toList_Rco_succ_succ_eq_map
 
+public theorem toArray_Rco_succ_succ_eq_map [UpwardEnumerable α] [SupportsLowerBound .closed α]
+    [LinearlyUpwardEnumerable α] [InfinitelyUpwardEnumerable α] [SupportsUpperBound .open α]
+    [HasFiniteRanges .open α] [LawfulUpwardEnumerable α] [LawfulOpenUpperBound α]
+    [LawfulUpwardEnumerableLowerBound .closed α] [LawfulUpwardEnumerableUpperBound .open α]
+    {lower : Bound .closed α} {upper : Bound .open α} :
+    ((succ lower)...(succ upper)).toArray =
+      (lower...upper).toArray.map succ := by
+  simp only [← toArray_toList]
+  rw [toList_Rco_succ_succ_eq_map]
+  simp only [List.map_toArray]
+
 private theorem Internal.forIn'_eq_forIn'_iter [UpwardEnumerable α]
     [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
     [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
@@ -324,6 +408,18 @@ public theorem forIn'_eq_forIn'_toList [UpwardEnumerable α]
   simp [Internal.forIn'_eq_forIn'_iter, Internal.toList_eq_toList_iter,
     Iter.forIn'_eq_forIn'_toList]
 
+public theorem forIn'_eq_forIn'_toArray [UpwardEnumerable α]
+    [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
+    [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
+    {r : PRange ⟨sl, su⟩ α}
+    {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m]
+    {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} :
+    ForIn'.forIn' r init f =
+      ForIn'.forIn' r.toArray init (fun a ha acc => f a (mem_toArray_iff_mem.mp ha) acc) := by
+  simp [Internal.forIn'_eq_forIn'_iter, Internal.toArray_eq_toArray_iter,
+    Iter.forIn'_eq_forIn'_toArray]
+
 public theorem forIn'_toList_eq_forIn' [UpwardEnumerable α]
     [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
     [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
@@ -335,6 +431,17 @@ public theorem forIn'_toList_eq_forIn' [UpwardEnumerable α]
       ForIn'.forIn' r init (fun a ha acc => f a (mem_toList_iff_mem.mpr ha) acc) := by
   simp [forIn'_eq_forIn'_toList]
 
+public theorem forIn'_toArray_eq_forIn' [UpwardEnumerable α]
+    [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
+    [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
+    {r : PRange ⟨sl, su⟩ α}
+    {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m]
+    {f : (a : α) → _ → γ → m (ForInStep γ)} :
+    ForIn'.forIn' r.toArray init f =
+      ForIn'.forIn' r init (fun a ha acc => f a (mem_toArray_iff_mem.mpr ha) acc) := by
+  simp [forIn'_eq_forIn'_toArray]
+
 public theorem mem_of_mem_open [UpwardEnumerable α]
     [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
     [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
@@ -431,6 +538,20 @@ public instance {su} [UpwardEnumerable α] [SupportsUpperBound su α] [RangeSize
         · have := LawfulRangeSize.size_eq_zero_of_not_isSatisfied _ _ h'
           simp [*] at this
 
+public theorem length_toList {sl su} [UpwardEnumerable α] [SupportsUpperBound su α]
+    [RangeSize su α] [LawfulUpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    [HasFiniteRanges su α] [LawfulRangeSize su α]
+    {r : PRange ⟨sl, su⟩ α} :
+    r.toList.length = r.size := by
+  simp [PRange.toList, PRange.size]
+
+public theorem size_toArray {sl su} [UpwardEnumerable α] [SupportsUpperBound su α]
+    [RangeSize su α] [LawfulUpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    [HasFiniteRanges su α] [LawfulRangeSize su α]
+    {r : PRange ⟨sl, su⟩ α} :
+    r.toArray.size = r.size := by
+  simp [PRange.toArray, PRange.size]
+
 public theorem isEmpty_iff_forall_not_mem {sl su} [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [BoundedUpwardEnumerable sl α] [SupportsLowerBound sl α] [SupportsUpperBound su α]
     [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
@@ -455,4 +576,94 @@ public theorem isEmpty_iff_forall_not_mem {sl su} [UpwardEnumerable α] [LawfulU
       (Option.some_get hi).symm
     exact h ((init? r.lower).get hi) ⟨hl, hu⟩
 
+theorem Std.PRange.getElem?_toList_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
+    [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
+    [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
+    {r : PRange ⟨.closed, su⟩ α} {i} :
+    r.toList[i]? = (UpwardEnumerable.succMany? i r.lower).filter (SupportsUpperBound.IsSatisfied r.upper) := by
+  induction i generalizing r
+  · rw [PRange.toList_eq_match, UpwardEnumerable.succMany?_zero]
+    simp only [Option.filter_some, decide_eq_true_eq]
+    split <;> simp
+  · rename_i n ih
+    rw [PRange.toList_eq_match]
+    simp only
+    split
+    · simp [UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?]
+      cases hs : UpwardEnumerable.succ? r.lower
+      · rw [PRange.toList_eq_match]
+        simp [BoundedUpwardEnumerable.init?, hs]
+      · rw [toList_Rox_eq_toList_Rcx_of_isSome_succ? (by simp [hs])]
+        rw [ih]
+        simp [hs]
+    · simp only [List.length_nil, Nat.not_lt_zero, not_false_eq_true, getElem?_neg]
+      cases hs : UpwardEnumerable.succMany? (n + 1) r.lower
+      · simp
+      · rename_i hl a
+        simp only [Option.filter_some, decide_eq_true_eq, right_eq_ite_iff]
+        have : UpwardEnumerable.LE r.lower a := ⟨n + 1, hs⟩
+        intro ha
+        exact hl.elim <| LawfulUpwardEnumerableUpperBound.isSatisfied_of_le r.upper _ _ ha this (α := α)
+
+theorem Std.PRange.getElem?_toArray_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
+    [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
+    [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
+    {r : PRange ⟨.closed, su⟩ α} {i} :
+    r.toArray[i]? = (UpwardEnumerable.succMany? i r.lower).filter (SupportsUpperBound.IsSatisfied r.upper) := by
+  rw [← toArray_toList, List.getElem?_toArray, getElem?_toList_Rcx_eq]
+
+theorem Std.PRange.isSome_succMany?_of_lt_length_toList_Rcx [LE α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
+    [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
+    {r : PRange ⟨.closed, su⟩ α} {i} (h : i < r.toList.length) :
+    (UpwardEnumerable.succMany? i r.lower).isSome := by
+  have : r.toList[i]?.isSome := by simp [h]
+  simp only [getElem?_toList_Rcx_eq, Option.isSome_filter] at this
+  exact Option.isSome_of_any this
+
+theorem Std.PRange.isSome_succMany?_of_lt_size_toArray_Rcx [LE α] [UpwardEnumerable α]
+    [LawfulUpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
+    [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
+    {r : PRange ⟨.closed, su⟩ α} {i} (h : i < r.toArray.size) :
+    (UpwardEnumerable.succMany? i r.lower).isSome := by
+  have : r.toArray[i]?.isSome := by simp [h]
+  simp only [getElem?_toArray_Rcx_eq, Option.isSome_filter] at this
+  exact Option.isSome_of_any this
+
+theorem Std.PRange.getElem_toList_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
+    [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
+    [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
+    {r : PRange ⟨.closed, su⟩ α} {i h} :
+    r.toList[i]'h = (UpwardEnumerable.succMany? i r.lower).get
+        (isSome_succMany?_of_lt_length_toList_Rcx h) := by
+  simp [List.getElem_eq_getElem?_get, getElem?_toList_Rcx_eq]
+
+theorem Std.PRange.getElem_toArray_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
+    [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
+    [LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
+    {r : PRange ⟨.closed, su⟩ α} {i h} :
+    r.toArray[i]'h = (UpwardEnumerable.succMany? i r.lower).get
+        (isSome_succMany?_of_lt_size_toArray_Rcx h) := by
+  simp [Array.getElem_eq_getElem?_get, getElem?_toArray_Rcx_eq]
+
+theorem Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons [LE α]
+    [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
+    [SupportsUpperBound su α] [HasFiniteRanges su α] [LawfulUpwardEnumerableUpperBound su α]
+    {r : PRange ⟨.closed, su⟩ α} {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) :
+    cur = (UpwardEnumerable.succMany? pref.length r.lower).get
+        (isSome_succMany?_of_lt_length_toList_Rcx (by simp [h])) := by
+  have : cur = (pref ++ cur :: suff)[pref.length] := by simp
+  simp only [← h] at this
+  simp [this, getElem_toList_Rcx_eq]
+
+theorem Std.PRange.eq_succMany?_of_toArray_Rcx_eq_append_append [LE α]
+    [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
+    [SupportsUpperBound su α] [HasFiniteRanges su α] [LawfulUpwardEnumerableUpperBound su α]
+    {r : PRange ⟨.closed, su⟩ α} {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff) :
+    cur = (UpwardEnumerable.succMany? pref.size r.lower).get
+        (isSome_succMany?_of_lt_size_toArray_Rcx (by simp [h, Nat.add_assoc, Nat.add_comm 1])) := by
+  have : cur = (pref ++ #[cur] ++ suff)[pref.size] := by simp
+  simp only [← h] at this
+  simp [this, getElem_toArray_Rcx_eq]
+
 end Std.PRange
diff --git a/src/Init/Data/Range/Polymorphic/NatLemmas.lean b/src/Init/Data/Range/Polymorphic/NatLemmas.lean
index ec11f9d0d1..fb3905fe3b 100644
--- a/src/Init/Data/Range/Polymorphic/NatLemmas.lean
+++ b/src/Init/Data/Range/Polymorphic/NatLemmas.lean
@@ -25,4 +25,17 @@ theorem toList_Rco_succ_succ {m n : Nat} :
 theorem ClosedOpen.toList_succ_succ {m n : Nat} :
     ((m+1)...(n+1)).toList = (m...n).toList.map (· + 1) := toList_Rco_succ_succ
 
+@[simp]
+theorem Nat.size_Rco {a b : Nat} :
+    (a...b).size = b - a := by
+  simp only [size, Iterators.Iter.size, Iterators.IteratorSize.size, Iterators.Iter.toIterM,
+    Internal.iter, init?, RangeSize.size, Id.run_pure]
+  omega
+
+@[simp]
+theorem Nat.size_Rcc {a b : Nat} :
+    (a...=b).size = b + 1- a := by
+  simp [Std.PRange.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size,
+    Std.PRange.Internal.iter, Std.Iterators.Iter.toIterM, Std.PRange.RangeSize.size]
+
 end Std.PRange.Nat