chore: bump to std#260 (#7134)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Alex Keizer <alex@keizer.dev>

Mathlib/Combinatorics/Composition.lean

@@ -690,7 +690,7 @@ theorem length_splitWrtComposition (l : List α) (c : Composition n) :
 theorem map_length_splitWrtCompositionAux {ns : List ℕ} :
     ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns := by
   induction' ns with n ns IH <;> intro l h <;> simp at h
-  · simp
+  · simp [splitWrtCompositionAux]
   have := le_trans (Nat.le_add_right _ _) h
   simp only [splitWrtCompositionAux_cons, this]; dsimp
   rw [length_take, IH] <;> simp [length_drop]

Mathlib/Data/List/Basic.lean

@@ -651,10 +651,6 @@ theorem length_dropLast : ∀ l : List α, length l.dropLast = length l - 1
     simp
 #align list.length_init List.length_dropLast
 
--- Porting note: `rw [dropLast]` in Lean4 generates a goal `(b::l) ≠ []`
--- so we use this lemma instead
-theorem dropLast_cons_cons (a b : α) (l : List α) : dropLast (a::b::l) = a::dropLast (b::l) := rfl
-
 /-! ### getLast -/
 
 @[simp]
@@ -699,7 +695,7 @@ theorem dropLast_append_getLast : ∀ {l : List α} (h : l ≠ []), dropLast l +
   | [], h => absurd rfl h
   | [a], h => rfl
   | a :: b :: l, h => by
-    rw [dropLast_cons_cons, cons_append, getLast_cons (cons_ne_nil _ _)]
+    rw [dropLast_cons₂, cons_append, getLast_cons (cons_ne_nil _ _)]
     congr
     exact dropLast_append_getLast (cons_ne_nil b l)
 #align list.init_append_last List.dropLast_append_getLast
@@ -782,7 +778,7 @@ theorem dropLast_append_getLast? : ∀ {l : List α}, ∀ a ∈ l.getLast?, drop
   | [a], _, rfl => rfl
   | a :: b :: l, c, hc => by
     rw [getLast?_cons_cons] at hc
-    rw [dropLast_cons_cons, cons_append, dropLast_append_getLast? _ hc]
+    rw [dropLast_cons₂, cons_append, dropLast_append_getLast? _ hc]
 #align list.init_append_last' List.dropLast_append_getLast?
 
 theorem getLastI_eq_getLast? [Inhabited α] : ∀ l : List α, l.getLastI = l.getLast?.iget
@@ -1877,9 +1873,6 @@ theorem zipWith_flip (f : α → β → γ) : ∀ as bs, zipWith (flip f) bs as
 
 /-! ### take, drop -/
 
-@[simp]
-theorem take_zero (l : List α) : take 0 l = [] :=
-  rfl
 #align list.take_zero List.take_zero
 
 #align list.take_nil List.take_nil
@@ -2043,7 +2036,7 @@ theorem dropLast_take {n : ℕ} {l : List α} (h : n < l.length) :
 #align list.init_take List.dropLast_take
 
 theorem dropLast_cons_of_ne_nil {α : Type*} {x : α}
-    {l : List α} (h : l ≠ []) : (x :: l).dropLast = x :: l.dropLast := by simp [h]
+    {l : List α} (h : l ≠ []) : (x :: l).dropLast = x :: l.dropLast := by simp [h, dropLast]
 #align list.init_cons_of_ne_nil List.dropLast_cons_of_ne_nil
 
 @[simp]
