diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 38cfda4d8e..f43e625e08 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -11,6 +11,7 @@ import Init.Data.List.Range
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
 import Init.Data.List.Monadic
+import Init.Data.List.OfFn
 import Init.Data.Array.Mem
 import Init.Data.Array.DecidableEq
 import Init.TacticsExtra
@@ -908,7 +909,7 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
   obtain ⟨m, eq, w⟩ := t
   · refine ⟨m, by simpa [map_eq_foldl] using eq, ?_⟩
     intro i h
-    simp [eq] at w
+    simp only [eq] at w
     specialize w ⟨i, h⟩ h
     simpa [map_eq_foldl] using w
   · exact ⟨h0, rfl, nofun⟩
@@ -1615,6 +1616,9 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   apply ext'
   simp
 
+@[simp] theorem toArray_ofFn (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f := by
+  ext <;> simp
+
 end List
 
 namespace Array
@@ -1622,6 +1626,9 @@ namespace Array
 @[simp] theorem mapM_id {l : Array α} {f : α → Id β} : l.mapM f = l.map f := by
   induction l; simp_all
 
+@[simp] theorem toList_ofFn (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f := by
+  apply List.ext_getElem <;> simp
+
 end Array
 
 /-! ### Deprecations -/
diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean
index 1ac4880a6f..d30d633127 100644
--- a/src/Init/Data/List.lean
+++ b/src/Init/Data/List.lean
@@ -25,3 +25,4 @@ import Init.Data.List.Perm
 import Init.Data.List.Sort
 import Init.Data.List.ToArray
 import Init.Data.List.MapIdx
+import Init.Data.List.OfFn
diff --git a/src/Init/Data/List/OfFn.lean b/src/Init/Data/List/OfFn.lean
new file mode 100644
index 0000000000..193fc494b8
--- /dev/null
+++ b/src/Init/Data/List/OfFn.lean
@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Kim Morrison
+-/
+prelude
+import Init.Data.List.Basic
+import Init.Data.Fin.Fold
+
+/-!
+# Theorems about `List.ofFn`
+-/
+
+namespace List
+
+/--
+`ofFn f` with `f : fin n → α` returns the list whose ith element is `f i`
+```
+ofFn f = [f 0, f 1, ... , f (n - 1)]
+```
+-/
+def ofFn {n} (f : Fin n → α) : List α := Fin.foldr n (f · :: ·) []
+
+@[simp]
+theorem length_ofFn (f : Fin n → α) : (ofFn f).length = n := by
+  simp only [ofFn]
+  induction n with
+  | zero => simp
+  | succ n ih => simp [Fin.foldr_succ, ih]
+
+@[simp]
+protected theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length) :
+    (ofFn f)[i] = f ⟨i, by simp_all⟩ := by
+  simp only [ofFn]
+  induction n generalizing i with
+  | zero => simp at h
+  | succ n ih =>
+    match i with
+    | 0 => simp [Fin.foldr_succ]
+    | i+1 =>
+      simp only [Fin.foldr_succ]
+      apply ih
+      simp_all
+
+@[simp]
+protected theorem getElem?_ofFn (f : Fin n → α) (i) : (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none :=
+  if h : i < (ofFn f).length
+  then by
+    rw [getElem?_eq_getElem h, List.getElem_ofFn]
+    · simp only [length_ofFn] at h; simp [h]
+  else by
+    rw [dif_neg] <;>
+    simpa using h
+
+end List