chore: move to v4.13.0-rc1 (#979)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Batteries.lean

@@ -45,9 +45,7 @@ import Batteries.Lean.HashMap
 import Batteries.Lean.HashSet
 import Batteries.Lean.IO.Process
 import Batteries.Lean.Json
-import Batteries.Lean.Meta.AssertHypotheses
 import Batteries.Lean.Meta.Basic
-import Batteries.Lean.Meta.Clear
 import Batteries.Lean.Meta.DiscrTree
 import Batteries.Lean.Meta.Expr
 import Batteries.Lean.Meta.Inaccessible

Batteries/Classes/SatisfiesM.lean

@@ -171,12 +171,12 @@ theorem SatisfiesM_StateRefT_eq [Monad m] :
   · refine ⟨fun s => (fun ⟨⟨a, h⟩, s'⟩ => ⟨⟨a, s'⟩, h⟩) <$> f s, fun s => ?_⟩
     rw [← comp_map, map_eq_pure_bind]; rfl
   · refine ⟨fun s => (fun ⟨⟨a, s'⟩, h⟩ => ⟨⟨a, h⟩, s'⟩) <$> f s, funext fun s => ?_⟩
-    show _ >>= _ = _; simp [map_eq_pure_bind, ← h]
+    show _ >>= _ = _; simp [← h]
 
 @[simp] theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
     SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x := by
   refine ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, eq⟩ => eq ▸ ?_⟩
   · exists (fun | .ok ⟨a, h⟩ => ⟨.ok a, fun | _, rfl => h⟩ | .error e => ⟨.error e, nofun⟩) <$> f
     show _ = _ >>= _; rw [← comp_map, map_eq_pure_bind]; congr; funext a; cases a <;> rfl
   · exists ((fun | ⟨.ok a, h⟩ => .ok ⟨a, h _ rfl⟩ | ⟨.error e, _⟩ => .error e) <$> f : m _)
-    show _ >>= _ = _; simp [← comp_map, map_eq_pure_bind]; congr; funext ⟨a, h⟩; cases a <;> rfl
+    show _ >>= _ = _; simp [← comp_map, ← bind_pure_comp]; congr; funext ⟨a, h⟩; cases a <;> rfl

Batteries/Data/Array/Basic.lean

@@ -27,13 +27,6 @@ arrays, remove duplicates and then compare them elementwise.
 def equalSet [BEq α] (xs ys : Array α) : Bool :=
   xs.all (ys.contains ·) && ys.all (xs.contains ·)
 
-set_option linter.unusedVariables.funArgs false in
-/--
-Sort an array using `compare` to compare elements.
--/
-def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
-  xs.qsort fun x y => compare x y |>.isLT
-
 set_option linter.unusedVariables.funArgs false in
 /--
 Returns the first minimal element among `d` and elements of the array.
@@ -184,22 +177,6 @@ end Array
 
 namespace Subarray
 
-/--
-The empty subarray.
--/
-protected def empty : Subarray α where
-  array := #[]
-  start := 0
-  stop := 0
-  start_le_stop := Nat.le_refl 0
-  stop_le_array_size := Nat.le_refl 0
-
-instance : EmptyCollection (Subarray α) :=
-  ⟨Subarray.empty⟩
-
-instance : Inhabited (Subarray α) :=
-  ⟨{}⟩
-
 /--
 Check whether a subarray is empty.
 -/

Batteries/Data/Array/Lemmas.lean

@@ -11,30 +11,33 @@ import Batteries.Util.ProofWanted
 
 namespace Array
 
-theorem forIn_eq_forIn_data [Monad m]
+theorem forIn_eq_forIn_toList [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn as b f = forIn as.data b f := by
+    forIn as b f = forIn as.toList b f := by
   let rec loop : ∀ {i h b j}, j + i = as.size →
-      Array.forIn.loop as f i h b = forIn (as.data.drop j) b f
+      Array.forIn.loop as f i h b = forIn (as.toList.drop j) b f
     | 0, _, _, _, rfl => by rw [List.drop_length]; rfl
     | i+1, _, _, j, ij => by
       simp only [forIn.loop, Nat.add]
       have j_eq : j = size as - 1 - i := by simp [← ij, ← Nat.add_assoc]
       have : as.size - 1 - i < as.size := j_eq ▸ ij ▸ Nat.lt_succ_of_le (Nat.le_add_right ..)
-      have : as[size as - 1 - i] :: as.data.drop (j + 1) = as.data.drop j := by
+      have : as[size as - 1 - i] :: as.toList.drop (j + 1) = as.toList.drop j := by
         rw [j_eq]; exact List.getElem_cons_drop _ _ this
       simp only [← this, List.forIn_cons]; congr; funext x; congr; funext b
       rw [loop (i := i)]; rw [← ij, Nat.succ_add]; rfl
   conv => lhs; simp only [forIn, Array.forIn]
   rw [loop (Nat.zero_add _)]; rfl
+
+@[deprecated (since := "2024-09-09")] alias forIn_eq_forIn_data := forIn_eq_forIn_toList
 @[deprecated (since := "2024-08-13")] alias forIn_eq_data_forIn := forIn_eq_forIn_data
 
 /-! ### zipWith / zip -/
 
-theorem data_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
-    (as.zipWith bs f).data = as.data.zipWith f bs.data := by
+theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
+    (as.zipWith bs f).toList = as.toList.zipWith f bs.toList := by
   let rec loop : ∀ (i : Nat) cs, i ≤ as.size → i ≤ bs.size →
-      (zipWithAux f as bs i cs).data = cs.data ++ (as.data.drop i).zipWith f (bs.data.drop i) := by
+      (zipWithAux f as bs i cs).toList =
+        cs.toList ++ (as.toList.drop i).zipWith f (bs.toList.drop i) := by
     intro i cs hia hib
     unfold zipWithAux
     by_cases h : i = as.size ∨ i = bs.size
@@ -59,27 +62,30 @@ theorem data_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
       have has : i < as.size := Nat.lt_of_le_of_ne hia h.1
       have hbs : i < bs.size := Nat.lt_of_le_of_ne hib h.2
       simp only [has, hbs, dite_true]
-      rw [loop (i+1) _ has hbs, Array.push_data]
+      rw [loop (i+1) _ has hbs, Array.push_toList]
       have h₁ : [f as[i] bs[i]] = List.zipWith f [as[i]] [bs[i]] := rfl
-      let i_as : Fin as.data.length := ⟨i, has⟩
-      let i_bs : Fin bs.data.length := ⟨i, hbs⟩
+      let i_as : Fin as.toList.length := ⟨i, has⟩
+      let i_bs : Fin bs.toList.length := ⟨i, hbs⟩
       rw [h₁, List.append_assoc]
       congr
-      rw [← List.zipWith_append (h := by simp), getElem_eq_data_getElem, getElem_eq_data_getElem]
-      show List.zipWith f (as.data[i_as] :: List.drop (i_as + 1) as.data)
-        ((List.get bs.data i_bs) :: List.drop (i_bs + 1) bs.data) =
-        List.zipWith f (List.drop i as.data) (List.drop i bs.data)
-      simp only [data_length, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem]
+      rw [← List.zipWith_append (h := by simp), getElem_eq_getElem_toList,
+        getElem_eq_getElem_toList]
+      show List.zipWith f (as.toList[i_as] :: List.drop (i_as + 1) as.toList)
+        ((List.get bs.toList i_bs) :: List.drop (i_bs + 1) bs.toList) =
+        List.zipWith f (List.drop i as.toList) (List.drop i bs.toList)
+      simp only [length_toList, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem]
   simp [zipWith, loop 0 #[] (by simp) (by simp)]
+@[deprecated (since := "2024-09-09")] alias data_zipWith := toList_zipWith
 @[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith
 
 theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
     (as.zipWith bs f).size = min as.size bs.size := by
-  rw [size_eq_length_data, data_zipWith, List.length_zipWith]
+  rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
 
-theorem data_zip (as : Array α) (bs : Array β) :
-    (as.zip bs).data = as.data.zip bs.data :=
-  data_zipWith Prod.mk as bs
+theorem toList_zip (as : Array α) (bs : Array β) :
+    (as.zip bs).toList = as.toList.zip bs.toList :=
+  toList_zipWith Prod.mk as bs
+@[deprecated (since := "2024-09-09")] alias data_zip := toList_zip
 @[deprecated (since := "2024-08-13")] alias zip_eq_zip_data := data_zip
 
 theorem size_zip (as : Array α) (bs : Array β) :
@@ -90,42 +96,43 @@ theorem size_zip (as : Array α) (bs : Array β) :
 
 theorem size_filter_le (p : α → Bool) (l : Array α) :
     (l.filter p).size ≤ l.size := by
-  simp only [← data_length, filter_data]
+  simp only [← length_toList, toList_filter]
   apply List.length_filter_le
 
 /-! ### join -/
 
-@[simp] theorem data_join {l : Array (Array α)} : l.join.data = (l.data.map data).join := by
+@[simp] theorem toList_join {l : Array (Array α)} : l.join.toList = (l.toList.map toList).join := by
   dsimp [join]
-  simp only [foldl_eq_foldl_data]
-  generalize l.data = l
-  have : ∀ a : Array α, (List.foldl ?_ a l).data = a.data ++ ?_ := ?_
+  simp only [foldl_eq_foldl_toList]
+  generalize l.toList = l
+  have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
   exact this #[]
   induction l with
   | nil => simp
-  | cons h => induction h.data <;> simp [*]
+  | cons h => induction h.toList <;> simp [*]
+@[deprecated (since := "2024-09-09")] alias data_join := toList_join
 @[deprecated (since := "2024-08-13")] alias join_data := data_join
 
 theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l := by
-  simp only [mem_def, data_join, List.mem_join, List.mem_map]
+  simp only [mem_def, toList_join, List.mem_join, List.mem_map]
   intro l
   constructor
   · rintro ⟨_, ⟨s, m, rfl⟩, h⟩
     exact ⟨s, m, h⟩
   · rintro ⟨s, h₁, h₂⟩
-    refine ⟨s.data, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
+    refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
 
 /-! ### indexOf? -/
 
-theorem indexOf?_data [BEq α] {a : α} {l : Array α} :
-    l.data.indexOf? a = (l.indexOf? a).map Fin.val := by
+theorem indexOf?_toList [BEq α] {a : α} {l : Array α} :
+    l.toList.indexOf? a = (l.indexOf? a).map Fin.val := by
   simpa using aux l 0
 where
   aux (l : Array α) (i : Nat) :
-       ((l.data.drop i).indexOf? a).map (·+i) = (indexOfAux l a i).map Fin.val := by
+       ((l.toList.drop i).indexOf? a).map (·+i) = (indexOfAux l a i).map Fin.val := by
     rw [indexOfAux]
     if h : i < l.size then
-      rw [List.drop_eq_getElem_cons h, ←getElem_eq_data_getElem, List.indexOf?_cons]
+      rw [List.drop_eq_getElem_cons h, ←getElem_eq_getElem_toList, List.indexOf?_cons]
       if h' : l[i] == a then
         simp [h, h']
       else
@@ -137,42 +144,8 @@ where
 
 /-! ### erase -/
 
-theorem eraseIdx_data_swap {l : Array α} (i : Nat) (lt : i + 1 < size l) :
-    (l.swap ⟨i+1, lt⟩ ⟨i, Nat.lt_of_succ_lt lt⟩).data.eraseIdx (i+1) = l.data.eraseIdx i := by
-  let ⟨xs⟩ := l
-  induction i generalizing xs <;> let x₀::x₁::xs := xs
-  case zero => simp [swap, get]
-  case succ i ih _ =>
-    have lt' := Nat.lt_of_succ_lt_succ lt
-    have : (swap ⟨x₀::x₁::xs⟩ ⟨i.succ + 1, lt⟩ ⟨i.succ, Nat.lt_of_succ_lt lt⟩).data
-        = x₀::(swap ⟨x₁::xs⟩ ⟨i + 1, lt'⟩ ⟨i, Nat.lt_of_succ_lt lt'⟩).data := by
-      simp [swap_def, getElem_eq_data_getElem]
-    simp [this, ih]
-
-@[simp] theorem data_feraseIdx {l : Array α} (i : Fin l.size) :
-    (l.feraseIdx i).data = l.data.eraseIdx i := by
-  induction l, i using feraseIdx.induct with
-  | @case1 a i lt a' i' ih =>
-    rw [feraseIdx]
-    simp [lt, ih, a', eraseIdx_data_swap i lt]
-  | case2 a i lt =>
-    have : i + 1 ≥ a.size := Nat.ge_of_not_lt lt
-    have last : i + 1 = a.size := Nat.le_antisymm i.is_lt this
-    simp [feraseIdx, lt, List.dropLast_eq_eraseIdx last]
-
-@[simp] theorem data_erase [BEq α] (l : Array α) (a : α) : (l.erase a).data = l.data.erase a := by
-  match h : indexOf? l a with
-  | none =>
-    simp only [erase, h]
-    apply Eq.symm
-    rw [List.erase_eq_self_iff_forall_bne, ←List.indexOf?_eq_none_iff, indexOf?_data,
-        h, Option.map_none']
-  | some i =>
-    simp only [erase, h]
-    rw [data_feraseIdx, ←List.eraseIdx_indexOf_eq_erase]
-    congr
-    rw [List.indexOf_eq_indexOf?, indexOf?_data]
-    simp [h]
+@[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} :
+    (l.erase a).toList = l.toList.erase a
 
 /-! ### shrink -/
 
@@ -196,12 +169,10 @@ theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by
 theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
   rw [mapM, mapM.map]; rfl
 
-@[simp] theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty ..
+theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
 
 /-! ### mem -/
 
-alias not_mem_empty := not_mem_nil
-
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
 
 /-! ### append -/
@@ -230,7 +201,7 @@ private theorem get_insertAt_loop_lt (as : Array α) (i : Fin (as.size+1)) (j :
   split
   · have h1 : k ≠ j - 1 := by omega
     have h2 : k ≠ j := by omega
-    rw [get_insertAt_loop_lt, get_swap, if_neg h1, if_neg h2]
+    rw [get_insertAt_loop_lt, getElem_swap, if_neg h1, if_neg h2]
     exact h
   · rfl
 
@@ -241,7 +212,7 @@ private theorem get_insertAt_loop_gt (as : Array α) (i : Fin (as.size+1)) (j :
   split
   · have h1 : k ≠ j - 1 := by omega
     have h2 : k ≠ j := by omega
-    rw [get_insertAt_loop_gt, get_swap, if_neg h1, if_neg h2]
+    rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_neg h2]
     exact Nat.lt_of_le_of_lt (Nat.pred_le _) hgt
   · rfl
 
@@ -251,8 +222,7 @@ private theorem get_insertAt_loop_eq (as : Array α) (i : Fin (as.size+1)) (j :
   unfold insertAt.loop
   split
   · next h =>
-    rw [get_insertAt_loop_eq, Fin.getElem_fin, get_swap, if_pos rfl]
-    exact Nat.lt_of_le_of_lt (Nat.pred_le _) j.is_lt
+    rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_swap, if_pos rfl]
     exact heq
     exact Nat.le_pred_of_lt h
   · congr; omega
@@ -266,18 +236,17 @@ private theorem get_insertAt_loop_gt_le (as : Array α) (i : Fin (as.size+1)) (j
     if h0 : k = j then
       cases h0
       have h1 : j.val ≠ j - 1 := by omega
-      rw [get_insertAt_loop_gt, get_swap, if_neg h1, if_pos rfl]; rfl
-      · exact j.is_lt
-      · exact Nat.pred_lt_of_lt hgt
+      rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_pos rfl]; rfl
+      exact Nat.pred_lt_of_lt hgt
     else
       have h1 : k - 1 ≠ j - 1 := by omega
       have h2 : k - 1 ≠ j := by omega
-      rw [get_insertAt_loop_gt_le, get_swap, if_neg h1, if_neg h2]
-      exact hgt
+      rw [get_insertAt_loop_gt_le, getElem_swap, if_neg h1, if_neg h2]
       apply Nat.le_of_lt_add_one
       rw [Nat.sub_one_add_one]
       exact Nat.lt_of_le_of_ne hle h0
       exact Nat.not_eq_zero_of_lt h
+      exact hgt
   · next h =>
     absurd h
     exact Nat.lt_of_lt_of_le hgt hle

Batteries/Data/Array/Merge.lean

@@ -31,6 +31,8 @@ set_option linter.unusedVariables false in
 def mergeSortedPreservingDuplicates [ord : Ord α] (xs ys : Array α) : Array α :=
   merge (compare · · |>.isLT) xs ys
 
+-- We name `ord` so it can be provided as a named argument.
+set_option linter.unusedVariables.funArgs false in
 /--
 `O(|xs| + |ys|)`. Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
 not contain duplicates. Equal elements are merged using `merge`. If `merge` respects the order
@@ -85,6 +87,8 @@ where
 
 @[deprecated (since := "2024-04-24")] alias mergeUnsortedDeduplicating := mergeUnsortedDedup
 
+-- We name `eq` so it can be provided as a named argument.
+set_option linter.unusedVariables.funArgs false in
 /--
 `O(|xs|)`. Replace each run `[x₁, ⋯, xₙ]` of equal elements in `xs` with
 `f ⋯ (f (f x₁ x₂) x₃) ⋯ xₙ`.

Batteries/Data/Array/OfFn.lean

@@ -12,12 +12,7 @@ namespace Array
 /-! ### ofFn -/
 
 @[simp]
-theorem data_ofFn (f : Fin n → α) : (ofFn f).data = List.ofFn f := by
-  ext1
-  simp only [getElem?_eq, data_length, size_ofFn, length_ofFn, getElem_ofFn]
-  split
-  · rw [← getElem_eq_data_getElem]
-    simp
-  · rfl
+theorem toList_ofFn (f : Fin n → α) : (ofFn f).toList = List.ofFn f := by
+  apply ext_getElem <;> simp
 
 end Array

Batteries/Data/Array/Pairwise.lean

@@ -17,15 +17,15 @@ larger indices.
 For example `as.Pairwise (· ≠ ·)` asserts that `as` has no duplicates, `as.Pairwise (· < ·)` asserts
 that `as` is strictly sorted and `as.Pairwise (· ≤ ·)` asserts that `as` is weakly sorted.
 -/
-def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.data.Pairwise R
+def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwise R
 
 theorem pairwise_iff_get {as : Array α} : as.Pairwise R ↔
     ∀ (i j : Fin as.size), i < j → R (as.get i) (as.get j) := by
-  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_data_get]; rfl
+  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_toList_get]
 
 theorem pairwise_iff_getElem {as : Array α} : as.Pairwise R ↔
     ∀ (i j : Nat) (_ : i < as.size) (_ : j < as.size), i < j → R as[i] as[j] := by
-  unfold Pairwise; simp [List.pairwise_iff_getElem, data_length]; rfl
+  unfold Pairwise; simp [List.pairwise_iff_getElem, length_toList]
 
 instance (R : α → α → Prop) [DecidableRel R] (as) : Decidable (Pairwise R as) :=
   have : (∀ (j : Fin as.size) (i : Fin j.val), R as[i.val] (as[j.val])) ↔ Pairwise R as := by
@@ -46,16 +46,17 @@ theorem pairwise_pair : #[a, b].Pairwise R ↔ R a b := by
 
 theorem pairwise_append {as bs : Array α} :
     (as ++ bs).Pairwise R ↔ as.Pairwise R ∧ bs.Pairwise R ∧ (∀ x ∈ as, ∀ y ∈ bs, R x y) := by
-  unfold Pairwise; simp [← mem_data, append_data, ← List.pairwise_append]
+  unfold Pairwise; simp [← mem_toList, toList_append, ← List.pairwise_append]
 
 theorem pairwise_push {as : Array α} :
     (as.push a).Pairwise R ↔ as.Pairwise R ∧ (∀ x ∈ as, R x a) := by
   unfold Pairwise
-  simp [← mem_data, push_data, List.pairwise_append, List.pairwise_singleton, List.mem_singleton]
+  simp [← mem_toList, push_toList, List.pairwise_append, List.pairwise_singleton,
+    List.mem_singleton]
 
 theorem pairwise_extract {as : Array α} (h : as.Pairwise R) (start stop) :
     (as.extract start stop).Pairwise R := by
-  simp only [pairwise_iff_getElem, get_extract, size_extract] at h ⊢
+  simp only [pairwise_iff_getElem, getElem_extract, size_extract] at h ⊢
   intro _ _ _ _ hlt
   apply h
   exact Nat.add_lt_add_left hlt start

Batteries/Data/AssocList.lean

@@ -78,7 +78,7 @@ def toListTR (as : AssocList α β) : List (α × β) :=
 
 @[csimp] theorem toList_eq_toListTR : @toList = @toListTR := by
   funext α β as; simp [toListTR]
-  exact .symm <| (Array.foldl_data_eq_map (toList as) _ id).trans (List.map_id _)
+  exact .symm <| (Array.foldl_toList_eq_map (toList as) _ id).trans (List.map_id _)
 
 /-- `O(n)`. Run monadic function `f` on all elements in the list, from head to tail. -/
 @[specialize] def forM [Monad m] (f : α → β → m PUnit) : AssocList α β → m PUnit