@@ -2343,26 +2336,9 @@ theorem foldr_ext (f g : α → β → β) (b : β) {l : List α} (H : ∀ a ∈
   simp only [foldr, ih H.2, H.1]
 #align list.foldr_ext List.foldr_ext
 
-@[simp]
-theorem foldl_nil (f : α → β → α) (a : α) : foldl f a [] = a :=
-  rfl
 #align list.foldl_nil List.foldl_nil
-
-@[simp]
-theorem foldl_cons (f : α → β → α) (a : α) (b : β) (l : List β) :
-    foldl f a (b :: l) = foldl f (f a b) l :=
-  rfl
 #align list.foldl_cons List.foldl_cons
-
-@[simp]
-theorem foldr_nil (f : α → β → β) (b : β) : foldr f b [] = b :=
-  rfl
 #align list.foldr_nil List.foldr_nil
-
-@[simp]
-theorem foldr_cons (f : α → β → β) (b : β) (a : α) (l : List α) :
-    foldr f b (a :: l) = f a (foldr f b l) :=
-  rfl
 #align list.foldr_cons List.foldr_cons
 
 #align list.foldl_append List.foldl_append
@@ -2748,18 +2724,9 @@ section FoldlMFoldrM
 
 variable {m : Type v → Type w} [Monad m]
 
-@[simp]
-theorem foldlM_nil (f : β → α → m β) {b} : List.foldlM f b [] = pure b :=
-  rfl
 #align list.mfoldl_nil List.foldlM_nil
-
 -- Porting note: now in std
 #align list.mfoldr_nil List.foldrM_nil
-
-@[simp]
-theorem foldlM_cons {f : β → α → m β} {b a l} :
-    List.foldlM f b (a :: l) = f b a >>= fun b' => List.foldlM f b' l :=
-  rfl
 #align list.mfoldl_cons List.foldlM_cons
 
 /- Porting note: now in std; now assumes an instance of `LawfulMonad m`, so we make everything
@@ -2795,9 +2762,6 @@ end FoldlMFoldrM
 
 /-! ### intersperse -/
 
-@[simp]
-theorem intersperse_nil {α : Type u} (a : α) : intersperse a [] = [] :=
-  rfl
 #align list.intersperse_nil List.intersperse_nil
 
 @[simp]
@@ -3195,18 +3159,13 @@ section find?
 
 variable {p : α → Bool} {l : List α} {a : α}
 
-@[simp]
-theorem find?_nil (p : α → Bool) : find? p [] = none :=
-  rfl
 #align list.find_nil List.find?_nil
 
--- Porting note: List.find? is given @[simp] in Std.Data.List.Init.Lemmas
 -- @[simp]
 -- Later porting note (at time of this lemma moving to Std): removing attribute `nolint simpNF`
 attribute [simp 1100] find?_cons_of_pos
 #align list.find_cons_of_pos List.find?_cons_of_pos
 
--- Porting note: List.find? is given @[simp] in Std.Data.List.Init.Lemmas
 -- @[simp]
 -- Later porting note (at time of this lemma moving to Std): removing attribute `nolint simpNF`
 attribute [simp 1100] find?_cons_of_neg
@@ -3818,15 +3777,8 @@ theorem enum_nil : enum ([] : List α) = [] :=
   rfl
 #align list.enum_nil List.enum_nil
 
-@[simp]
-theorem enumFrom_nil (n : ℕ) : enumFrom n ([] : List α) = [] :=
-  rfl
 #align list.enum_from_nil List.enumFrom_nil
 
-@[simp]
-theorem enumFrom_cons (x : α) (xs : List α) (n : ℕ) :
-    enumFrom n (x :: xs) = (n, x) :: enumFrom (n + 1) xs :=
-  rfl
 #align list.enum_from_cons List.enumFrom_cons
 
 @[simp]

Mathlib/Data/List/Chain.lean

@@ -72,7 +72,7 @@ theorem chain_iff_forall₂ :
   | a, [] => by simp
   | a, b :: l => by
     by_cases h : l = [] <;>
-    simp [@chain_iff_forall₂ b l, *]
+    simp [@chain_iff_forall₂ b l, dropLast, *]
 #align list.chain_iff_forall₂ List.chain_iff_forall₂
 
 theorem chain_append_singleton_iff_forall₂ : Chain R a (l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b]) :=

Mathlib/Data/List/EditDistance/Defs.lean

@@ -251,21 +251,17 @@ theorem suffixLevenshtein_eq_tails_map (xs ys) :
 
 @[simp]
 theorem levenshtein_nil_nil : levenshtein C [] [] = 0 := by
-  simp [levenshtein]
+  simp [levenshtein, suffixLevenshtein]
 
 @[simp]
 theorem levenshtein_nil_cons (y) (ys) :
     levenshtein C [] (y :: ys) = C.insert y + levenshtein C [] ys := by
