From 87fdd7809fa4d2fe33283ced4f4aa9c12763e9bd Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Thu, 12 Sep 2024 11:09:57 +1000
Subject: [PATCH] feat: List.tail lemma (#5316)

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

diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index bb14e4f6de3f..b948d76a500a 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -1052,6 +1052,9 @@ theorem tail_eq_tailD (l) : @tail α l = tailD l [] := by cases l <;> rfl
 
 theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_tailD]
 
+theorem mem_of_mem_tail {a : α} {l : List α} (h : a ∈ tail l) : a ∈ l := by
+  induction l <;> simp_all
+
 /-! ## Basic operations -/
 
 /-! ### map -/