chore: adaptations for nightly-2024-09-27 (#971)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

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/Lemmas.lean

@@ -68,8 +68,8 @@ theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
       let i_bs : Fin bs.toList.length := ⟨i, hbs⟩
       rw [h₁, List.append_assoc]
       congr
-      rw [← List.zipWith_append (h := by simp), getElem_eq_toList_getElem,
-        getElem_eq_toList_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)
@@ -96,7 +96,7 @@ theorem size_zip (as : Array α) (bs : Array β) :
 
 theorem size_filter_le (p : α → Bool) (l : Array α) :
     (l.filter p).size ≤ l.size := by
-  simp only [← toList_length, filter_toList]
+  simp only [← toList_length, toList_filter]
   apply List.length_filter_le
 
 /-! ### join -/
@@ -124,15 +124,15 @@ theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L 
 
 /-! ### 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
@@ -144,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 -/
 
@@ -203,7 +169,7 @@ 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 -/
 

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

@@ -21,11 +21,11 @@ def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwi
 
 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_toList_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, toList_length]; rfl
+  unfold Pairwise; simp [List.pairwise_iff_getElem, toList_length]
 
 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

Batteries/Data/Fin/Lemmas.lean

@@ -9,10 +9,6 @@ namespace Fin
 
 attribute [norm_cast] val_last
 
-/-! ### last -/
-
-@[simp] theorem last_zero : last 0 = 0 := rfl
-
 /-! ### clamp -/
 
 @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl
@@ -30,7 +26,7 @@ attribute [norm_cast] val_last
 
 @[simp] theorem getElem_list (i : Nat) (h : i < (list n).length) :
     (list n)[i] = cast (length_list n) ⟨i, h⟩ := by
-  simp only [list]; rw [← Array.getElem_eq_toList_getElem, getElem_enum, cast_mk]
+  simp only [list]; rw [← Array.getElem_eq_getElem_toList, getElem_enum, cast_mk]
 
 @[deprecated getElem_list (since := "2024-06-12")]
 theorem get_list (i : Fin (list n).length) : (list n).get i = i.cast (length_list n) := by
@@ -44,14 +40,14 @@ theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by
 theorem list_succ_last (n) : list (n+1) = (list n).map castSucc ++ [last n] := by
   rw [list_succ]
   induction n with
-  | zero => simp [last]
+  | zero => simp
   | succ n ih =>
     rw [list_succ, List.map_cons castSucc, ih]
     simp [Function.comp_def, succ_castSucc]
 
 theorem list_reverse (n) : (list n).reverse = (list n).map rev := by
   induction n with
-  | zero => simp [last]
+  | zero => simp
   | succ n ih =>
     conv => lhs; rw [list_succ_last]
     conv => rhs; rw [list_succ]

Batteries/Data/HashMap/WF.lean