-  dsimp [levenshtein]
+  dsimp [levenshtein, suffixLevenshtein, impl]
   congr
   rw [List.getLast_eq_get]
   congr
   rw [show (List.length _) = 1 from _]
-  induction ys with
-  | nil => simp
-  | cons y ys ih =>
-    simp only [List.foldr]
-    rw [impl_length] <;> simp [ih]
+  induction ys <;> simp
 
 @[simp]
 theorem levenshtein_cons_nil (x : α) (xs : List α) :

Mathlib/Data/List/Indexes.lean

@@ -167,14 +167,15 @@ theorem mapIdx_eq_enum_map (l : List α) (f : ℕ → α → β) :
   induction' l with hd tl hl generalizing f
   · rfl
   · rw [List.oldMapIdx, List.oldMapIdxCore, List.oldMapIdxCore_eq, hl]
-    simp [enum_eq_zip_range, map_uncurry_zip_eq_zipWith]
+    simp [map, enum_eq_zip_range, map_uncurry_zip_eq_zipWith]
 #align list.map_with_index_eq_enum_map List.mapIdx_eq_enum_map
 
 @[simp]
 theorem mapIdx_cons {α β} (l : List α) (f : ℕ → α → β) (a : α) :
     mapIdx f (a :: l) = f 0 a :: mapIdx (fun i ↦ f (i + 1)) l := by
   simp [mapIdx_eq_enum_map, enum_eq_zip_range, map_uncurry_zip_eq_zipWith,
     range_succ_eq_map, zipWith_map_left]
+  rfl
 #align list.map_with_index_cons List.mapIdx_cons
 
 theorem mapIdx_append {α} (K L : List α) (f : ℕ → α → β) :

Mathlib/Data/List/Zip.lean

@@ -30,52 +30,29 @@ namespace List
 
 variable {α : Type u} {β γ δ ε : Type*}
 
-@[simp]
-theorem zipWith_cons_cons (f : α → β → γ) (a : α) (b : β) (l₁ : List α) (l₂ : List β) :
-    zipWith f (a :: l₁) (b :: l₂) = f a b :: zipWith f l₁ l₂ := rfl
 #align list.zip_with_cons_cons List.zipWith_cons_cons
-
-@[simp]
-theorem zip_cons_cons (a : α) (b : β) (l₁ : List α) (l₂ : List β) :
-    zip (a :: l₁) (b :: l₂) = (a, b) :: zip l₁ l₂ := rfl
 #align list.zip_cons_cons List.zip_cons_cons
-
-@[simp]
-theorem zipWith_nil_left (f : α → β → γ) (l) : zipWith f [] l = [] := rfl
 #align list.zip_with_nil_left List.zipWith_nil_left
