fix: harmonize with List

Batteries/Data/Fin/Lemmas.lean

@@ -33,9 +33,15 @@ theorem findSome?_succ {f : Fin (n+1) → Option α} :
 @[simp] theorem findSome?_succ_of_some {f : Fin (n+1) → Option α} (h : f 0 = some x) :
     findSome? f = some x := by simp [findSome?_succ, h]
 
+@[simp] theorem findSome?_succ_of_isSome {f : Fin (n+1) → Option α} (h : (f 0).isSome) :
+    findSome? f = f 0 := by cases _h : f 0 <;> simp_all
+
 @[simp] theorem findSome?_succ_of_none {f : Fin (n+1) → Option α} (h : f 0 = none) :
     findSome? f = findSome? fun i => f i.succ := by simp [findSome?_succ, h]
 
+@[simp] theorem findSome?_succ_of_isNone {f : Fin (n+1) → Option α} (h : (f 0).isNone) :
+    findSome? f = findSome? fun i => f i.succ := by simp_all
+
 theorem exists_of_findSome?_eq_some {f : Fin n → Option α} (h : findSome? f = some x) :
     ∃ i, f i = some x := by
   induction n with
@@ -90,7 +96,6 @@ theorem eq_none_of_findSome?_eq_none {f : Fin n → Option α} (h : findSome? f
       match exists_of_findSome?_eq_some h with
       | ⟨i, h⟩ => rw [hf] at h; contradiction
 
-
 theorem findSome?_isNone_iff {f : Fin n → Option α} :
     (findSome? f).isNone ↔ ∀ i, (f i).isNone := by simp