From 344bd60fa5d7531f760ff537762b7d36a4409a88 Mon Sep 17 00:00:00 2001
From: Bulhwi Cha <chabulhwi@semmalgil.com>
Date: Mon, 18 Mar 2024 16:27:14 +0900
Subject: [PATCH] feat: add lemmas about lists

I need these lemmas to prove `String.splitOn_of_valid`.
---
 Batteries/Data/List/Lemmas.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 6a956f9b1d..0ed5bf978d 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -19,6 +19,11 @@ namespace List
 
 @[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff
 
+/-! ### head and tail -/
+
+theorem head_cons_tail : ∀ l h, @head α l h :: l.tail = l
+  | _::_, _ => rfl
+
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl
@@ -482,6 +487,12 @@ theorem Sublist.erase_diff_erase_sublist {a : α} :
 
 end Diff
 
+/-! ### prefix, suffix, infix -/
+
+theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by
+  intro heq
+  simp [heq, nil_prefix] at h
+
 /-! ### drop -/
 
 theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n)