From 46fed98b5cac2b1ea64e363b420c382ed1af0d85 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 10 Sep 2024 16:50:25 +1000
Subject: [PATCH] chore: remove >6 month deprecations (#945)

---
 Batteries.lean                    |  4 --
 Batteries/Data/BitVec.lean        |  1 -
 Batteries/Data/BitVec/Lemmas.lean | 16 ------
 Batteries/Data/Bool.lean          | 19 -------
 Batteries/Data/Int.lean           |  3 --
 Batteries/Data/Int/DivMod.lean    | 84 -------------------------------
 Batteries/Data/Int/Lemmas.lean    |  6 ---
 Batteries/Data/Int/Order.lean     | 10 ----
 Batteries/Data/List/Basic.lean    | 17 -------
 Batteries/Data/List/Count.lean    |  8 ---
 Batteries/Data/List/Pairwise.lean | 12 -----
 Batteries/Data/Nat/Lemmas.lean    | 21 --------
 Batteries/Data/Option.lean        |  1 -
 Batteries/Data/Option/Lemmas.lean | 13 -----
 scripts/check_imports.lean        |  8 +--
 15 files changed, 4 insertions(+), 219 deletions(-)
 delete mode 100644 Batteries/Data/BitVec.lean
 delete mode 100644 Batteries/Data/BitVec/Lemmas.lean
 delete mode 100644 Batteries/Data/Bool.lean
 delete mode 100644 Batteries/Data/Int.lean
 delete mode 100644 Batteries/Data/Int/DivMod.lean
 delete mode 100644 Batteries/Data/Int/Lemmas.lean
 delete mode 100644 Batteries/Data/Int/Order.lean
 delete mode 100644 Batteries/Data/Option.lean
 delete mode 100644 Batteries/Data/Option/Lemmas.lean

diff --git a/Batteries.lean b/Batteries.lean
index 37d88fa3fb..3bd1f4ef79 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -16,8 +16,6 @@ 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
@@ -25,12 +23,10 @@ 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
diff --git a/Batteries/Data/BitVec.lean b/Batteries/Data/BitVec.lean
deleted file mode 100644
index ff4358f07d..0000000000
--- a/Batteries/Data/BitVec.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Batteries.Data.BitVec.Lemmas
diff --git a/Batteries/Data/BitVec/Lemmas.lean b/Batteries/Data/BitVec/Lemmas.lean
deleted file mode 100644
index 2bcd3ce4aa..0000000000
--- a/Batteries/Data/BitVec/Lemmas.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-/-
-Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joe Hendrix
--/
-import Batteries.Tactic.Alias
-
-namespace BitVec
-
-@[deprecated (since := "2024-02-07")] alias zero_is_unique := eq_nil
-
-/-! ### sub/neg -/
-
-@[deprecated (since := "2024-02-07")] alias sub_toNat := toNat_sub
-
-@[deprecated (since := "2024-02-07")] alias neg_toNat := toNat_neg
diff --git a/Batteries/Data/Bool.lean b/Batteries/Data/Bool.lean
deleted file mode 100644
index b6c0c9b4e7..0000000000
--- a/Batteries/Data/Bool.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2023 F. G. Dorais. No rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: F. G. Dorais
--/
-
-import Batteries.Tactic.Alias
-
-namespace Bool
-
-/-! ### injectivity lemmas -/
-
-@[deprecated (since := "2023-10-27")] alias not_inj' := not_inj_iff
-
-@[deprecated (since := "2023-10-27")] alias and_or_inj_right' := and_or_inj_right_iff
-
-@[deprecated (since := "2023-10-27")] alias and_or_inj_left' := and_or_inj_left_iff
-
-end Bool
diff --git a/Batteries/Data/Int.lean b/Batteries/Data/Int.lean
deleted file mode 100644
index 29b6c2e4a9..0000000000
--- a/Batteries/Data/Int.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Batteries.Data.Int.DivMod
-import Batteries.Data.Int.Lemmas
-import Batteries.Data.Int.Order
diff --git a/Batteries/Data/Int/DivMod.lean b/Batteries/Data/Int/DivMod.lean
deleted file mode 100644
index 7558c98a3d..0000000000
--- a/Batteries/Data/Int/DivMod.lean
+++ /dev/null
@@ -1,84 +0,0 @@
-/-
-Copyright (c) 2016 Jeremy Avigad. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad, Mario Carneiro
--/
-import Batteries.Data.Int.Order
-
-/-!
-# Lemmas about integer division
--/
-
-
-open Nat
-
-namespace Int
-
-/-!
-### The following lemmas have been commented out here for a while, and need restoration.
--/
-
-/-
-theorem eq_mul_ediv_of_mul_eq_mul_of_dvd_left {a b c d : Int}
-    (hb : b ≠ 0) (hbc : b ∣ c) (h : b * a = c * d) : a = c / b * d := by
-  rcases hbc with ⟨k, hk⟩
-  subst hk
-  rw [Int.mul_ediv_cancel_left _ hb]
-  rw [Int.mul_assoc] at h
-  apply mul_left_cancel₀ hb h
-
-/-- If an integer with larger absolute value divides an integer, it is
-zero. -/
-theorem eq_zero_of_dvd_ofNatAbs_lt_natAbs {a b : Int} (w : a ∣ b) (h : natAbs b < natAbs a) :
-    b = 0 := by
-  rw [← natAbs_dvd, ← dvd_natAbs, ofNat_dvd] at w
-  rw [← natAbs_eq_zero]
-  exact eq_zero_of_dvd_of_lt w h
-
-theorem eq_zero_of_dvd_of_nonneg_of_lt {a b : Int} (w₁ : 0 ≤ a) (w₂ : a < b) (h : b ∣ a) : a = 0 :=
-  eq_zero_of_dvd_ofNatAbs_lt_natAbs h (natAbs_lt_natAbs_of_nonneg_of_lt w₁ w₂)
-
-/-- If two integers are congruent to a sufficiently large modulus,
-they are equal. -/
-theorem eq_of_mod_eq_ofNatAbs_sub_lt_natAbs {a b c : Int}
-    (h1 : a % b = c) (h2 : natAbs (a - c) < natAbs b) : a = c :=
-  Int.eq_of_sub_eq_zero (eq_zero_of_dvd_ofNatAbs_lt_natAbs (dvd_sub_of_emod_eq h1) h2)
-
-theorem ofNat_add_negSucc_of_lt {m n : Nat} (h : m < n.succ) : ofNat m + -[n+1] = -[n+1 - m] := by
-  change subNatNat _ _ = _
-  have h' : n.succ - m = (n - m).succ
-  apply succ_sub
-  apply le_of_lt_succ h
-  simp [*, subNatNat]
-
-theorem ofNat_add_negSucc_of_ge {m n : Nat} (h : n.succ ≤ m) :
-    ofNat m + -[n+1] = ofNat (m - n.succ) := by
-  change subNatNat _ _ = _
-  have h' : n.succ - m = 0
-  apply tsub_eq_zero_iff_le.mpr h
-  simp [*, subNatNat]
-
-@[simp]
-theorem neg_add_neg (m n : Nat) : -[m+1] + -[n+1] = -[Nat+1.succ (m + n)] :=
-  rfl
-
-theorem natAbs_le_of_dvd_ne_zero {s t : Int} (hst : s ∣ t) (ht : t ≠ 0) : natAbs s ≤ natAbs t :=
-  not_lt.mp (mt (eq_zero_of_dvd_ofNatAbs_lt_natAbs hst) ht)
-
-theorem natAbs_eq_of_dvd_dvd {s t : Int} (hst : s ∣ t) (hts : t ∣ s) : natAbs s = natAbs t :=
-  Nat.dvd_antisymm (natAbs_dvd_iff_dvd.mpr hst) (natAbs_dvd_iff_dvd.mpr hts)
-
-theorem div_dvd_of_dvd {s t : Int} (hst : s ∣ t) : t / s ∣ t := by
-  rcases eq_or_ne s 0 with (rfl | hs)
-  · simpa using hst
-  rcases hst with ⟨c, hc⟩
-  simp [hc, Int.mul_div_cancel_left _ hs]
-
-theorem dvd_div_of_mul_dvd {a b c : Int} (h : a * b ∣ c) : b ∣ c / a := by
-  rcases eq_or_ne a 0 with (rfl | ha)
-  · simp only [Int.div_zero, dvd_zero]
-
-  rcases h with ⟨d, rfl⟩
-  refine' ⟨d, _⟩
-  rw [mul_assoc, Int.mul_div_cancel_left _ ha]
--/
diff --git a/Batteries/Data/Int/Lemmas.lean b/Batteries/Data/Int/Lemmas.lean
deleted file mode 100644
index 3ce6c74c04..0000000000
--- a/Batteries/Data/Int/Lemmas.lean
+++ /dev/null
@@ -1,6 +0,0 @@
--- This is a backwards compatibility shim,
--- after `Batteries.Data.Int.Lemmas` was split into smaller files.
--- Hopefully it can later be removed.
-
-import Batteries.Data.Int.Order
-import Batteries.Data.Int.DivMod
diff --git a/Batteries/Data/Int/Order.lean b/Batteries/Data/Int/Order.lean
deleted file mode 100644
index daab75c612..0000000000
--- a/Batteries/Data/Int/Order.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-/-
-Copyright (c) 2016 Jeremy Avigad. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
--/
-import Batteries.Tactic.Alias
-
-namespace Int
-
-@[deprecated (since := "2024-01-24")] alias ofNat_natAbs_eq_of_nonneg := natAbs_of_nonneg
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index a44f430c8d..963920017c 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/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`
 ```
diff --git a/Batteries/Data/List/Count.lean b/Batteries/Data/List/Count.lean
index 036a76b4b8..151169f74b 100644
--- a/Batteries/Data/List/Count.lean
+++ b/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
diff --git a/Batteries/Data/List/Pairwise.lean b/Batteries/Data/List/Pairwise.lean
index 9df947bf4c..de13a5e292 100644
--- a/Batteries/Data/List/Pairwise.lean
+++ b/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
diff --git a/Batteries/Data/Nat/Lemmas.lean b/Batteries/Data/Nat/Lemmas.lean
index 3492037135..7fa93705f7 100644
--- a/Batteries/Data/Nat/Lemmas.lean
+++ b/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
diff --git a/Batteries/Data/Option.lean b/Batteries/Data/Option.lean
deleted file mode 100644
index e99c38ee11..0000000000
--- a/Batteries/Data/Option.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Batteries.Data.Option.Lemmas
diff --git a/Batteries/Data/Option/Lemmas.lean b/Batteries/Data/Option/Lemmas.lean
deleted file mode 100644
index 05a38b25a7..0000000000
--- a/Batteries/Data/Option/Lemmas.lean
+++ /dev/null
@@ -1,13 +0,0 @@
-/-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
--/
-import Batteries.Tactic.Alias
-
-namespace Option
-
-@[deprecated (since := "2024-03-05")] alias to_list_some := toList_some
-@[deprecated (since := "2024-03-05")] alias to_list_none := toList_none
-
-end Option
diff --git a/scripts/check_imports.lean b/scripts/check_imports.lean
index 55bf0e8342..bc651dcc12 100644
--- a/scripts/check_imports.lean
+++ b/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