diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index faee86f313..a964caee15 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -923,12 +923,12 @@ theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
   | a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
 
 theorem filter_congr {p q : α → Bool} :
-    ∀ {l : List α}, (∀ x ∈ l, p x ↔ q x) → filter p l = filter q l
+    ∀ {l : List α}, (∀ x ∈ l, p x = q x) → filter p l = filter q l
   | [], _ => rfl
   | a :: l, h => by
     rw [forall_mem_cons] at h; by_cases pa : p a
-    · simp [pa, h.1.1 pa, filter_congr h.2]
-    · simp [pa, mt h.1.2 pa, filter_congr h.2]
+    · simp [pa, h.1 ▸ pa, filter_congr h.2]
+    · simp [pa, h.1 ▸ pa, filter_congr h.2]
 
 @[deprecated filter_congr (since := "2024-06-20")] abbrev filter_congr' := @filter_congr