refactor: move theorems about lists from mathlib

`List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from `Mathlib.Data.List.Basic`. I removed the `simp` priority and `nolint` attribute from `modifyHead_modifyHead` because we don't need them anymore. We need these theorems to prove `String.splitOn_of_valid`. See #756. Co-authored-by: Kim Morrison <[email protected]>
leanprover-community · Sep 3, 2024 · 6fb4f5e · 6fb4f5e
1 parent 9c6c2d6
commit 6fb4f5e
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
@@ -17,6 +17,10 @@ open Nat
 @[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [Array.mem_def]
 
+/-! ### isEmpty -/
+
+theorem isEmpty_iff_eq_nil {l : List α} : l.isEmpty ↔ l = [] := by cases l <;> simp [isEmpty]
+
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl
@@ -34,6 +38,11 @@ theorem get?_inj
   apply getElem?_inj h₀ h₁
   simp_all
 
+/-! ### modifyHead -/
+
+@[simp] theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
+    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead]
+
 /-! ### modifyNth -/
 
 @[simp] theorem modifyNth_nil (f : α → α) (n) : [].modifyNth f n = [] := by cases n <;> rfl