From b88cdf6a3e0779342918bb6aa16c1575a190e54b Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 11 Sep 2024 16:13:24 +1000
Subject: [PATCH] chore: Array.not_mem_empty (#5304)

---
 src/Init/Data/Array/Lemmas.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index b3effb086765..89b3716d3d35 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -147,6 +147,9 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
 theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
+@[simp] theorem not_mem_empty (a : α) : ¬(a ∈ #[]) := by
+  simp [mem_def]
+
 /-! # get -/
 
 @[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl