refactor: move theorem about lists to batteries (#12540)

`List.modifyHead_modifyHead` is from `Mathlib.Data.List.Basic`. I need it to prove `String.splitOn_of_valid`. See leanprover-community/batteries#743. Corresponding Batteries PR: leanprover-community/batteries#756 Co-authored-by: Kim Morrison <[email protected]>
leanprover-community · Oct 14, 2024 · 8142938 · 8142938
1 parent 5d2ccbb
commit 8142938
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 14 deletions.
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -287,10 +287,6 @@ theorem map_reverseAux (f : α → β) (l₁ l₂ : List α) :
     map f (reverseAux l₁ l₂) = reverseAux (map f l₁) (map f l₂) := by
   simp only [reverseAux_eq, map_append, map_reverse]
 
-/-! ### empty -/
-
-@[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff
-
 /-! ### getLast -/
 
 attribute [simp] getLast_cons
@@ -509,9 +505,6 @@ theorem get_cons {l : List α} {a : α} {n} (hl) :
       l.get ⟨n - 1, by contrapose! hl; rw [length_cons]; omega⟩ :=
   getElem_cons hl
 
-theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
-    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp
-
 /-! ### Induction from the right -/
 
 /-- Induction principle from the right for lists: if a property holds for the empty list, and

diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean
@@ -131,12 +131,6 @@ lemma subperm_iff : l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l := by
   · rintro (rfl | rfl)
     exacts [nil_subperm, Subperm.refl _]
 
-attribute [simp] nil_subperm
-
-@[simp]
-theorem subperm_nil : List.Subperm l [] ↔ l = [] :=
-  ⟨fun h ↦ length_eq_zero.1 <| Nat.le_zero.1 h.length_le, by rintro rfl; rfl⟩
-
 lemma subperm_cons_self : l <+~ a :: l := ⟨l, Perm.refl _, sublist_cons_self _ _⟩
 
 lemma count_eq_count_filter_add [DecidableEq α] (P : α → Prop) [DecidablePred P]

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
+   "rev": "9efd9c267ad7a71c5e3a83e8fbbd446fe61ef119",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",