From 1e98fd7f2d965ab035dbf1099fb4a4ffde16b151 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 6 Nov 2024 21:02:25 +1100
Subject: [PATCH] feat: add another List.find?_eq_some lemma (#5974)

Inspired by https://github.com/leanprover-community/mathlib4/pull/18593
---
 src/Init/Data/List/Find.lean      |  8 ++++++--
 src/Init/Data/List/Nat/Find.lean  | 26 ++++++++++++++++++++++++++
 src/Init/Data/List/Nat/Range.lean |  4 ++--
 3 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index 0efb96bc0001..1a6ab8291bde 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -206,7 +206,8 @@ theorem IsInfix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (
 @[simp] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
   induction l <;> simp [find?_cons]; split <;> simp [*]
 
-theorem find?_eq_some : xs.find? p = some b ↔ p b ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ a ∈ as, !p a := by
+theorem find?_eq_some_iff_append :
+    xs.find? p = some b ↔ p b ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ a ∈ as, !p a := by
   induction xs with
   | nil => simp
   | cons x xs ih =>
@@ -242,6 +243,9 @@ theorem find?_eq_some : xs.find? p = some b ↔ p b ∧ ∃ as bs, xs = as ++ b
           cases h₁
           simp
 
+@[deprecated find?_eq_some_iff_append (since := "2024-11-06")]
+abbrev find?_eq_some := @find?_eq_some_iff_append
+
 @[simp]
 theorem find?_cons_eq_some : (a :: xs).find? p = some b ↔ (p a ∧ a = b) ∨ (!p a ∧ xs.find? p = some b) := by
   rw [find?_cons]
@@ -347,7 +351,7 @@ theorem find?_flatten_eq_some {xs : List (List α)} {p : α → Bool} {a : α} :
     xs.flatten.find? p = some a ↔
       p a ∧ ∃ as ys zs bs, xs = as ++ (ys ++ a :: zs) :: bs ∧
         (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by
-  rw [find?_eq_some]
+  rw [find?_eq_some_iff_append]
   constructor
   · rintro ⟨h, ⟨ys, zs, h₁, h₂⟩⟩
     refine ⟨h, ?_⟩
diff --git a/src/Init/Data/List/Nat/Find.lean b/src/Init/Data/List/Nat/Find.lean
index d5e950381ca6..a6e558b94ed2 100644
--- a/src/Init/Data/List/Nat/Find.lean
+++ b/src/Init/Data/List/Nat/Find.lean
@@ -9,6 +9,32 @@ import Init.Data.List.Find
 
 namespace List
 
+open Nat
+
+theorem find?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {b : α} :
+    xs.find? p = some b ↔ p b ∧ ∃ i h, xs[i] = b ∧ ∀ j : Nat, (hj : j < i) → !p xs[j] := by
+  rw [find?_eq_some_iff_append]
+  simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]
+  intro w
+  constructor
+  · rintro ⟨as, ⟨bs, rfl⟩, h⟩
+    refine ⟨as.length, ⟨?_, ?_, ?_⟩⟩
+    · simp only [length_append, length_cons]
+      refine Nat.lt_add_of_pos_right (zero_lt_succ bs.length)
+    · rw [getElem_append_right (Nat.le_refl as.length)]
+      simp
+    · intro j h'
+      rw [getElem_append_left h']
+      exact h _ (getElem_mem h')
+  · rintro ⟨i, h, rfl, h'⟩
+    refine ⟨xs.take i, ⟨xs.drop (i+1), ?_⟩, ?_⟩
+    · rw [getElem_cons_drop, take_append_drop]
+    · intro a m
+      rw [mem_take_iff_getElem] at m
+      obtain ⟨j, h, rfl⟩ := m
+      apply h'
+      omega
+
 theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) {i : Nat}
     (h : xs.findIdx? p = some i) : ∃ j, j ≤ i ∧ xs.findIdx? q = some j := by
   simp only [findIdx?_eq_findSome?_enum] at h
diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean
index 3c72fa693959..939ce85d7c20 100644
--- a/src/Init/Data/List/Nat/Range.lean
+++ b/src/Init/Data/List/Nat/Range.lean
@@ -108,7 +108,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
 
 @[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
     (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
-  rw [find?_eq_some]
+  rw [find?_eq_some_iff_append]
   simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_range'_1,
     and_congr_right_iff]
   simp only [range'_eq_append_iff, eq_comm (a := i :: _), range'_eq_cons_iff]
@@ -282,7 +282,7 @@ theorem find?_iota_eq_none {n : Nat} {p : Nat → Bool} :
 
 @[simp] theorem find?_iota_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
     (iota n).find? p = some i ↔ p i ∧ i ∈ iota n ∧ ∀ j, i < j → j ≤ n → !p j := by
-  rw [find?_eq_some]
+  rw [find?_eq_some_iff_append]
   simp only [iota_eq_reverse_range', reverse_eq_append_iff, reverse_cons, append_assoc, cons_append,
     nil_append, Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_reverse, mem_range'_1,
     and_congr_right_iff]