diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean
index d87435c78e..82d5839a3c 100644
--- a/src/Init/Data/Array.lean
+++ b/src/Init/Data/Array.lean
@@ -21,3 +21,4 @@ import Init.Data.Array.Set
 import Init.Data.Array.Monadic
 import Init.Data.Array.FinRange
 import Init.Data.Array.Perm
+import Init.Data.Array.Find
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index d7208a787a..52fb7faecf 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -474,6 +474,10 @@ def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f
     | _      => pure ⟨⟩
   return none
 
+/--
+Note that the universe level is contrained to `Type` here,
+to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
+-/
 @[inline]
 def findM? {α : Type} {m : Type → Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := do
   for a in as do
@@ -585,8 +589,12 @@ def zipWithIndex (arr : Array α) : Array (α × Nat) :=
   arr.mapIdx fun i a => (a, i)
 
 @[inline]
-def find? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
-  Id.run <| as.findM? p
+def find? {α : Type u} (p : α → Bool) (as : Array α) : Option α :=
+  Id.run do
+    for a in as do
+      if p a then
+        return a
+    return none
 
 @[inline]
 def findSome? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 2225e85e58..7aebc66b4b 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -230,7 +230,13 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis
 
 @[simp] theorem find?_toArray (f : α → Bool) (l : List α) :
     l.toArray.find? f = l.find? f := by
-  rw [Array.find?, ← findM?_id, findM?_toArray, Id.run]
+  rw [Array.find?]
+  simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray]
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?]
+    by_cases f a <;> simp_all
 
 theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
     Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index b0318c0f47..245f8ce941 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -354,7 +354,7 @@ theorem containsThenInsert_snd {k : α} : (m.containsThenInsert k).2 = m.insert
   ext HashMap.containsThenInsertIfNew_snd
 
 @[simp]
-theorem length_toList [EquivBEq α] [LawfulHashable α] : 
+theorem length_toList [EquivBEq α] [LawfulHashable α] :
     m.toList.length = m.size :=
   HashMap.length_keys
 
@@ -369,7 +369,7 @@ theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α}:
   HashMap.contains_keys
 
 @[simp]
-theorem mem_toList [LawfulBEq α] [LawfulHashable α]  {k : α}:
+theorem mem_toList [LawfulBEq α] [LawfulHashable α] {k : α} :
     k ∈ m.toList ↔ k ∈ m :=
   HashMap.mem_keys