From ae524d465fac731391e2fb1cf4490338dc213f83 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 15 Feb 2024 19:55:48 +1100
Subject: [PATCH] chore: a missing List lemma in Init (#3344)

---
 src/Init/Data/List/Lemmas.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index d348f5a32d..767baa086a 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -418,8 +418,8 @@ theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
     · exact or_congr_left (and_iff_left_of_imp fun | rfl => h).symm
     · exact (or_iff_right fun ⟨rfl, h'⟩ => h h').symm
 
--- theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a, a ∈ l → ¬p a := by
---   simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]
+theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a, a ∈ l → ¬p a := by
+  simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]
 
 /-! ### findSome? -/