diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index b04bb16f4881..4252bd32c1dd 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -663,7 +663,7 @@ def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool
   Id.run <| as.allM p start stop
 
 def contains [BEq α] (as : Array α) (a : α) : Bool :=
-  as.any (· == a)
+  as.any (a == ·)
 
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index e63bba6b253d..377027f08f1a 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -379,6 +379,22 @@ theorem isEmpty_iff_size_eq_zero {l : Array α} : l.isEmpty ↔ l.size = 0 := by
 @[simp] theorem isEmpty_eq_false {l : Array α} : l.isEmpty = false ↔ l ≠ #[] := by
   cases l <;> simp
 
+/-! ### Decidability of bounded quantifiers -/
+
+instance {xs : Array α} {p : α → Prop} [DecidablePred p] :
+    Decidable (∀ x, x ∈ xs → p x) :=
+  decidable_of_iff (∀ (i : Nat) h, p (xs[i]'h)) (by
+    simp only [mem_iff_getElem, forall_exists_index]
+    exact
+      ⟨by rintro w _ i h rfl; exact w i h, fun w i h => w _ i h rfl⟩)
+
+instance {xs : Array α} {p : α → Prop} [DecidablePred p] :
+    Decidable (∃ x, x ∈ xs ∧ p x) :=
+  decidable_of_iff (∃ (i : Nat), ∃ (h : i < xs.size), p (xs[i]'h)) (by
+    simp [mem_iff_getElem]
+    exact
+      ⟨by rintro ⟨i, h, w⟩; exact ⟨_, ⟨i, h, rfl⟩, w⟩, fun ⟨_, ⟨i, h, rfl⟩, w⟩ => ⟨i, h, w⟩⟩)
+
 /-! ### any / all -/
 
 theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
@@ -389,14 +405,15 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
     (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by
   rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]
 
-theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat) (h : stop + 1 ≤ (a :: as).length) :
-    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) = anyM.loop p ⟨as⟩ stop (by simpa using h) start := by
+theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat)
+    (h : stop + 1 ≤ (a :: as).length) :
+    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) =
+      anyM.loop p ⟨as⟩ stop (by simpa using h) start := by
   rw [anyM.loop]
   conv => rhs; rw [anyM.loop]
   split <;> rename_i h'
   · simp only [Nat.add_lt_add_iff_right] at h'
-    rw [dif_pos h']
-    rw [anyM_loop_cons]
+    rw [dif_pos h', anyM_loop_cons]
     simp
   · rw [dif_neg]
     omega
@@ -451,10 +468,15 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
     · rintro ⟨i, hi, ge, _, h⟩
       exact ⟨i, by omega, by omega, by omega, h⟩
 
-theorem any_eq_true {p : α → Bool} {as : Array α} :
-    as.any p ↔ ∃ (i : Nat) (_ : i < as.size), p as[i] := by
+@[simp] theorem any_eq_true {p : α → Bool} {as : Array α} :
+    as.any p = true ↔ ∃ (i : Nat) (_ : i < as.size), p as[i] := by
   simp [any_iff_exists]
 
+@[simp] theorem any_eq_false {p : α → Bool} {as : Array α} :
+    as.any p = false ↔ ∀ (i : Nat) (_ : i < as.size), ¬p as[i] := by
+  rw [Bool.eq_false_iff, Ne, any_eq_true]
+  simp
+
 theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]
   simp only [List.mem_iff_getElem, getElem_toList]
@@ -485,10 +507,15 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
   simp only [any_iff_exists, Bool.not_eq_eq_eq_not, Bool.not_true, not_exists, not_and,
     Bool.not_eq_false, and_imp]
 
-theorem all_eq_true {p : α → Bool} {as : Array α} :
-    as.all p ↔ ∀ (i : Nat) (_ : i < as.size), p as[i] := by
+@[simp] theorem all_eq_true {p : α → Bool} {as : Array α} :
+    as.all p = true ↔ ∀ (i : Nat) (_ : i < as.size), p as[i] := by
   simp [all_iff_forall]
 
+@[simp] theorem all_eq_false {p : α → Bool} {as : Array α} :
+    as.all p = false ↔ ∃ (i : Nat) (_ : i < as.size), ¬p as[i] := by
+  rw [Bool.eq_false_iff, Ne, all_eq_true]
+  simp
+
 theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
   rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]
   simp only [List.mem_iff_getElem, getElem_toList]
@@ -501,6 +528,188 @@ theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
   simp only [← all_toList, List.all_eq_true, mem_def]
 
+theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.anyM p = l.anyM p := by
+  rw [← anyM_toList]
+
+theorem _root_.List.any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
+  rw [any_toList]
+
+theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.allM p = l.allM p := by
+  rw [← allM_toList]
+
+theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
+  rw [all_toList]
+
+/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
+@[simp] theorem _root_.List.anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.anyM p 0 stop = l.anyM p := by
+  subst h
+  rw [← anyM_toList]
+
+/-- Variant of `any_toArray` with a side condition on `stop`. -/
+@[simp] theorem _root_.List.any_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.any p 0 stop = l.any p := by
+  subst h
+  rw [any_toList]
+
+/-- Variant of `allM_toArray` with a side condition on `stop`. -/
+@[simp] theorem _root_.List.allM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.allM p 0 stop = l.allM p := by
+  subst h
+  rw [← allM_toList]
+
+/-- Variant of `all_toArray` with a side condition on `stop`. -/
+@[simp] theorem _root_.List.all_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.all p 0 stop = l.all p := by
+  subst h
+  rw [all_toList]
+
+/-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
+theorem any_eq_true' {p : α → Bool} {as : Array α} :
+    as.any p = true ↔ (∃ x, x ∈ as ∧ p x) := by
+  cases as
+  simp
+
+/-- Variant of `any_eq_false` in terms of membership rather than an array index. -/
+theorem any_eq_false' {p : α → Bool} {as : Array α} :
+    as.any p = false ↔ ∀ x, x ∈ as → ¬p x := by
+  rw [Bool.eq_false_iff, Ne, any_eq_true']
+  simp
+
+/-- Variant of `all_eq_true` in terms of membership rather than an array index. -/
+theorem all_eq_true' {p : α → Bool} {as : Array α} :
+    as.all p = true ↔ (∀ x, x ∈ as → p x) := by
+  cases as
+  simp
+
+/-- Variant of `all_eq_false` in terms of membership rather than an array index. -/
+theorem all_eq_false' {p : α → Bool} {as : Array α} :
+    as.all p = false ↔ ∃ x, x ∈ as ∧ ¬p x := by
+  rw [Bool.eq_false_iff, Ne, all_eq_true']
+  simp
+
+theorem any_eq {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ i : Nat, ∃ h, p (xs[i]'h)) := by
+  by_cases h : xs.any p
+  · simp_all [any_eq_true]
+  · simp_all [any_eq_false]
+
+/-- Variant of `any_eq` in terms of membership rather than an array index. -/
+theorem any_eq' {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ x, x ∈ xs ∧ p x) := by
+  by_cases h : xs.any p
+  · simp_all [any_eq_true', -any_eq_true]
+  · simp only [Bool.not_eq_true] at h
+    simp only [h]
+    simp only [any_eq_false'] at h
+    simpa using h
+
+theorem all_eq {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ i, (_ : i < xs.size) → p xs[i]) := by
+  by_cases h : xs.all p
+  · simp_all [all_eq_true]
+  · simp only [Bool.not_eq_true] at h
+    simp only [h]
+    simp only [all_eq_false] at h
+    simpa using h
+
+/-- Variant of `all_eq` in terms of membership rather than an array index. -/
+theorem all_eq' {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ x, x ∈ xs → p x) := by
+  by_cases h : xs.all p
+  · simp_all [all_eq_true', -all_eq_true]
+  · simp only [Bool.not_eq_true] at h
+    simp only [h]
+    simp only [all_eq_false'] at h
+    simpa using h
+
+theorem decide_exists_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
+    decide (∃ x, x ∈ xs ∧ p x) = xs.any p := by
+  simp [any_eq']
+
+theorem decide_forall_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
+    decide (∀ x, x ∈ xs → p x) = xs.all p := by
+  simp [all_eq']
+
+@[simp] theorem _root_.List.contains_toArray [BEq α] {l : List α} {a : α} :
+    l.toArray.contains a = l.contains a := by
+  simp [Array.contains, List.any_beq]
+
+@[simp] theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
+    Array.elem a l.toArray = List.elem a l := by
+  simp [Array.elem]
+
+theorem any_beq [BEq α] {xs : Array α} {a : α} : (xs.any fun x => a == x) = xs.contains a := by
+  cases xs
+  simp [List.any_beq]
+
+/-- Variant of `any_beq` with `==` reversed. -/
+theorem any_beq' [BEq α] [PartialEquivBEq α] {xs : Array α} :
+    (xs.any fun x => x == a) = xs.contains a := by
+  simp only [BEq.comm, any_beq]
+
+theorem all_bne [BEq α] {xs : Array α} : (xs.all fun x => a != x) = !xs.contains a := by
+  cases xs
+  simp [List.all_bne]
+
+/-- Variant of `all_bne` with `!=` reversed. -/
+theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Array α} :
+    (xs.all fun x => x != a) = !xs.contains a := by
+  simp only [bne_comm, all_bne]
+
+theorem mem_of_elem_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : elem a as = true → a ∈ as := by
+  cases as
+  simp
+
+theorem elem_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : elem a as = true := by
+  cases as
+  simpa using h
+
+instance [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
+  decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
+
+@[simp] theorem elem_eq_contains [BEq α] {a : α} {l : Array α} :
+    elem a l = l.contains a := by
+  simp [elem]
+
+theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
+    elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
+
+theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
+    as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
+
+theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
+    elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
+
+@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
+    as.contains a = decide (a ∈ as) := by rw [← elem_eq_contains, elem_eq_mem]
+
+/-- Variant of `any_push` with a side condition on `stop`. -/
+@[simp] theorem any_push' [BEq α] {as : Array α} {a : α} {p : α → Bool} (h : stop = as.size + 1) :
+    (as.push a).any p 0 stop = (as.any p || p a) := by
+  cases as
+  rw [List.push_toArray]
+  simp [h]
+
+theorem any_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
+    (as.push a).any p = (as.any p || p a) :=
+  any_push' (by simp)
+
+/-- Variant of `all_push` with a side condition on `stop`. -/
+@[simp] theorem all_push' [BEq α] {as : Array α} {a : α} {p : α → Bool} (h : stop = as.size + 1) :
+    (as.push a).all p 0 stop = (as.all p && p a) := by
+  cases as
+  rw [List.push_toArray]
+  simp [h]
+
+theorem all_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
+    (as.push a).all p = (as.all p && p a) :=
+  all_push' (by simp)
+
+@[simp] theorem contains_push [BEq α] {l : Array α} {a : α} {b : α} :
+    (l.push a).contains b = (l.contains b || b == a) := by
+  simp [contains]
+
 theorem singleton_inj : #[a] = #[b] ↔ a = b := by
   simp
 
@@ -1797,46 +2006,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   · simp
   · simp_all [List.set_eq_of_length_le]
 
-theorem anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
-    l.toArray.anyM p = l.anyM p := by
-  rw [← anyM_toList]
-
-theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
-  rw [any_toList]
-
-theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
-    l.toArray.allM p = l.allM p := by
-  rw [← allM_toList]
-
-theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
-  rw [all_toList]
-
-/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
-@[simp] theorem anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
-    (h : stop = l.toArray.size) :
-    l.toArray.anyM p 0 stop = l.anyM p := by
-  subst h
-  rw [← anyM_toList]
-
-/-- Variant of `any_toArray` with a side condition on `stop`. -/
-@[simp] theorem any_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
-    l.toArray.any p 0 stop = l.any p := by
-  subst h
-  rw [any_toList]
-
-/-- Variant of `allM_toArray` with a side condition on `stop`. -/
-@[simp] theorem allM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
-    (h : stop = l.toArray.size) :
-    l.toArray.allM p 0 stop = l.allM p := by
-  subst h
-  rw [← allM_toList]
-
-/-- Variant of `all_toArray` with a side condition on `stop`. -/
-@[simp] theorem all_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
-    l.toArray.all p 0 stop = l.all p := by
-  subst h
-  rw [all_toList]
-
 @[simp] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
     l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
   apply ext'
diff --git a/src/Init/Data/BEq.lean b/src/Init/Data/BEq.lean
index 786744b2d951..369e586ee7f5 100644
--- a/src/Init/Data/BEq.lean
+++ b/src/Init/Data/BEq.lean
@@ -40,6 +40,9 @@ theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
 theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
 
+theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a) := by
+  rw [bne, BEq.comm, bne]
+
 theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = false → (b == a) = false :=
   BEq.comm (α := α) ▸ id
 
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 1626fa78c47f..f223857146e8 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -666,10 +666,14 @@ def isEmpty : List α → Bool
 /-! ### elem -/
 
 /--
-`O(|l|)`. `elem a l` or `l.contains a` is true if there is an element in `l` equal to `a`.
+`O(|l|)`.
+`l.contains a` or `elem a l` is true if there is an element in `l` equal (according to `==`) to `a`.
 
-* `elem 3 [1, 4, 2, 3, 3, 7] = true`
-* `elem 5 [1, 4, 2, 3, 3, 7] = false`
+* `[1, 4, 2, 3, 3, 7].contains 3 = true`
+* `[1, 4, 2, 3, 3, 7].contains 5 = false`
+
+The preferred simp normal form is `l.contains a`, and when `LawfulBEq α` is available,
+`l.contains a = true ↔ a ∈ l` and `l.contains a = false ↔ a ∉ l`.
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 2b94abd89a45..ea9b72590e45 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -451,6 +451,10 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
         simp only [getElem_cons_succ]
         exact getElem_mem (lt_of_succ_lt_succ h)
 
+@[simp] theorem elem_eq_contains [BEq α] {a : α} {l : List α} :
+    elem a l = l.contains a := by
+  simp [contains]
+
 @[simp] theorem decide_mem_cons [BEq α] [LawfulBEq α] {l : List α} :
     decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
   cases h : y == a <;> simp_all
@@ -458,9 +462,20 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
     elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
 
-@[simp] theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
+theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
+    as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
+
+theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
     elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
 
+@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
+    as.contains a = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
+
+@[simp] theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
+    (a :: l).contains b = (b == a || l.contains b) := by
+  simp only [contains, elem_cons]
+  split <;> simp_all
+
 /-! ### `isEmpty` -/
 
 theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
@@ -505,17 +520,21 @@ theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] :
 @[simp] theorem all_eq_false {l : List α} : l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x := by
   simp [all_eq]
 
-theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by
-  simp
+theorem any_beq [BEq α] {l : List α} {a : α} : (l.any fun x => a == x) = l.contains a := by
+  induction l <;> simp_all [contains_cons]
 
-theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by
-  simp
+/-- Variant of `any_beq` with `==` reversed. -/
+theorem any_beq' [BEq α] [PartialEquivBEq α] {l : List α} :
+    (l.any fun x => x == a) = l.contains a := by
+  simp only [BEq.comm, any_beq]
 
-theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by
-  induction l <;> simp_all
+theorem all_bne [BEq α] {l : List α} : (l.all fun x => a != x) = !l.contains a := by
+  induction l <;> simp_all [bne]
 
-theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by
-  induction l <;> simp_all [eq_comm (a := a)]
+/-- Variant of `all_bne` with `!=` reversed. -/
+theorem all_bne' [BEq α] [PartialEquivBEq α] {l : List α} :
+    (l.all fun x => x != a) = !l.contains a := by
+  simp only [bne_comm, all_bne]
 
 /-! ### set -/
 
@@ -2828,11 +2847,6 @@ theorem leftpad_suffix (n : Nat) (a : α) (l : List α) : l <:+ (leftpad n a l)
 
 theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by simp
 
-@[simp] theorem contains_cons [BEq α] :
-    (a :: as : List α).contains x = (x == a || as.contains x) := by
-  simp only [contains, elem]
-  split <;> simp_all
-
 theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by
   induction l with simp | cons b l => cases b == a <;> simp [*]
 
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index b0530b5a6a86..7509ebe06a7a 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -1046,6 +1046,25 @@ instance decidableExistsLE [DecidablePred p] : DecidablePred fun n => ∃ m : Na
   fun n => decidable_of_iff (∃ m, m < n + 1 ∧ p m)
     (exists_congr fun _ => and_congr_left' Nat.lt_succ_iff)
 
+/-- Dependent version of `decidableExistsLT`. -/
+instance decidableExistsLT' {p : (m : Nat) → m < k → Prop} [I : ∀ m h, Decidable (p m h)] :
+    Decidable (∃ m : Nat, ∃ h : m < k, p m h) :=
+  match k, p, I with
+  | 0, _, _ => isFalse (by simp)
+  | (k + 1), p, I => @decidable_of_iff _ ((∃ m, ∃ h : m < k, p m (by omega)) ∨ p k (by omega))
+      ⟨by rintro (⟨m, h, w⟩ | w); exact ⟨m, by omega, w⟩; exact ⟨k, by omega, w⟩,
+        fun ⟨m, h, w⟩ => if h' : m < k then .inl ⟨m, h', w⟩ else
+          by obtain rfl := (by omega : m = k); exact .inr w⟩
+      (@instDecidableOr _ _
+        (decidableExistsLT' (p := fun m h => p m (by omega)) (I := fun m h => I m (by omega)))
+        inferInstance)
+
+/-- Dependent version of `decidableExistsLE`. -/
+instance decidableExistsLE' {p : (m : Nat) → m ≤ k → Prop} [I : ∀ m h, Decidable (p m h)] :
+    Decidable (∃ m : Nat, ∃ h : m ≤ k, p m h) :=
+  decidable_of_iff (∃ m, ∃ h : m < k + 1, p m (by omega)) (exists_congr fun _ =>
+    ⟨fun ⟨h, w⟩ => ⟨le_of_lt_succ h, w⟩, fun ⟨h, w⟩ => ⟨lt_add_one_of_le h, w⟩⟩)
+
 /-! ### Results about `List.sum` specialized to `Nat` -/
 
 protected theorem sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by
diff --git a/tests/lean/run/wfOverapplicationIssue.lean b/tests/lean/run/wfOverapplicationIssue.lean
index cacefc89be04..55dda3ae009c 100644
--- a/tests/lean/run/wfOverapplicationIssue.lean
+++ b/tests/lean/run/wfOverapplicationIssue.lean
@@ -1,6 +1,6 @@
 theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h : as.contains a) : sizeOf a < sizeOf as := by
   simp [Membership.mem, contains, any, Id.run, BEq.beq, anyM] at h
-  let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (b = a)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
+  let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (a = b)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
     unfold anyM.loop
     intro h
     split at h