updates

Batteries/Data/HashMap/WF.lean

@@ -315,7 +315,7 @@ theorem WF.mapVal {α β γ} {f : α → β → γ} [BEq α] [Hashable α]
   have ⟨h₁, h₂⟩ := H.out
   simp only [Imp.mapVal, h₁, Buckets.mapVal, WF_iff]; refine ⟨?_, ?_, fun i h => ?_⟩
   · simp only [Buckets.size, Array.map_data, List.map_map]; congr; funext l; simp
-  · simp only [Array.map_data, List.forall_mem_map_iff]
+  · simp only [Array.map_data, List.forall_mem_map]
     simp only [AssocList.toList_mapVal, List.pairwise_map]
     exact fun _ => h₂.1 _
   · simp only [Array.size_map, AssocList.All, Array.getElem_map, AssocList.toList_mapVal,
@@ -361,7 +361,7 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable
   simp only [Array.mapM_eq_mapM_data, bind, StateT.bind, H2, List.map_map, Nat.zero_add, g]
   intro bk sz h e'; cases e'
   refine .mk (by simp [Buckets.size]) ⟨?_, fun i h => ?_⟩
-  · simp only [List.forall_mem_map_iff, List.toList_toAssocList]
+  · simp only [List.forall_mem_map, List.toList_toAssocList]
     refine fun l h => (List.pairwise_reverse.2 ?_).imp (mt PartialEquivBEq.symm)
     have := H.out.2.1 _ h
     rw [← List.pairwise_map (R := (¬ · == ·))] at this ⊢

Batteries/Data/List/Count.lean

@@ -152,7 +152,7 @@ theorem count_le_length (a : α) (l : List α) : count a l ≤ l.length := count
 theorem Sublist.count_le (h : l₁ <+ l₂) (a : α) : count a l₁ ≤ count a l₂ := h.countP_le _
 
 theorem count_le_count_cons (a b : α) (l : List α) : count a l ≤ count a (b :: l) :=
-  (sublist_cons _ _).count_le _
+  (sublist_cons_self _ _).count_le _
 
 theorem count_singleton (a : α) : count a [a] = 1 := by simp
 

Batteries/Data/List/EraseIdx.lean

@@ -50,7 +50,7 @@ theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤
     eraseIdx (l ++ l') k = l ++ eraseIdx l' (k - length l) := by
   rw [eraseIdx_eq_take_drop_succ, eraseIdx_eq_take_drop_succ,
     take_append_eq_append_take, drop_append_eq_append_drop,
-    take_all_of_le hk, drop_eq_nil_of_le (by omega), nil_append, append_assoc]
+    take_of_length_le hk, drop_eq_nil_of_le (by omega), nil_append, append_assoc]
   congr
   omega
 

Batteries/Data/List/Lemmas.lean

@@ -437,10 +437,10 @@ theorem disjoint_of_subset_right (ss : l₂ ⊆ l) (d : Disjoint l₁ l) : Disjo
   fun _ m m₁ => d m (ss m₁)
 
 theorem disjoint_of_disjoint_cons_left {l₁ l₂} : Disjoint (a :: l₁) l₂ → Disjoint l₁ l₂ :=
-disjoint_of_subset_left (subset_cons _ _)
+  disjoint_of_subset_left (subset_cons_self _ _)
 
 theorem disjoint_of_disjoint_cons_right {l₁ l₂} : Disjoint l₁ (a :: l₂) → Disjoint l₁ l₂ :=
-disjoint_of_subset_right (subset_cons _ _)
+  disjoint_of_subset_right (subset_cons_self _ _)
 
 @[simp] theorem disjoint_nil_left (l : List α) : Disjoint [] l := fun a => (not_mem_nil a).elim
 

Batteries/Data/List/Perm.lean

@@ -231,7 +231,7 @@ theorem Subperm.trans {l₁ l₂ l₃ : List α} (s₁₂ : l₁ <+~ l₂) (s₂
   ⟨l₁', p₁, s₁.trans s₂⟩
 
 theorem Subperm.cons_right {α : Type _} {l l' : List α} (x : α) (h : l <+~ l') : l <+~ x :: l' :=
-  h.trans (sublist_cons x l').subperm
+  h.trans (sublist_cons_self x l').subperm
 
 theorem Subperm.length_le {l₁ l₂ : List α} : l₁ <+~ l₂ → length l₁ ≤ length l₂
   | ⟨_l, p, s⟩ => p.length_eq ▸ s.length_le
@@ -368,7 +368,7 @@ theorem perm_append_right_iff {l₁ l₂ : List α} (l) : l₁ ++ l ~ l₂ ++ l
 theorem subperm_cons (a : α) {l₁ l₂ : List α} : a :: l₁ <+~ a :: l₂ ↔ l₁ <+~ l₂ := by
   refine ⟨fun ⟨l, p, s⟩ => ?_, fun ⟨l, p, s⟩ => ⟨a :: l, p.cons a, s.cons₂ _⟩⟩
   match s with
-  | .cons _ s' => exact (p.subperm_left.2 <| (sublist_cons _ _).subperm).trans s'.subperm
+  | .cons _ s' => exact (p.subperm_left.2 <| (sublist_cons_self _ _).subperm).trans s'.subperm
   | .cons₂ _ s' => exact ⟨_, p.cons_inv, s'⟩
 
 /-- Weaker version of `Subperm.cons_left` -/
@@ -409,7 +409,7 @@ theorem Subperm.exists_of_length_lt {l₁ l₂ : List α} (s : l₁ <+~ l₂) (h
   | slnil => cases h
   | cons a s IH =>
     match Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h) with
-    | .inl h => exact (IH h).imp fun a s => s.trans (sublist_cons _ _).subperm
+    | .inl h => exact (IH h).imp fun a s => s.trans (sublist_cons_self _ _).subperm
     | .inr h => exact ⟨a, s.eq_of_length h ▸ .refl _⟩
   | cons₂ b _ IH =>
     exact (IH <| Nat.lt_of_succ_lt_succ h).imp fun a s =>
@@ -461,7 +461,7 @@ theorem subperm_cons_erase (a : α) (l : List α) : l <+~ a :: l.erase a :=
   if h : a ∈ l then
     (perm_cons_erase h).subperm
   else
-    (erase_of_not_mem h).symm ▸ (sublist_cons _ _).subperm
+    (erase_of_not_mem h).symm ▸ (sublist_cons_self _ _).subperm
 
 theorem erase_subperm (a : α) (l : List α) : l.erase a <+~ l := (erase_sublist _ _).subperm
 

Batteries/Data/Nat/Lemmas.lean

@@ -177,10 +177,6 @@ protected alias le_of_le_of_sub_le_sub_left := Nat.le_of_sub_le_sub_left
 
 /-! ### sum -/
 
-@[simp] theorem sum_nil : Nat.sum [] = 0 := rfl
-
-@[simp] theorem sum_cons : Nat.sum (a :: l) = a + Nat.sum l := rfl
-
 @[simp] theorem sum_append : Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂ := by
   induction l₁ <;> simp [*, Nat.add_assoc]