-
-theorem zipWith_nil_right (f : α → β → γ) (l) : zipWith f l [] = [] := by simp
 #align list.zip_with_nil_right List.zipWith_nil_right
 
 @[simp]
 theorem zipWith_eq_nil_iff {f : α → β → γ} {l l'} : zipWith f l l' = [] ↔ l = [] ∨ l' = [] := by
   cases l <;> cases l' <;> simp
 #align list.zip_with_eq_nil_iff List.zipWith_eq_nil_iff
 
-@[simp]
-theorem zip_nil_left (l : List α) : zip ([] : List β) l = [] :=
-  rfl
 #align list.zip_nil_left List.zip_nil_left
-
-@[simp]
-theorem zip_nil_right (l : List α) : zip l ([] : List β) = [] :=
-  zipWith_nil_right _ l
 #align list.zip_nil_right List.zip_nil_right
 
 @[simp]
 theorem zip_swap : ∀ (l₁ : List α) (l₂ : List β), (zip l₁ l₂).map Prod.swap = zip l₂ l₁
-  | [], l₂ => (zip_nil_right _).symm
+  | [], l₂ => zip_nil_right.symm
   | l₁, [] => by rw [zip_nil_right]; rfl
   | a :: l₁, b :: l₂ => by
     simp only [zip_cons_cons, map_cons, zip_swap l₁ l₂, Prod.swap_prod_mk]
 #align list.zip_swap List.zip_swap
 
 #align list.length_zip_with List.length_zipWith
 
-@[simp]
-theorem length_zip :
-    ∀ (l₁ : List α) (l₂ : List β), length (zip l₁ l₂) = min (length l₁) (length l₂) :=
-  length_zipWith _
 #align list.length_zip List.length_zip
 
 theorem all₂_zipWith {f : α → β → γ} {p : γ → Prop} :
@@ -199,13 +176,8 @@ theorem map_snd_zip :
     rw [map_snd_zip as bs h]
 #align list.map_snd_zip List.map_snd_zip
 
-@[simp]
-theorem unzip_nil : unzip (@nil (α × β)) = ([], []) := rfl
 #align list.unzip_nil List.unzip_nil
 
-@[simp]
-theorem unzip_cons (a : α) (b : β) (l : List (α × β)) :
-    unzip ((a, b) :: l) = (a :: (unzip l).1, b :: (unzip l).2) := rfl
 #align list.unzip_cons List.unzip_cons
 
 theorem unzip_eq_map : ∀ l : List (α × β), unzip l = (l.map Prod.fst, l.map Prod.snd)
@@ -268,7 +240,7 @@ theorem map_prod_right_eq_zip {l : List α} (f : α → β) :
 
 theorem zipWith_comm (f : α → β → γ) :
     ∀ (la : List α) (lb : List β), zipWith f la lb = zipWith (fun b a => f a b) lb la
-  | [], _ => (List.zipWith_nil_right _ _).symm
+  | [], _ => List.zipWith_nil_right.symm
   | _ :: _, [] => rfl
   | _ :: as, _ :: bs => congr_arg _ (zipWith_comm f as bs)
 #align list.zip_with_comm List.zipWith_comm

Mathlib/Data/UnionFind.lean

@@ -150,7 +150,7 @@ theorem setParent {arr : Array (UFNode α)} {n} {m : UFModel n} (hm : m.Models a
   (m.setParent i j H).Models (arr.set ⟨i.1, hi⟩ x) :=
   ⟨hm.1.set
       (fun k (h : (k:ℕ) ≠ i) ↦ by simp [UFModel.setParent, h.symm])
-      (fun h ↦ by simp [UFModel.setParent, hp]),
+      (fun _ ↦ by simp [UFModel.setParent, hp]),
     hm.2.set (fun _ _ ↦ rfl) (fun _ ↦ hrk.trans $ hm.2.get_eq ..)⟩
 
 end UFModel.Models
@@ -277,7 +277,7 @@ def link (self : UnionFind α) (x y : Fin self.size)
       (by simpa [← hm.parent_eq'] using yroot), ?_⟩
     let parent (i : Fin n) := (if x.1 = i then y else m.parent i).1
     have : UFModel.Agrees arr₁ (·.parent) parent :=
-      hm.1.set (fun i h ↦ by simp; rw [if_neg h.symm]) (fun h ↦ by simp)
+      hm.1.set (fun i h ↦ by simp; rw [if_neg h.symm]) (fun _ ↦ by simp)
     have H1 : UFModel.Agrees arr₂ (·.parent) parent := by
       simp; split
       · exact this.set (fun i h ↦ by simp [h.symm]) (fun h ↦ by simp [ne, hm.parent_eq'])

Mathlib/Data/Vector/Basic.lean

@@ -393,7 +393,7 @@ theorem scanl_get (i : Fin n) :
   · exact i.elim0
   induction' n with n hn generalizing b
   · have i0 : i = 0 := Fin.eq_zero _
-    simp [scanl_singleton, i0, get_zero]; simp [get_eq_get]
+    simp [scanl_singleton, i0, get_zero]; simp [get_eq_get, List.get]
   · rw [← cons_head_tail v, scanl_cons, get_cons_succ]
     refine' Fin.cases _ _ i
     · simp only [get_zero, scanl_head, Fin.castSucc_zero, head_cons]

lake-manifest.json

@@ -2,14 +2,6 @@
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "538a09123ed1080bb7227fb5d133abe0e2183b8d",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": false}},
-  {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
     "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
@@ -40,5 +32,13 @@
     "opts": {},
     "name": "proofwidgets",
     "inputRev?": "v0.0.16",
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
     "inherited": false}}],
  "name": "mathlib"}