diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 1db5a4acf7..0987c71822 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -3893,7 +3893,7 @@ theorem all_map {xs : Array α} {p : β → Bool} : (xs.map f).all p = xs.all (p
 
 /-- Variant of `all_filter` with a side condition for the `stop` argument. -/
 @[simp] theorem all_filter' {xs : Array α} {p q : α → Bool} (w : stop = (xs.filter p).size) :
-    (xs.filter p).all q 0 stop = xs.all fun a => p a → q a := by
+    (xs.filter p).all q 0 stop = xs.all fun a => !(p a) || q a := by
   subst w
   rcases xs with ⟨xs⟩
   rw [List.filter_toArray]
@@ -3904,7 +3904,7 @@ theorem any_filter {xs : Array α} {p q : α → Bool} :
   simp
 
 theorem all_filter {xs : Array α} {p q : α → Bool} :
-    (xs.filter p).all q 0 = xs.all fun a => p a → q a := by
+    (xs.filter p).all q 0 = xs.all fun a => !(p a) || q a := by
   simp
 
 /-- Variant of `any_filterMap` with a side condition for the `stop` argument. -/
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index a4410addbd..ceac926bad 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -3359,7 +3359,7 @@ theorem all_eq_not_any_not {l : List α} {p : α → Bool} : l.all p = !l.any (!
     split <;> simp_all
 
 @[simp] theorem all_filter {l : List α} {p q : α → Bool} :
-    (filter p l).all q = l.all fun a => p a → q a := by
+    (filter p l).all q = l.all fun a => !(p a) || q a := by
   induction l with
   | nil => rfl
   | cons h t ih =>
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 3ef11c2036..ae0771e734 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -2783,7 +2783,7 @@ theorem any_eq_not_all_not {xs : Vector α n} {p : α → Bool} : xs.any p = !xs
   simp
 
 @[simp] theorem all_filter {xs : Vector α n} {p q : α → Bool} :
-    (xs.filter p).all q = xs.all fun a => p a → q a := by
+    (xs.filter p).all q = xs.all fun a => !(p a) || q a := by
   rcases xs with ⟨xs, rfl⟩
   simp