feat: List.tail lemma (#5316)

leanprover · Sep 12, 2024 · 87fdd78 · 87fdd78
1 parent 8fd6e46
commit 87fdd78
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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 -/