chore: remove >6 month deprecations (#945)

Batteries.lean

@@ -16,21 +16,17 @@ import Batteries.Data.Array
 import Batteries.Data.AssocList
 import Batteries.Data.BinaryHeap
 import Batteries.Data.BinomialHeap
-import Batteries.Data.BitVec
-import Batteries.Data.Bool
 import Batteries.Data.ByteArray
 import Batteries.Data.ByteSubarray
 import Batteries.Data.Char
 import Batteries.Data.DList
 import Batteries.Data.Fin
 import Batteries.Data.FloatArray
 import Batteries.Data.HashMap
-import Batteries.Data.Int
 import Batteries.Data.LazyList
 import Batteries.Data.List
 import Batteries.Data.MLList
 import Batteries.Data.Nat
-import Batteries.Data.Option
 import Batteries.Data.PairingHeap
 import Batteries.Data.RBMap
 import Batteries.Data.Range

Batteries/Data/List/Basic.lean

@@ -706,23 +706,6 @@ Defined as `pwFilter (≠)`.
     eraseDup [1, 0, 2, 2, 1] = [0, 2, 1] -/
 @[inline] def eraseDup [BEq α] : List α → List α := pwFilter (· != ·)
 
-/--
-`ilast' x xs` returns the last element of `xs` if `xs` is non-empty; it returns `x` otherwise.
-Use `List.getLastD` instead.
--/
-@[simp, deprecated getLastD (since := "2024-01-09")] def ilast' {α} : α → List α → α
-  | a, [] => a
-  | _, b :: l => ilast' b l
-
-/--
-`last' xs` returns the last element of `xs` if `xs` is non-empty; it returns `none` otherwise.
-Use `List.getLast?` instead
--/
-@[simp, deprecated getLast? (since := "2024-01-09")] def last' {α} : List α → Option α
-  | [] => none
-  | [a] => some a
-  | _ :: l => last' l
-
 /--
 `rotate l n` rotates the elements of `l` to the left by `n`
 ```

Batteries/Data/List/Count.lean

@@ -29,11 +29,3 @@ variable [DecidableEq α]
 theorem count_singleton' (a b : α) : count a [b] = if b = a then 1 else 0 := by simp [count_cons]
 
 theorem count_concat (a : α) (l : List α) : count a (concat l a) = succ (count a l) := by simp
-
-@[deprecated filter_eq (since := "2023-12-14")]
-theorem filter_eq' (l : List α) (a : α) : l.filter (a = ·) = replicate (count a l) a := by
-  simpa only [eq_comm] using filter_eq l a
-
-@[deprecated filter_beq (since := "2023-12-14")]
-theorem filter_beq' (l : List α) (a : α) : l.filter (a == ·) = replicate (count a l) a := by
-  simpa only [eq_comm (b := a)] using filter_eq l a

Batteries/Data/List/Pairwise.lean

@@ -29,18 +29,6 @@ namespace List
 
 /-! ### Pairwise -/
 
-@[deprecated pairwise_iff_forall_sublist (since := "2023-09-18")]
-theorem pairwise_of_reflexive_on_dupl_of_forall_ne [DecidableEq α] {l : List α} {r : α → α → Prop}
-    (hr : ∀ a, 1 < count a l → r a a) (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) : l.Pairwise r := by
-  apply pairwise_iff_forall_sublist.mpr
-  intro a b hab
-  if heq : a = b then
-    cases heq; apply hr
-    rwa [show [a,a] = replicate 2 a from rfl, ← le_count_iff_replicate_sublist] at hab
-  else
-    apply h <;> try (apply hab.subset; simp)
-    exact heq
-
 theorem pairwise_iff_get : Pairwise R l ↔ ∀ (i j) (_hij : i < j), R (get l i) (get l j) := by
   rw [pairwise_iff_getElem]
   constructor <;> intro h

Batteries/Data/Nat/Lemmas.lean

@@ -149,24 +149,6 @@ protected def sum_trichotomy (a b : Nat) : a < b ⊕' a = b ⊕' b < a :=
   | .eq => .inr (.inl (Nat.compare_eq_eq.1 h))
   | .gt => .inr (.inr (Nat.compare_eq_gt.1 h))
 
-/-! ## add -/
-
-@[deprecated (since := "2023-11-25")] alias succ_add_eq_succ_add := Nat.succ_add_eq_add_succ
-
-/-! ## sub -/
-
-@[deprecated (since := "2023-11-25")]
-protected alias le_of_le_of_sub_le_sub_right := Nat.le_of_sub_le_sub_right
-
-@[deprecated (since := "2023-11-25")]
-protected alias le_of_le_of_sub_le_sub_left := Nat.le_of_sub_le_sub_left
-
-/-! ### mul -/
-
-@[deprecated (since := "2024-01-11")] protected alias mul_lt_mul := Nat.mul_lt_mul_of_lt_of_le'
-
-@[deprecated (since := "2024-01-11")] protected alias mul_lt_mul' := Nat.mul_lt_mul_of_le_of_lt
-
 /-! ### div/mod -/
 
 -- TODO mod_core_congr, mod_def
@@ -179,6 +161,3 @@ protected alias le_of_le_of_sub_le_sub_left := Nat.le_of_sub_le_sub_left
 
 @[simp] theorem sum_append : Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂ := by
   induction l₁ <;> simp [*, Nat.add_assoc]
-
-@[deprecated (since := "2024-03-05")] protected alias lt_connex := Nat.lt_or_gt_of_ne
-@[deprecated (since := "2024-02-09")] alias pow_two_pos := Nat.two_pow_pos

scripts/check_imports.lean

@@ -34,7 +34,7 @@ def warn (fixable : Bool) (msg : String) : LogIO Unit := do
 -- | Predicate indicates if warnings are present and if they fixable.
 def getWarningInfo : LogIO (Bool × Bool) :=  get
 
-def createModuleHashmap (env : Environment) : HashMap Name ModuleData := Id.run do
+def createModuleHashmap (env : Environment) : Std.HashMap Name ModuleData := Id.run do
   let mut nameMap := {}
   for i in [0:env.header.moduleNames.size] do
     let nm := env.header.moduleNames[i]!
@@ -80,11 +80,11 @@ def checkMissingImports (modName : Name) (modData : ModuleData) (reqImports : Ar
 
 /-- Check directory entry in `Batteries/Data/` -/
 def checkBatteriesDataDir
-    (modMap : HashMap Name ModuleData)
+    (modMap : Std.HashMap Name ModuleData)
     (entry : IO.FS.DirEntry) (autofix : Bool := false) : LogIO Unit := do
   let moduleName := `Batteries.Data ++ .mkSimple entry.fileName
   let requiredImports ← addModulesIn (recurse := true) #[] (root := moduleName) entry.path
-  let .some module := modMap.find? moduleName
+  let .some module := modMap[moduleName]?
     | warn true s!"Could not find {moduleName}; Not imported into Batteries."
       let path := modulePath moduleName
       -- We refuse to generate imported modules whose path doesn't exist.
@@ -134,7 +134,7 @@ def checkBatteriesDataImports : MetaM Unit := do
       if ← entry.path.isDir then
         checkBatteriesDataDir (autofix := autofix) modMap entry
     let batteriesImports ← expectedBatteriesImports
-    let .some batteriesMod := modMap.find? `Batteries
+    let .some batteriesMod := modMap[`Batteries]?
         | warn false "Missing Batteries module!; Run `lake build`."
     let warned ← checkMissingImports `Batteries batteriesMod batteriesImports
     if autofix && warned then