chore: remove >6 month old deprecations (leanprover#10968)

Author: kim-em

src/Init/Classical.lean

@@ -181,9 +181,6 @@ theorem not_imp_iff_and_not : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff
 
 theorem not_and_iff_not_or_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and_iff_not_or_not
 
-@[deprecated not_and_iff_not_or_not (since := "2025-03-18")]
-abbrev not_and_iff_or_not_not := @not_and_iff_not_or_not
-
 theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff
 
 @[simp] theorem imp_iff_left_iff  : (b ↔ a → b) ↔ a ∨ b := Decidable.imp_iff_left_iff

src/Init/Control/Lawful/Basic.lean

@@ -255,11 +255,6 @@ instance : LawfulMonad Id := by
 @[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
 @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
 
--- These lemmas are bad as they abuse the defeq of `Id α` and `α`
-@[deprecated run_map (since := "2025-03-05")] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl
-@[deprecated run_bind (since := "2025-03-05")] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl
-@[deprecated run_pure (since := "2025-03-05")] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
-
 end Id
 
 /-! # Option -/

src/Init/Core.lean

@@ -600,17 +600,6 @@ export LawfulSingleton (insert_empty_eq)
 
 attribute [simp] insert_empty_eq
 
-@[deprecated insert_empty_eq (since := "2025-03-12")]
-theorem insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
-    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
-  insert_empty_eq _
-
-@[deprecated insert_empty_eq (since := "2025-03-12")]
-theorem LawfulSingleton.insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
-    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
-  insert_empty_eq _
-
-
 /-- Type class used to implement the notation `{ a ∈ c | p a }` -/
 class Sep (α : outParam <| Type u) (γ : Type v) where
   /-- Computes `{ a ∈ c | p a }`. -/

src/Init/Data/Array/Attach.lean

@@ -749,9 +749,6 @@ and simplifies these to the function directly taking the value.
     (Array.replicate n x).unattach = Array.replicate n x.1 := by
   simp [unattach]
 
-@[deprecated unattach_replicate (since := "2025-03-18")]
-abbrev unattach_mkArray := @unattach_replicate
-
 /-! ### Well-founded recursion preprocessing setup -/
 
 @[wf_preprocess] theorem map_wfParam {xs : Array α} {f : α → β} :

src/Init/Data/Array/Basic.lean

@@ -209,20 +209,6 @@ Examples:
 def replicate {α : Type u} (n : Nat) (v : α) : Array α where
   toList := List.replicate n v
 
-/--
-Creates an array that contains `n` repetitions of `v`.
-
-The corresponding `List` function is `List.replicate`.
-
-Examples:
- * `Array.mkArray 2 true = #[true, true]`
- * `Array.mkArray 3 () = #[(), (), ()]`
- * `Array.mkArray 0 "anything" = #[]`
--/
-@[extern "lean_mk_array", deprecated replicate (since := "2025-03-18")]
-def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
-  toList := List.replicate n v
-
 /--
 Swaps two elements of an array. The modification is performed in-place when the reference to the
 array is unique.
@@ -2147,5 +2133,3 @@ instance [ToString α] : ToString (Array α) where
   toString xs := String.Internal.append "#" (toString xs.toList)
 
 end Array
-
-export Array (mkArray)

src/Init/Data/Array/Count.lean

@@ -99,9 +99,6 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
 theorem countP_replicate {a : α} {n : Nat} : countP p (replicate n a) = if p a then n else 0 := by
   simp [← List.toArray_replicate, List.countP_replicate]
 
-@[deprecated countP_replicate (since := "2025-03-18")]
-abbrev countP_mkArray := @countP_replicate
-
 theorem boole_getElem_le_countP {xs : Array α} {i : Nat} (h : i < xs.size) :
     (if p xs[i] then 1 else 0) ≤ xs.countP p := by
   rcases xs with ⟨xs⟩
@@ -262,15 +259,9 @@ theorem count_eq_size {xs : Array α} : count a xs = xs.size ↔ ∀ b ∈ xs, a
 @[simp] theorem count_replicate_self {a : α} {n : Nat} : count a (replicate n a) = n := by
   simp [← List.toArray_replicate]
 
-@[deprecated count_replicate_self (since := "2025-03-18")]
-abbrev count_mkArray_self := @count_replicate_self
-
 theorem count_replicate {a b : α} {n : Nat} : count a (replicate n b) = if b == a then n else 0 := by
   simp [← List.toArray_replicate, List.count_replicate]
 
-@[deprecated count_replicate (since := "2025-03-18")]
-abbrev count_mkArray := @count_replicate
-
 theorem filter_beq {xs : Array α} (a : α) : xs.filter (· == a) = replicate (count a xs) a := by
   rcases xs with ⟨xs⟩
   simp [List.filter_beq]
@@ -284,9 +275,6 @@ theorem replicate_count_eq_of_count_eq_size {xs : Array α} (h : count a xs = xs
   rw [← toList_inj]
   simp [List.replicate_count_eq_of_count_eq_length (by simpa using h)]
 
-@[deprecated replicate_count_eq_of_count_eq_size (since := "2025-03-18")]
-abbrev mkArray_count_eq_of_count_eq_size := @replicate_count_eq_of_count_eq_size
-
 @[simp] theorem count_filter {xs : Array α} (h : p a) : count a (filter p xs) = count a xs := by
   rcases xs with ⟨xs⟩
   simp [List.count_filter, h]

src/Init/Data/Array/Erase.lean

@@ -139,25 +139,16 @@ theorem eraseP_replicate {n : Nat} {a : α} {p : α → Bool} :
   simp only [← List.toArray_replicate, List.eraseP_toArray, List.eraseP_replicate]
   split <;> simp
 
-@[deprecated eraseP_replicate (since := "2025-03-18")]
-abbrev eraseP_mkArray := @eraseP_replicate
-
 @[simp] theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) :
     (replicate n a).eraseP p = replicate (n - 1) a := by
   simp only [← List.toArray_replicate, List.eraseP_toArray]
   simp [h]
 
-@[deprecated eraseP_replicate_of_pos (since := "2025-03-18")]
-abbrev eraseP_mkArray_of_pos := @eraseP_replicate_of_pos
-
 @[simp] theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) :
     (replicate n a).eraseP p = replicate n a := by
   simp only [← List.toArray_replicate, List.eraseP_toArray]
   simp [h]
 
-@[deprecated eraseP_replicate_of_neg (since := "2025-03-18")]
-abbrev eraseP_mkArray_of_neg := @eraseP_replicate_of_neg
-
 theorem eraseP_eq_iff {p} {xs : Array α} :
     xs.eraseP p = ys ↔
       ((∀ a ∈ xs, ¬ p a) ∧ xs = ys) ∨
@@ -278,9 +269,6 @@ theorem erase_replicate [LawfulBEq α] {n : Nat} {a b : α} :
   simp only [List.erase_replicate, beq_iff_eq, List.toArray_replicate]
   split <;> simp
 
-@[deprecated erase_replicate (since := "2025-03-18")]
-abbrev erase_mkArray := @erase_replicate
-
 -- The arguments `a b` are explicit,
 -- so they can be specified to prevent `simp` repeatedly applying the lemma.
 @[grind =]
@@ -308,17 +296,11 @@ theorem erase_eq_iff [LawfulBEq α] {a : α} {xs : Array α} :
   simp only [← List.toArray_replicate, List.erase_toArray]
   simp
 
-@[deprecated erase_replicate_self (since := "2025-03-18")]
-abbrev erase_mkArray_self := @erase_replicate_self
-
 @[simp] theorem erase_replicate_ne [LawfulBEq α] {a b : α} (h : !b == a) :
     (replicate n a).erase b = replicate n a := by
   rw [erase_of_not_mem]
   simp_all
 
-@[deprecated erase_replicate_ne (since := "2025-03-18")]
-abbrev erase_mkArray_ne := @erase_replicate_ne
-
 end erase
 
 /-! ### eraseIdxIfInBounds -/
@@ -429,9 +411,6 @@ theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} {h} :
   simp only [← List.toArray_replicate, List.eraseIdx_toArray]
   simp [List.eraseIdx_replicate, h]
 
