feat(List/Basic): add get_eq_get? (#12304)

Should it be `get_eq_get?`, `get_eq_get?_get`, or `get_eq_get_get?`?

Mathlib/Data/List/Basic.lean

@@ -853,6 +853,13 @@ theorem tail_append_of_ne_nil (l l' : List α) (h : l ≠ []) : (l ++ l').tail =
   · simp
 #align list.tail_append_of_ne_nil List.tail_append_of_ne_nil
 
+theorem get_eq_iff {l : List α} {n : Fin l.length} {x : α} : l.get n = x ↔ l.get? n.1 = some x := by
+  simp [get?_eq_some]
+
+theorem get_eq_get? (l : List α) (i : Fin l.length) :
+    l.get i = (l.get? i).get (by simp [get?_eq_get]) := by
+  simp [get_eq_iff]
+
 section deprecated
 set_option linter.deprecated false -- TODO(Mario): make replacements for theorems in this section
 
@@ -1453,10 +1460,6 @@ theorem eq_cons_of_length_one {l : List α} (h : l.length = 1) :
   omega
 #align list.eq_cons_of_length_one List.eq_cons_of_length_one
 
-theorem get_eq_iff {l : List α} {n : Fin l.length} {x : α} : l.get n = x ↔ l.get? n.1 = some x := by
-  rw [get?_eq_some]
-  simp [n.2]
-
 @[deprecated get_eq_iff] -- 2023-01-05
 theorem nthLe_eq_iff {l : List α} {n : ℕ} {x : α} {h} : l.nthLe n h = x ↔ l.get? n = some x :=
   get_eq_iff