feat: prove findMap?_map

Batteries/Data/List/Lemmas.lean

@@ -681,6 +681,14 @@ theorem eq_none_of_findMap?_eq_none_of_mem {f : α → Option β} {xs : List α}
       · apply ih h
         assumption
 
+theorem findMap?_map {g : α → β} {f : β → Option γ} {xs : List α} :
+    (xs.map g).findMap? f = xs.findMap? fun x => f (g x) := by
+  induction xs with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [map_cons, findMap?_cons]
+    cases (f (g x)) <;> simp [ih]
+
 proof_wanted findMap?_isSome {f : α → Option β} {xs : List α} :
     (xs.findMap? f).isSome ↔ ∃ x ∈ xs, (f x).isSome
 
@@ -698,9 +706,6 @@ proof_wanted findMap?_flatMap {g : α → List β} {f : β → Option γ} {xs :
 proof_wanted findMap?_flatten {f : α → Option β} {xss : List (List α)} :
     xss.flatten.findMap? f = xss.findMap? fun xs => xs.findMap? f
 
-proof_wanted findMap?_map {g : α → β} {f : β → Option γ} {xs : List α} :
-    (xs.map g).findMap? f = xs.findMap? fun x => f (g x)
-
 /-! ### deprecations -/
 
 @[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff