feat: finish aligning List/Array/Vector.ofFn lemmas (#6838)

This PR completes aligning the (limited) verification API for
`List/Array/Vector.ofFn`.

src/Init/Data/Array/Lemmas.lean

@@ -397,6 +397,10 @@ theorem getElem_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ (i : Nat) (h : i <
 theorem getElem?_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ i : Nat, l[i]? = some a :=
   let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩
 
+theorem mem_of_getElem {l : Array α} {i : Nat} {h} {a : α} (e : l[i] = a) : a ∈ l := by
+  subst e
+  simp
+
 theorem mem_of_getElem? {l : Array α} {i : Nat} {a : α} (e : l[i]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
 

src/Init/Data/Array/OfFn.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Array.Lemmas
+import Init.Data.List.OfFn
+
+/-!
+# Theorems about `Array.ofFn`
+-/
+
+namespace Array
+
+@[simp]
+theorem ofFn_eq_empty_iff {f : Fin n → α} : ofFn f = #[] ↔ n = 0 := by
+  rw [← Array.toList_inj]
+  simp
+
+@[simp 500]
+theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ ∃ i, f i = a := by
+  constructor
+  · intro w
+    obtain ⟨i, h, rfl⟩ := getElem_of_mem w
+    exact ⟨⟨i, by simpa using h⟩, by simp⟩
+  · rintro ⟨i, rfl⟩
+    apply mem_of_getElem (i := i) <;> simp
+
+end Array

src/Init/Data/List/Lemmas.lean

@@ -436,6 +436,10 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ i : Nat, l[i]? = s
   let ⟨n, _, e⟩ := getElem_of_mem h
   exact ⟨n, e ▸ getElem?_eq_getElem _⟩
 
+theorem mem_of_getElem {l : List α} {i : Nat} {h} {a : α} (e : l[i] = a) : a ∈ l := by
+  subst e
+  simp
+
 theorem mem_of_getElem? {l : List α} {i : Nat} {a : α} (e : l[i]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
 

src/Init/Data/List/OfFn.lean

@@ -68,6 +68,15 @@ theorem ofFn_succ {n} (f : Fin (n + 1) → α) : ofFn f = f 0 :: ofFn fun i => f
 theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by
   cases n <;> simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero, reduceCtorEq]
 
+@[simp 500]
+theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ ∃ i, f i = a := by
+  constructor
+  · intro w
+    obtain ⟨i, h, rfl⟩ := getElem_of_mem w
+    exact ⟨⟨i, by simpa using h⟩, by simp⟩
+  · rintro ⟨i, rfl⟩
+    apply mem_of_getElem (i := i) <;> simp
+
 theorem head_ofFn {n} (f : Fin n → α) (h : ofFn f ≠ []) :
     (ofFn f).head h = f ⟨0, Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)⟩ := by
   rw [← getElem_zero (length_ofFn _ ▸ Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)),

src/Init/Data/Vector.lean

@@ -10,3 +10,4 @@ import Init.Data.Vector.Lex
 import Init.Data.Vector.MapIdx
 import Init.Data.Vector.Count
 import Init.Data.Vector.DecidableEq
+import Init.Data.Vector.OfFn

src/Init/Data/Vector/Lemmas.lean

@@ -776,6 +776,10 @@ theorem getElem_of_mem {a} {l : Vector α n} (h : a ∈ l) : ∃ (i : Nat) (h :
 theorem getElem?_of_mem {a} {l : Vector α n} (h : a ∈ l) : ∃ i : Nat, l[i]? = some a :=
   let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩
 
+theorem mem_of_getElem {l : Vector α n} {i : Nat} {h} {a : α} (e : l[i] = a) : a ∈ l := by
+  subst e
+  simp
+
 theorem mem_of_getElem? {l : Vector α n} {i : Nat} {a : α} (e : l[i]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
 
@@ -2136,10 +2140,6 @@ theorem foldr_rel {l : Array α} {f g : α → β → β} {a b : β} (r : β →
 
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
-@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
-    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
-  simp [ofFn]
-
 @[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
   rcases v with ⟨data, rfl⟩
   simp

src/Init/Data/Vector/OfFn.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Vector.Lemmas
+import Init.Data.Array.OfFn
+
+/-!
+# Theorems about `Vector.ofFn`
+-/
+
+namespace Vector
+
+@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
+    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
+  simp [ofFn]
+
+theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
+    (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by
+  simp [getElem?_def]
+
+@[simp 500]
+theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ ∃ i, f i = a := by
+  constructor
+  · intro w
+    obtain ⟨i, h, rfl⟩ := getElem_of_mem w
+    exact ⟨⟨i, by simpa using h⟩, by simp⟩
+  · rintro ⟨i, rfl⟩
+    apply mem_of_getElem (i := i) <;> simp
+
+theorem back_ofFn {n} [NeZero n](f : Fin n → α) :
+    (ofFn f).back = f ⟨n - 1, by have := NeZero.ne n; omega⟩ := by
+  simp [back]
+
+end Vector