-@[deprecated eraseIdx_replicate (since := "2025-03-18")]
-abbrev eraseIdx_mkArray := @eraseIdx_replicate
-
 theorem mem_eraseIdx_iff_getElem {x : α} {xs : Array α} {k} {h} : x ∈ xs.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ xs[i]'w = x := by
   rcases xs with ⟨xs⟩
   simp [List.mem_eraseIdx_iff_getElem, *]

src/Init/Data/Array/Extract.lean

@@ -289,9 +289,6 @@ theorem extract_append_right {as bs : Array α} :
   · simp only [size_extract, size_replicate] at h₁ h₂
     simp only [getElem_extract, getElem_replicate]
 
-@[deprecated extract_replicate (since := "2025-03-18")]
-abbrev extract_mkArray := @extract_replicate
-
 theorem extract_eq_extract_right {as : Array α} {i j j' : Nat} :
     as.extract i j = as.extract i j' ↔ min (j - i) (as.size - i) = min (j' - i) (as.size - i) := by
   rcases as with ⟨as⟩
@@ -429,32 +426,20 @@ theorem popWhile_append {xs ys : Array α} :
     (replicate n a).takeWhile p = (replicate n a).filter p := by
   simp [← List.toArray_replicate]
 
-@[deprecated takeWhile_replicate_eq_filter (since := "2025-03-18")]
-abbrev takeWhile_mkArray_eq_filter := @takeWhile_replicate_eq_filter
-
 theorem takeWhile_replicate {p : α → Bool} :
     (replicate n a).takeWhile p = if p a then replicate n a else #[] := by
   simp [takeWhile_replicate_eq_filter, filter_replicate]
 