@@ -26,7 +26,7 @@ theorem toList_update (self : Buckets α β) (i d h) :
 theorem exists_of_update (self : Buckets α β) (i d h) :
     ∃ l₁ l₂, self.1.toList = l₁ ++ self.1[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
       (self.update i d h).1.toList = l₁ ++ d :: l₂ := by
-  simp only [Array.toList_length, Array.ugetElem_eq_getElem, Array.getElem_eq_toList_getElem]
+  simp only [Array.toList_length, Array.ugetElem_eq_getElem, Array.getElem_eq_getElem_toList]
   exact List.exists_of_set h
 
 theorem update_update (self : Buckets α β) (i d d' h h') :
@@ -46,7 +46,7 @@ theorem WF.mk' [BEq α] [Hashable α] (h) : (Buckets.mk n h : Buckets α β).WF
   refine ⟨fun _ h => ?_, fun i h => ?_⟩
   · simp only [Buckets.mk, mkArray, List.mem_replicate, ne_eq] at h
     simp [h, List.Pairwise.nil]
-  · simp [Buckets.mk, empty', mkArray, Array.getElem_eq_toList_getElem, AssocList.All]
+  · simp [Buckets.mk, empty', mkArray, Array.getElem_eq_getElem_toList, AssocList.All]
 
 theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H : buckets.WF)
     (h₁ : ∀ [PartialEquivBEq α] [LawfulHashable α],
@@ -60,7 +60,7 @@ theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H :
     | .inl hl => H.1 _ hl
     | .inr rfl => h₁ (H.1 _ (Array.getElem_mem_toList ..))
   · revert hp
-    simp only [Array.getElem_eq_toList_getElem, toList_update, List.getElem_set,
+    simp only [Array.getElem_eq_getElem_toList, toList_update, List.getElem_set,
       Array.toList_length, update_size]
     split <;> intro hp
     · next eq => exact eq ▸ h₂ (H.2 _ _) _ hp
@@ -98,19 +98,19 @@ where
     · next H =>
       refine (go (i+1) _ _ fun j hj => ?a).trans ?b
       · case a =>
-        simp only [Array.data_length, Array.data_set]
+        simp only [Array.toList_length, Array.toList_set]
         simp [List.getD_eq_getElem?_getD, List.getElem?_set, Option.map_eq_map]; split
         · cases source.toList[j]? <;> rfl
         · next H => exact hs _ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (Ne.symm H))
       · case b =>
-        simp only [Array.data_length, Array.data_set, Array.get_eq_getElem, AssocList.foldl_eq]
+        simp only [Array.toList_length, Array.toList_set, Array.get_eq_getElem, AssocList.foldl_eq]
         refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set H; eq ▸ ?_
         rw [h₁]
         simp only [Buckets.size_eq, List.map_append, List.map_cons, AssocList.toList,
           List.length_nil, Nat.sum_append, Nat.sum_cons, Nat.zero_add, Array.toList_length]
         rw [Nat.add_assoc, Nat.add_assoc, Nat.add_assoc]; congr 1
         (conv => rhs; rw [Nat.add_left_comm]); congr 1
-        rw [← Array.getElem_eq_toList_getElem]
+        rw [← Array.getElem_eq_getElem_toList]
         have := @reinsertAux_size α β _; simp [Buckets.size] at this
         induction source[i].toList generalizing target <;> simp [*, Nat.succ_add]; rfl
     · next H =>
@@ -173,7 +173,7 @@ where
       · match List.mem_or_eq_of_mem_set hl with
         | .inl hl => exact hs₁ _ hl
         | .inr e => exact e ▸ .nil
-      · simp only [Array.toList_length, Array.size_set, Array.getElem_eq_toList_getElem,
+      · simp only [Array.toList_length, Array.size_set, Array.getElem_eq_getElem_toList,
           Array.toList_set, List.getElem_set]
         split
         · nofun
@@ -371,7 +371,7 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable
     have := H.out.2.1 _ h
     rw [← List.pairwise_map (R := (¬ · == ·))] at this ⊢
     exact this.sublist (H3 l.toList)
-  · simp only [Array.size_mk, List.length_map, Array.toList_length, Array.getElem_eq_toList_getElem,
+  · simp only [Array.size_mk, List.length_map, Array.toList_length, Array.getElem_eq_getElem_toList,
       List.getElem_map] at h ⊢
     have := H.out.2.2 _ h
     simp only [AssocList.All, List.toList_toAssocList, List.mem_reverse, List.mem_filterMap,
@@ -387,13 +387,15 @@ variable {_ : BEq α} {_ : Hashable α}
 @[inline] def mapVal (f : α → β → γ) (self : HashMap α β) : HashMap α γ :=
   ⟨self.1.mapVal f, self.2.mapVal⟩
 
-/--
-Applies `f` to each key-value pair `a, b` in the map. If it returns `some c` then
-`a, c` is pushed into the new map; else the key is removed from the map.
--/
-@[inline] def filterMap (f : α → β → Option γ) (self : HashMap α β) : HashMap α γ :=
-  ⟨self.1.filterMap f, self.2.filterMap⟩
+-- Temporarily removed on lean-pr-testing-5403.
+
+-- /--
+-- Applies `f` to each key-value pair `a, b` in the map. If it returns `some c` then
+-- `a, c` is pushed into the new map; else the key is removed from the map.
+-- -/
+-- @[inline] def filterMap (f : α → β → Option γ) (self : HashMap α β) : HashMap α γ :=
+--   ⟨self.1.filterMap f, self.2.filterMap⟩
 
-/-- Constructs a map with the set of all pairs `a, b` such that `f` returns true. -/
-@[inline] def filter (f : α → β → Bool) (self : HashMap α β) : HashMap α β :=
-  self.filterMap fun a b => bif f a b then some b else none
+-- /-- Constructs a map with the set of all pairs `a, b` such that `f` returns true. -/
+-- @[inline] def filter (f : α → β → Bool) (self : HashMap α β) : HashMap α β :=
+--   self.filterMap fun a b => bif f a b then some b else none

Batteries/Data/List/Lemmas.lean

@@ -10,29 +10,11 @@ import Batteries.Tactic.Alias
 
 namespace List
 
-/-! ### mem -/
-
-@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
-  simp [Array.mem_def]
-
 /-! ### toArray-/
 
-@[simp] theorem size_toArrayAux (l : List α) (r : Array α) :
-    (l.toArrayAux r).size = r.size + l.length := by
-  induction l generalizing r with
-  | nil => simp [toArrayAux]
-  | cons a l ih =>
-    simp [ih, List.toArrayAux]
-    omega
-
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) :
     (Array.mk xs)[i] = xs[i] := rfl
 
-@[simp] theorem getElem_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
-    l.toArray[i] = l[i]'(by simpa using h) := by
-  rw [Array.getElem_eq_data_getElem]
-  simp
-
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl
@@ -231,12 +213,6 @@ theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) :
 theorem length_tail_add_one (l : List α) (h : 0 < length l) : (length (tail l)) + 1 = length l := by
   simp [Nat.sub_add_cancel h]
 
-@[simp] theorem getElem?_tail (l : List α) : l.tail[n]? = l[n + 1]? := by cases l <;> simp
-
-@[simp] theorem getElem_tail (l : List α) (h : n < l.tail.length) :
-    l.tail[n] = l[n + 1]'(by simp at h; omega) := by
-  cases l; contradiction; simp
-
 /-! ### eraseP -/
 
 @[simp] theorem extractP_eq_find?_eraseP
@@ -417,7 +393,7 @@ theorem pair_mem_product {xs : List α} {ys : List β} {x : α} {y : β} :
 theorem forIn_eq_bindList [Monad m] [LawfulMonad m]
     (f : α → β → m (ForInStep β)) (l : List α) (init : β) :
     forIn l init f = ForInStep.run <$> (ForInStep.yield init).bindList f l := by
-  induction l generalizing init <;> simp [*, map_eq_pure_bind]
+  induction l generalizing init <;> simp [*]
   congr; ext (b | b) <;> simp
 
 /-! ### diff -/
@@ -673,37 +649,6 @@ theorem insertP_loop (a : α) (l r : List α) :
   induction l with simp [insertP, insertP.loop, cond]
   | cons _ _ ih => split <;> simp [insertP_loop, ih]
 
-/-! ### merge -/
-
-theorem cons_merge_cons (s : α → α → Bool) (a b l r) :
-    merge (a::l) (b::r) s = if s a b then a :: merge l (b::r) s else b :: merge (a::l) r s := by
-  simp only [merge]
-
-@[simp] theorem cons_merge_cons_pos (s : α → α → Bool) (l r) (h : s a b) :
-    merge (a::l) (b::r) s = a :: merge l (b::r) s := by
-  rw [cons_merge_cons, if_pos h]
-
-@[simp] theorem cons_merge_cons_neg (s : α → α → Bool) (l r) (h : ¬ s a b) :
-    merge (a::l) (b::r) s = b :: merge (a::l) r s := by
-  rw [cons_merge_cons, if_neg h]
-
-@[simp] theorem length_merge (s : α → α → Bool) (l r) :
-    (merge l r s).length = l.length + r.length := by
-  match l, r with
-  | [], r => simp
-  | l, [] => simp
-  | a::l, b::r =>
-    rw [cons_merge_cons]
-    split
-    · simp_arith [length_merge s l (b::r)]
-    · simp_arith [length_merge s (a::l) r]
-
-theorem mem_merge_left (s : α → α → Bool) (h : x ∈ l) : x ∈ merge l r s :=
-  mem_merge.2 <| .inl h
-
-theorem mem_merge_right (s : α → α → Bool) (h : x ∈ r) : x ∈ merge l r s :=
-  mem_merge.2 <| .inr h
-
 /-! ### foldlM and foldrM -/
 
 theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :

Batteries/Data/Vector/Basic.lean

@@ -263,7 +263,7 @@ alias take := shrink
 if and only if `p a[i] b[i]` holds true for all valid indices `i`.
 -/
 @[inline] def isEqv (a b : Vector α n) (p : α → α → Bool) : Bool :=
-  Array.isEqvAux a.toArray b.toArray (a.size_eq.trans b.size_eq.symm) p 0
+  Array.isEqvAux a.toArray b.toArray (a.size_eq.trans b.size_eq.symm) p 0 (Nat.zero_le _)
 
 instance [BEq α] : BEq (Vector α n) :=
   ⟨fun a b => isEqv a b BEq.beq⟩

Batteries/Lean/HashSet.lean

@@ -59,10 +59,3 @@ def insert' (s : HashSet α) (a : α) : HashSet α × Bool :=
   let oldSize := s.size
   let s := s.insert a
   (s, s.size == oldSize)
-
-/--
-`O(n)`. Obtain a `HashSet` from an array.
--/
-@[inline]
-protected def ofArray [BEq α] [Hashable α] (as : Array α) : HashSet α :=
-  HashSet.empty.insertMany as

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-09-12
+leanprover/lean4:nightly-2024-09-27