chore: a missing List lemma in Init

2026-03-17 18:34:06 +00:00 · 2024-02-15 19:17:53 +11:00
1 changed files with 2 additions and 2 deletions
--- 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? -/