-@[deprecated takeWhile_replicate (since := "2025-03-18")]
-abbrev takeWhile_mkArray := @takeWhile_replicate
-
 @[simp] theorem popWhile_replicate_eq_filter_not {p : α → Bool} :
     (replicate n a).popWhile p = (replicate n a).filter (fun a => !p a) := by
   simp [← List.toArray_replicate, ← List.filter_reverse]
 
-@[deprecated popWhile_replicate_eq_filter_not (since := "2025-03-18")]
-abbrev popWhile_mkArray_eq_filter_not := @popWhile_replicate_eq_filter_not
-
 theorem popWhile_replicate {p : α → Bool} :
     (replicate n a).popWhile p = if p a then #[] else replicate n a := by
   simp only [popWhile_replicate_eq_filter_not, size_replicate, filter_replicate, Bool.not_eq_eq_eq_not,
     Bool.not_true]
   split <;> simp_all
 
-@[deprecated popWhile_replicate (since := "2025-03-18")]
-abbrev popWhile_mkArray := @popWhile_replicate
-
 theorem extract_takeWhile {as : Array α} {i : Nat} :
     (as.takeWhile p).extract 0 i = (as.extract 0 i).takeWhile p := by
   rcases as with ⟨as⟩

src/Init/Data/Array/Find.lean

@@ -129,31 +129,19 @@ theorem getElem_zero_flatten {xss : Array (Array α)} (h) :
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   simp [← List.toArray_replicate, List.findSome?_replicate]
 
-@[deprecated findSome?_replicate (since := "2025-03-18")]
-abbrev findSome?_mkArray := @findSome?_replicate
-
 @[simp] theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by
   simp [findSome?_replicate, Nat.ne_of_gt h]
 
-@[deprecated findSome?_replicate_of_pos (since := "2025-03-18")]
-abbrev findSome?_mkArray_of_pos := @findSome?_replicate_of_pos
-
 -- Argument is unused, but used to decide whether `simp` should unfold.
 @[simp] theorem findSome?_replicate_of_isSome (_ : (f a).isSome) :
    findSome? f (replicate n a) = if n = 0 then none else f a := by
   simp [findSome?_replicate]
 
-@[deprecated findSome?_replicate_of_isSome (since := "2025-03-18")]
-abbrev findSome?_mkArray_of_isSome := @findSome?_replicate_of_isSome
-
 @[simp] theorem findSome?_replicate_of_isNone (h : (f a).isNone) :
     findSome? f (replicate n a) = none := by
   rw [Option.isNone_iff_eq_none] at h
   simp [findSome?_replicate, h]
 
-@[deprecated findSome?_replicate_of_isNone (since := "2025-03-18")]
-abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
-
 /-! ### find? -/
 
 @[simp, grind =] theorem find?_empty : find? p #[] = none := rfl
@@ -318,16 +306,10 @@ theorem find?_replicate :
     find? p (replicate n a) = if p a then some a else none := by
   simp [find?_replicate, Nat.ne_of_gt h]
 
-@[deprecated find?_replicate_of_size_pos (since := "2025-03-18")]
-abbrev find?_mkArray_of_length_pos := @find?_replicate_of_size_pos
-
 @[simp] theorem find?_replicate_of_pos (h : p a) :
     find? p (replicate n a) = if n = 0 then none else some a := by
   simp [find?_replicate, h]
 
-@[deprecated find?_replicate_of_pos (since := "2025-03-18")]
-abbrev find?_mkArray_of_pos := @find?_replicate_of_pos
-
 @[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
   simp [find?_replicate, h]
 
@@ -583,9 +565,6 @@ theorem findIdx?_flatten {xss : Array (Array α)} {p : α → Bool} :
   simp only [List.findIdx?_toArray]
   simp
 
-@[deprecated findIdx?_replicate (since := "2025-03-18")]
-abbrev findIdx?_mkArray := @findIdx?_replicate
-
 theorem findIdx?_eq_findSome?_zipIdx {xs : Array α} {p : α → Bool} :
     xs.findIdx? p = xs.zipIdx.findSome? fun ⟨a, i⟩ => if p a then some i else none := by
   rcases xs with ⟨xs⟩