From 813e86c555ec6a97b46e3d42fd0b3826d5fe3019 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 8 Jun 2025 01:27:00 +0100
Subject: [PATCH 1/4] feat: strengthen finIdxOf? lemmas

This PR makes the LHS of `isSome_finIdxOf?` and `isNone_finIdxOf?` more general.
---
 src/Init/Data/List/Find.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index 56cdf2ad7f5b..f05f4d077600 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -1098,16 +1098,17 @@ theorem finIdxOf?_cons [BEq α] {a : α} {xs : List α} :
 
 @[simp]
 theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
-    (l.finIdxOf? a).isSome ↔ a ∈ l := by
+    (l.finIdxOf? a).isSome = l.contains a := by
   induction l with
   | nil => simp
   | cons x xs ih =>
     simp only [finIdxOf?_cons]
     split <;> simp_all [@eq_comm _ x a]
 
-theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
-    (l.finIdxOf? a).isNone = ¬ a ∈ l := by
-  simp
+@[simp]
+theorem isNone_finIdxOf?' [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+    (l.finIdxOf? a).isNone = !l.contains a := by
+  rw [← isSome_finIdxOf?, Option.not_isSome]
 
 /-! ### idxOf?
 

From a90dd4ae3d7223abf0500d5a23337c27b7c77136 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 8 Jun 2025 01:31:59 +0100
Subject: [PATCH 2/4] PartialEquivBEq

---
 src/Init/Data/List/Find.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index f05f4d077600..bf352355bada 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -1097,16 +1097,16 @@ theorem finIdxOf?_cons [BEq α] {a : α} {xs : List α} :
   simp only [finIdxOf?, findFinIdx?_eq_some_iff, beq_iff_eq]
 
 @[simp]
-theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+theorem isSome_finIdxOf? [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
     (l.finIdxOf? a).isSome = l.contains a := by
   induction l with
   | nil => simp
   | cons x xs ih =>
     simp only [finIdxOf?_cons]
-    split <;> simp_all [@eq_comm _ x a]
+    split <;> simp_all [BEq.comm]
 
 @[simp]
-theorem isNone_finIdxOf?' [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+theorem isNone_finIdxOf?' [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
     (l.finIdxOf? a).isNone = !l.contains a := by
   rw [← isSome_finIdxOf?, Option.not_isSome]
 

From 9365fd4644fcd7de1273c490c9c8be565d79c2e1 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 8 Jun 2025 01:34:39 +0100
Subject: [PATCH 3/4] Update Find.lean

---
 src/Init/Data/Array/Find.lean | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean
index 881329c9702a..d8e709185244 100644
--- a/src/Init/Data/Array/Find.lean
+++ b/src/Init/Data/Array/Find.lean
@@ -743,13 +743,15 @@ theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by sim
   simp [List.finIdxOf?_eq_some_iff]
 
 @[simp]
-theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
-    (xs.finIdxOf? a).isSome ↔ a ∈ xs := by
+theorem isSome_finIdxOf? [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} :
+    (xs.finIdxOf? a).isSome = xs.contains a := by
   rcases xs with ⟨xs⟩
   simp [Array.size]
 
-theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
-    (xs.finIdxOf? a).isNone = ¬ a ∈ xs := by
-  simp
+@[simp]
+theorem isNone_finIdxOf? [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} :
+    (xs.finIdxOf? a).isNone = !xs.contains a := by
+  rcases xs with ⟨xs⟩
+  simp [Array.size]
 
 end Array

From 67e91aeffd9b2a0fbadb5a79939a9aeb01710763 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 11 Jun 2025 07:37:56 +0100
Subject: [PATCH 4/4] Update src/Init/Data/List/Find.lean

---
 src/Init/Data/List/Find.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index bf352355bada..227dfcbeee41 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -1106,7 +1106,7 @@ theorem isSome_finIdxOf? [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
     split <;> simp_all [BEq.comm]
 
 @[simp]
-theorem isNone_finIdxOf?' [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
+theorem isNone_finIdxOf? [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
     (l.finIdxOf? a).isNone = !l.contains a := by
   rw [← isSome_finIdxOf?, Option.not_isSome]