chore: rename List.bind and Array.concatMap to flatMap

fix

src/Init/Core.lean

@@ -1864,8 +1864,7 @@ section
 variable {α : Type u}
 variable (r : α → α → Prop)
 
-instance Quotient.decidableEq {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)]
-    : DecidableEq (Quotient s) :=
+instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
   fun (q₁ q₂ : Quotient s) =>
     Quotient.recOnSubsingleton₂ q₁ q₂
       fun a₁ a₂ =>

src/Init/Data/Array/Basic.lean

@@ -607,13 +607,17 @@ protected def appendList (as : Array α) (bs : List α) : Array α :=
 instance : HAppend (Array α) (List α) (Array α) := ⟨Array.appendList⟩
 
 @[inline]
-def concatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β) :=
+def flatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β) :=
   as.foldlM (init := empty) fun bs a => do return bs ++ (← f a)
 
+@[deprecated concatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
+
 @[inline]
-def concatMap (f : α → Array β) (as : Array α) : Array β :=
+def flatMap (f : α → Array β) (as : Array α) : Array β :=
   as.foldl (init := empty) fun bs a => bs ++ f a
 
+@[deprecated flatMap (since := "2024-10-16")] abbrev concatMap := @flatMap
+
 /-- Joins array of array into a single array.
 
 `flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` = `#[a₁, a₂, ⋯, b₁, b₂, ⋯]`

src/Init/Data/Array/Lemmas.lean

@@ -242,14 +242,17 @@ abbrev map_data := @toList_map
   cases arr
   simp
 
-theorem foldl_toList_eq_bind (l : List α) (acc : Array β)
+theorem foldl_toList_eq_flatMap (l : List α) (acc : Array β)
     (F : Array β → α → Array β) (G : α → List β)
     (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
-    (l.foldl F acc).toList = acc.toList ++ l.bind G := by
-  induction l generalizing acc <;> simp [*, List.bind]
+    (l.foldl F acc).toList = acc.toList ++ l.flatMap G := by
+  induction l generalizing acc <;> simp [*, List.flatMap]
 
-@[deprecated foldl_toList_eq_bind (since := "2024-09-09")]
-abbrev foldl_data_eq_bind := @foldl_toList_eq_bind
+@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
+abbrev foldl_toList_eq_bind := @foldl_toList_eq_flatMap
+
+@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
+abbrev foldl_data_eq_bind := @foldl_toList_eq_flatMap
 
 theorem foldl_toList_eq_map (l : List α) (acc : Array β) (G : α → β) :
     (l.foldl (fun acc a => acc.push (G a)) acc).toList = acc.toList ++ l.map G := by

src/Init/Data/BitVec/Lemmas.lean

@@ -286,19 +286,6 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 
 @[simp] theorem getMsbD_zero : (0#w).getMsbD i = false := by simp [getMsbD]
 
-@[simp] theorem getLsbD_one : (1#w).getLsbD i = (decide (0 < w) && decide (i = 0)) := by
-  simp only [getLsbD, toNat_ofNat, Nat.testBit_mod_two_pow]
-  by_cases h : i = 0
-    <;> simp [h, Nat.testBit_to_div_mod, Nat.div_eq_of_lt]
-
-@[simp] theorem getElem_one (h : i < w) : (1#w)[i] = decide (i = 0) := by
-  simp [← getLsbD_eq_getElem, getLsbD_one, h, show 0 < w by omega]
-
-/-- The msb at index `w-1` is the least significant bit, and is true when the width is nonzero. -/
-@[simp] theorem getMsbD_one : (1#w).getMsbD i = (decide (i = w - 1) && decide (0 < w)) := by
-  simp only [getMsbD]
-  by_cases h : 0 < w <;> by_cases h' : i = w - 1 <;> simp [h, h'] <;> omega
-
 @[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
   Nat.mod_eq_of_lt x.isLt
 
@@ -360,10 +347,6 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
 
-@[simp] theorem msb_one : (1#w).msb = decide (w = 1) := by
-  simp [BitVec.msb, getMsbD_one, ← Bool.decide_and]
-  omega
-
 theorem msb_eq_getLsbD_last (x : BitVec w) :
     x.msb = x.getLsbD (w - 1) := by
   simp only [BitVec.msb, getMsbD]
@@ -2090,11 +2073,6 @@ theorem sub_eq_xor {a b : BitVec 1} : a - b = a ^^^ b := by
   have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
   rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
 
-@[simp]
-theorem sub_eq_self {x : BitVec 1} : -x = x := by
-  have ha : x = 0 ∨ x = 1 := eq_zero_or_eq_one _
-  rcases ha with h | h <;> simp [h]
-
 theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
   rcases w with _ | w
   · apply Subsingleton.elim
@@ -2363,24 +2341,6 @@ theorem toNat_sdiv {x y : BitVec w} : (x.sdiv y).toNat =
   simp only [sdiv_eq, toNat_udiv]
   by_cases h : x.msb <;> by_cases h' : y.msb <;> simp [h, h']
 
-@[simp]
-theorem zero_sdiv {x : BitVec w} : (0#w).sdiv x = 0#w := by
-  simp only [sdiv_eq]
-  rcases x.msb with msb | msb <;> simp
-
-@[simp]
-theorem sdiv_zero {x : BitVec n} : x.sdiv 0#n = 0#n := by
-  simp only [sdiv_eq, msb_zero]
-  rcases x.msb with msb | msb <;> apply eq_of_toNat_eq <;> simp
-
-@[simp]
-theorem sdiv_one {x : BitVec w} : x.sdiv 1#w = x := by
-  simp only [sdiv_eq]
-  · by_cases h : w = 1
-    · subst h
-      rcases x.msb with msb | msb <;> simp
-    · rcases x.msb with msb | msb <;> simp [h]
-
 theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
   have hx : x = 0#1 ∨ x = 1#1 := by bv_omega
   have hy : y = 0#1 ∨ y = 1#1 := by bv_omega
@@ -2389,13 +2349,9 @@ theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
       rfl
 
 @[simp]
-theorem sdiv_self {x : BitVec w} :
-    x.sdiv x = if x == 0#w then 0#w else 1#w := by
-  simp [sdiv_eq]
-  · by_cases h : w = 1
-    · subst h
-      rcases x.msb with msb | msb <;> simp
-    · rcases x.msb with msb | msb <;> simp [h]
+theorem sdiv_zero {x : BitVec n} : x.sdiv 0#n = 0#n := by
+  simp only [sdiv_eq, msb_zero]
+  rcases x.msb with msb | msb <;> apply eq_of_toNat_eq <;> simp
 
 /-! ### smod -/
 
@@ -2697,6 +2653,14 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
   apply eq_of_toNat_eq
   simp
 
+@[simp]
+theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by
+  rw [← twoPow_zero, getLsbD_twoPow]
+
+@[simp]
+theorem getElem_one {w i : Nat} (h : i < w) : (1#w)[i] = decide (i = 0) := by
+  rw [← twoPow_zero, getElem_twoPow]
+
 theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
     x <<< n = x * (BitVec.twoPow w n) := by
   ext i
@@ -2716,6 +2680,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
 @[simp] theorem zero_concat_true : concat 0#w true = 1#(w + 1) := by
   ext
   simp [getLsbD_concat]
+  omega
 
 /- ### setWidth, setWidth, and bitwise operations -/
 
@@ -2756,7 +2721,7 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
   ext i
   simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_ofBool,
     Bool.true_and]
-  by_cases h : ((i : Nat) = 0) <;> simp [h] <;> omega
+  by_cases h : (0 = (i : Nat)) <;> simp [h] <;> omega
 
 @[simp]
 theorem replicate_zero_eq {x : BitVec w} : x.replicate 0 = 0#0 := by

src/Init/Data/List/Attach.lean

@@ -639,14 +639,16 @@ and simplifies these to the function directly taking the value.
   | nil => simp
   | cons a l ih => simp [ih, hf, filterMap_cons]
 
-@[simp] theorem bind_subtype {p : α → Prop} {l : List { x // p x }}
+@[simp] theorem flatMap_subtype {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → List β} {g : α → List β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
-    (l.bind f) = l.unattach.bind g := by
+    (l.flatMap f) = l.unattach.flatMap g := by
   unfold unattach
   induction l with
   | nil => simp
   | cons a l ih => simp [ih, hf]
 
+@[deprecated flatMap_subtype (since := "2024-10-16")] abbrev bind_subtype := @flatMap_subtype
+
 @[simp] theorem unattach_filter {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
     (l.filter f).unattach = l.unattach.filter g := by

src/Init/Data/List/Basic.lean

@@ -563,23 +563,30 @@ def flatten : List (List α) → List α
 /-- `pure x = [x]` is the `pure` operation of the list monad. -/
 @[inline] protected def pure {α : Type u} (a : α) : List α := [a]
 
-/-! ### bind -/
+/-! ### flatMap -/
 
 /--
-`bind xs f` is the bind operation of the list monad. It applies `f` to each element of `xs`
+`flatMap xs f` applies `f` to each element of `xs`
 to get a list of lists, and then concatenates them all together.
 * `[2, 3, 2].bind range = [0, 1, 0, 1, 2, 0, 1]`
 -/
-@[inline] protected def bind {α : Type u} {β : Type v} (a : List α) (b : α → List β) : List β := flatten (map b a)
+@[inline] def flatMap {α : Type u} {β : Type v} (a : List α) (b : α → List β) : List β := flatten (map b a)
 
-@[simp] theorem bind_nil (f : α → List β) : List.bind [] f = [] := by simp [flatten, List.bind]
-@[simp] theorem bind_cons x xs (f : α → List β) :
-  List.bind (x :: xs) f = f x ++ List.bind xs f := by simp [flatten, List.bind]
+@[simp] theorem flatMap_nil (f : α → List β) : List.flatMap [] f = [] := by simp [flatten, List.flatMap]
+@[simp] theorem flatMap_cons x xs (f : α → List β) :
+  List.flatMap (x :: xs) f = f x ++ List.flatMap xs f := by simp [flatten, List.flatMap]
 
 set_option linter.missingDocs false in
-@[deprecated bind_nil (since := "2024-06-15")] abbrev nil_bind := @bind_nil
+@[deprecated flatMap (since := "2024-10-16")] abbrev bind := @flatMap
 set_option linter.missingDocs false in
-@[deprecated bind_cons (since := "2024-06-15")] abbrev cons_bind := @bind_cons
+@[deprecated flatMap_nil (since := "2024-10-16")] abbrev nil_flatMap := @flatMap_nil
+set_option linter.missingDocs false in
+@[deprecated flatMap_cons (since := "2024-10-16")] abbrev cons_flatMap := @flatMap_cons
+
+set_option linter.missingDocs false in
+@[deprecated flatMap_nil (since := "2024-06-15")] abbrev nil_bind := @flatMap_nil
+set_option linter.missingDocs false in
+@[deprecated flatMap_cons (since := "2024-06-15")] abbrev cons_bind := @flatMap_cons
 
 /-! ### replicate -/
 
@@ -1398,17 +1405,8 @@ def unzip : List (α × β) → List α × List β
 
 /-! ## Ranges and enumeration -/
 
-/-- Sum of a list.
-
-`List.sum [a, b, c] = a + (b + (c + 0))` -/
-def sum {α} [Add α] [Zero α] : List α → α :=
-  foldr (· + ·) 0
-
-@[simp] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
-@[simp] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
-
 /-- Sum of a list of natural numbers. -/
--- We intend to subsequently deprecate this in favor of `List.sum`.
+-- This is not in the `List` namespace as later `List.sum` will be defined polymorphically.
 protected def _root_.Nat.sum (l : List Nat) : Nat := l.foldr (·+·) 0
 
 @[simp] theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl

src/Init/Data/List/Count.lean

@@ -156,7 +156,7 @@ theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : List α)
   simp (config := { contextual := true }) [Option.getD_eq_iff, Option.isSome_eq_isSome]
 
 @[simp] theorem countP_flatten (l : List (List α)) :
-    countP p l.flatten = (l.map (countP p)).sum := by
+    countP p l.flatten = Nat.sum (l.map (countP p)) := by
   simp only [countP_eq_length_filter, filter_flatten]
   simp [countP_eq_length_filter']
 
@@ -232,7 +232,7 @@ theorem count_singleton (a b : α) : count a [b] = if b == a then 1 else 0 := by
 @[simp] theorem count_append (a : α) : ∀ l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
   countP_append _
 
-theorem count_flatten (a : α) (l : List (List α)) : count a l.flatten = (l.map (count a)).sum := by
+theorem count_flatten (a : α) (l : List (List α)) : count a l.flatten = Nat.sum (l.map (count a)) := by
   simp only [count_eq_countP, countP_flatten, count_eq_countP']
 
 @[deprecated count_flatten (since := "2024-10-14")] abbrev count_join := @count_flatten

src/Init/Data/List/Find.lean

@@ -378,14 +378,18 @@ theorem find?_flatten_eq_some {xs : List (List α)} {p : α → Bool} {a : α} :
     · exact h₁ l ml a m
     · exact h₂ a m
 
-@[simp] theorem find?_bind (xs : List α) (f : α → List β) (p : β → Bool) :
-    (xs.bind f).find? p = xs.findSome? (fun x => (f x).find? p) := by
-  simp [bind_def, findSome?_map]; rfl
+@[simp] theorem find?_flatMap (xs : List α) (f : α → List β) (p : β → Bool) :
+    (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
+  simp [flatMap_def, findSome?_map]; rfl
 
-theorem find?_bind_eq_none {xs : List α} {f : α → List β} {p : β → Bool} :
-    (xs.bind f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
+@[deprecated find?_flatMap (since := "2024-10-16")] abbrev find?_bind := @find?_flatMap
+
+theorem find?_flatMap_eq_none {xs : List α} {f : α → List β} {p : β → Bool} :
+    (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
+@[deprecated find?_flatMap_eq_none (since := "2024-10-16")] abbrev find?_bind_eq_none := @find?_flatMap_eq_none
+
 theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   cases n
   · simp
@@ -789,7 +793,7 @@ theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
 theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
     l.flatten.findIdx? p =
       (l.findIdx? (·.any p)).map
-        fun i => ((l.take i).map List.length).sum +
+        fun i => Nat.sum ((l.take i).map List.length) +
           (l[i]?.map fun xs => xs.findIdx p).getD 0 := by
   induction l with
   | nil => simp

src/Init/Data/List/Impl.lean

@@ -93,29 +93,29 @@ The following operations are given `@[csimp]` replacements below:
 @[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
   funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_toList, -Array.size_toArray]
 
-/-! ### bind  -/
+/-! ### flatMap  -/
 
-/-- Tail recursive version of `List.bind`. -/
-@[inline] def bindTR (as : List α) (f : α → List β) : List β := go as #[] where
-  /-- Auxiliary for `bind`: `bind.go f as = acc.toList ++ bind f as` -/
+/-- Tail recursive version of `List.flatMap`. -/
+@[inline] def flatMapTR (as : List α) (f : α → List β) : List β := go as #[] where
+  /-- Auxiliary for `flatMap`: `flatMap.go f as = acc.toList ++ bind f as` -/
   @[specialize] go : List α → Array β → List β
   | [], acc => acc.toList
   | x::xs, acc => go xs (acc ++ f x)
 
-@[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by
+@[csimp] theorem flatMap_eq_flatMapTR : @List.flatMap = @flatMapTR := by
   funext α β as f
-  let rec go : ∀ as acc, bindTR.go f as acc = acc.toList ++ as.bind f
-    | [], acc => by simp [bindTR.go, bind]
-    | x::xs, acc => by simp [bindTR.go, bind, go xs]
+  let rec go : ∀ as acc, flatMapTR.go f as acc = acc.toList ++ as.flatMap f
+    | [], acc => by simp [flatMapTR.go, flatMap]
+    | x::xs, acc => by simp [flatMapTR.go, flatMap, go xs]
   exact (go as #[]).symm
 
 /-! ### flatten -/
 
 /-- Tail recursive version of `List.flatten`. -/
-@[inline] def flattenTR (l : List (List α)) : List α := bindTR l id
+@[inline] def flattenTR (l : List (List α)) : List α := flatMapTR l id
 
 @[csimp] theorem flatten_eq_flattenTR : @flatten = @flattenTR := by
-  funext α l; rw [← List.bind_id, List.bind_eq_bindTR]; rfl
+  funext α l; rw [← List.flatMap_id, List.flatMap_eq_flatMapTR]; rfl
 
 /-! ## Sublists -/
 

src/Init/Data/List/Lemmas.lean

@@ -2070,7 +2070,8 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = concat L b
 
 /-! ### flatten -/
 
-@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = (L.map length).sum := by
+
+@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = Nat.sum (L.map length) := by
   induction L with
   | nil => rfl
   | cons =>
@@ -2097,8 +2098,8 @@ theorem forall_mem_flatten {p : α → Prop} {L : List (List α)} :
   simp only [mem_flatten, forall_exists_index, and_imp]
   constructor <;> (intros; solve_by_elim)
 
-theorem flatten_eq_bind {L : List (List α)} : flatten L = L.bind id := by
-  induction L <;> simp [List.bind]
+theorem flatten_eq_flatMap {L : List (List α)} : flatten L = L.flatMap id := by
+  induction L <;> simp [List.flatMap]
 
 theorem head?_flatten {L : List (List α)} : (flatten L).head? = L.findSome? fun l => l.head? := by
   induction L with
@@ -2215,86 +2216,86 @@ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
       obtain ⟨rfl, h⟩ := append_inj h₁ h₂
       exact ⟨rfl, h, h₃⟩
 
-/-! ### bind -/
+/-! ### flatMap -/
 
-theorem bind_def (l : List α) (f : α → List β) : l.bind f = flatten (map f l) := by rfl
+theorem flatMap_def (l : List α) (f : α → List β) : l.flatMap f = flatten (map f l) := by rfl
 
-@[simp] theorem bind_id (l : List (List α)) : List.bind l id = l.flatten := by simp [bind_def]
+@[simp] theorem flatMap_id (l : List (List α)) : List.flatMap l id = l.flatten := by simp [flatMap_def]
 
-@[simp] theorem mem_bind {f : α → List β} {b} {l : List α} : b ∈ l.bind f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
-  simp [bind_def, mem_flatten]
+@[simp] theorem mem_flatMap {f : α → List β} {b} {l : List α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
+  simp [flatMap_def, mem_flatten]
   exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩
 
-theorem exists_of_mem_bind {b : β} {l : List α} {f : α → List β} :
-    b ∈ l.bind f → ∃ a, a ∈ l ∧ b ∈ f a := mem_bind.1
+theorem exists_of_mem_flatMap {b : β} {l : List α} {f : α → List β} :
+    b ∈ l.flatMap f → ∃ a, a ∈ l ∧ b ∈ f a := mem_flatMap.1
 
-theorem mem_bind_of_mem {b : β} {l : List α} {f : α → List β} {a} (al : a ∈ l) (h : b ∈ f a) :
-    b ∈ l.bind f := mem_bind.2 ⟨a, al, h⟩
+theorem mem_flatMap_of_mem {b : β} {l : List α} {f : α → List β} {a} (al : a ∈ l) (h : b ∈ f a) :
+    b ∈ l.flatMap f := mem_flatMap.2 ⟨a, al, h⟩
 
 @[simp]
-theorem bind_eq_nil_iff {l : List α} {f : α → List β} : List.bind l f = [] ↔ ∀ x ∈ l, f x = [] :=
+theorem flatMap_eq_nil_iff {l : List α} {f : α → List β} : List.flatMap l f = [] ↔ ∀ x ∈ l, f x = [] :=
   flatten_eq_nil_iff.trans <| by
     simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
 
-@[deprecated bind_eq_nil_iff (since := "2024-09-05")] abbrev bind_eq_nil := @bind_eq_nil_iff
+@[deprecated flatMap_eq_nil_iff (since := "2024-09-05")] abbrev bind_eq_nil := @flatMap_eq_nil_iff
 
-theorem forall_mem_bind {p : β → Prop} {l : List α} {f : α → List β} :
-    (∀ (x) (_ : x ∈ l.bind f), p x) ↔ ∀ (a) (_ : a ∈ l) (b) (_ : b ∈ f a), p b := by
-  simp only [mem_bind, forall_exists_index, and_imp]
+theorem forall_mem_flatMap {p : β → Prop} {l : List α} {f : α → List β} :
+    (∀ (x) (_ : x ∈ l.flatMap f), p x) ↔ ∀ (a) (_ : a ∈ l) (b) (_ : b ∈ f a), p b := by
+  simp only [mem_flatMap, forall_exists_index, and_imp]
   constructor <;> (intros; solve_by_elim)
 
-theorem bind_singleton (f : α → List β) (x : α) : [x].bind f = f x :=
+theorem flatMap_singleton (f : α → List β) (x : α) : [x].flatMap f = f x :=
   append_nil (f x)
 
-@[simp] theorem bind_singleton' (l : List α) : (l.bind fun x => [x]) = l := by
+@[simp] theorem flatMap_singleton' (l : List α) : (l.flatMap fun x => [x]) = l := by
   induction l <;> simp [*]
 
-theorem head?_bind {l : List α} {f : α → List β} :
-    (l.bind f).head? = l.findSome? fun a => (f a).head? := by
+theorem head?_flatMap {l : List α} {f : α → List β} :
+    (l.flatMap f).head? = l.findSome? fun a => (f a).head? := by
   induction l with
   | nil => rfl
   | cons =>
     simp only [findSome?_cons]
     split <;> simp_all
 
-@[simp] theorem bind_append (xs ys : List α) (f : α → List β) :
-    (xs ++ ys).bind f = xs.bind f ++ ys.bind f := by
-  induction xs; {rfl}; simp_all [bind_cons, append_assoc]
+@[simp] theorem flatMap_append (xs ys : List α) (f : α → List β) :
+    (xs ++ ys).flatMap f = xs.flatMap f ++ ys.flatMap f := by
+  induction xs; {rfl}; simp_all [flatMap_cons, append_assoc]
 
-@[deprecated bind_append (since := "2024-07-24")] abbrev append_bind := @bind_append
+@[deprecated flatMap_append (since := "2024-07-24")] abbrev append_bind := @flatMap_append
 
-theorem bind_assoc {α β} (l : List α) (f : α → List β) (g : β → List γ) :
-    (l.bind f).bind g = l.bind fun x => (f x).bind g := by
+theorem flatMap_assoc {α β} (l : List α) (f : α → List β) (g : β → List γ) :
+    (l.flatMap f).flatMap g = l.flatMap fun x => (f x).flatMap g := by
   induction l <;> simp [*]
 
-theorem map_bind (f : β → γ) (g : α → List β) :
-    ∀ l : List α, (l.bind g).map f = l.bind fun a => (g a).map f
+theorem map_flatMap (f : β → γ) (g : α → List β) :
+    ∀ l : List α, (l.flatMap g).map f = l.flatMap fun a => (g a).map f
   | [] => rfl
-  | a::l => by simp only [bind_cons, map_append, map_bind _ _ l]
+  | a::l => by simp only [flatMap_cons, map_append, map_flatMap _ _ l]
 
-theorem bind_map (f : α → β) (g : β → List γ) (l : List α) :
-    (map f l).bind g = l.bind (fun a => g (f a)) := by
-  induction l <;> simp [bind_cons, *]
+theorem flatMap_map (f : α → β) (g : β → List γ) (l : List α) :
+    (map f l).flatMap g = l.flatMap (fun a => g (f a)) := by
+  induction l <;> simp [flatMap_cons, *]
 
-theorem map_eq_bind {α β} (f : α → β) (l : List α) : map f l = l.bind fun x => [f x] := by
+theorem map_eq_flatMap {α β} (f : α → β) (l : List α) : map f l = l.flatMap fun x => [f x] := by
   simp only [← map_singleton]
-  rw [← bind_singleton' l, map_bind, bind_singleton']
+  rw [← flatMap_singleton' l, map_flatMap, flatMap_singleton']
 
-theorem filterMap_bind {β γ} (l : List α) (g : α → List β) (f : β → Option γ) :
-    (l.bind g).filterMap f = l.bind fun a => (g a).filterMap f := by
+theorem filterMap_flatMap {β γ} (l : List α) (g : α → List β) (f : β → Option γ) :
+    (l.flatMap g).filterMap f = l.flatMap fun a => (g a).filterMap f := by
   induction l <;> simp [*]
 
-theorem filter_bind (l : List α) (g : α → List β) (f : β → Bool) :
-    (l.bind g).filter f = l.bind fun a => (g a).filter f := by
+theorem filter_flatMap (l : List α) (g : α → List β) (f : β → Bool) :
+    (l.flatMap g).filter f = l.flatMap fun a => (g a).filter f := by
   induction l <;> simp [*]
 
-theorem bind_eq_foldl (f : α → List β) (l : List α) :
-    l.bind f = l.foldl (fun acc a => acc ++ f a) [] := by
-  suffices ∀ l', l' ++ l.bind f = l.foldl (fun acc a => acc ++ f a) l' by simpa using this []
+theorem flatMap_eq_foldl (f : α → List β) (l : List α) :
+    l.flatMap f = l.foldl (fun acc a => acc ++ f a) [] := by
+  suffices ∀ l', l' ++ l.flatMap f = l.foldl (fun acc a => acc ++ f a) l' by simpa using this []
   intro l'
   induction l generalizing l'
   · simp
-  · next ih => rw [bind_cons, ← append_assoc, ih, foldl_cons]
+  · next ih => rw [flatMap_cons, ← append_assoc, ih, foldl_cons]
 
 /-! ### replicate -/
 
@@ -2484,10 +2485,10 @@ theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
     simp only [replicate_succ, flatten_cons, ih, append_replicate_replicate, replicate_inj, or_true,
       and_true, add_one_mul, Nat.add_comm]
 
-theorem bind_replicate {β} (f : α → List β) : (replicate n a).bind f = (replicate n (f a)).flatten := by
+theorem flatMap_replicate {β} (f : α → List β) : (replicate n a).flatMap f = (replicate n (f a)).flatten := by
   induction n with
   | zero => simp
-  | succ n ih => simp only [replicate_succ, bind_cons, ih, flatten_cons]
+  | succ n ih => simp only [replicate_succ, flatMap_cons, ih, flatten_cons]
 
 @[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
   cases n <;> simp [replicate_succ]
@@ -2672,10 +2673,10 @@ theorem flatten_reverse (L : List (List α)) :
     L.reverse.flatten = (L.map reverse).flatten.reverse := by
   induction L <;> simp_all
 
-theorem reverse_bind {β} (l : List α) (f : α → List β) : (l.bind f).reverse = l.reverse.bind (reverse ∘ f) := by
+theorem reverse_flatMap {β} (l : List α) (f : α → List β) : (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by
   induction l <;> simp_all
 
-theorem bind_reverse {β} (l : List α) (f : α → List β) : (l.reverse.bind f) = (l.bind (reverse ∘ f)).reverse := by
+theorem flatMap_reverse {β} (l : List α) (f : α → List β) : (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by
   induction l <;> simp_all
 
 @[simp] theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
@@ -2783,15 +2784,15 @@ theorem getLast_filterMap_of_eq_some {f : α → Option β} {l : List α} {w : l
   rw [head_filterMap_of_eq_some (by simp_all)]
   simp_all
 
-theorem getLast?_bind {L : List α} {f : α → List β} :
-    (L.bind f).getLast? = L.reverse.findSome? fun a => (f a).getLast? := by
-  simp only [← head?_reverse, reverse_bind]
-  rw [head?_bind]
+theorem getLast?_flatMap {L : List α} {f : α → List β} :
+    (L.flatMap f).getLast? = L.reverse.findSome? fun a => (f a).getLast? := by
+  simp only [← head?_reverse, reverse_flatMap]
+  rw [head?_flatMap]
   rfl
 
 theorem getLast?_flatten {L : List (List α)} :
     (flatten L).getLast? = L.reverse.findSome? fun l => l.getLast? := by
-  simp [← bind_id, getLast?_bind]
+  simp [← flatMap_id, getLast?_flatMap]
 
 theorem getLast?_replicate (a : α) (n : Nat) : (replicate n a).getLast? = if n = 0 then none else some a := by
   simp only [← head?_reverse, reverse_replicate, head?_replicate]
@@ -3300,12 +3301,12 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
 
 @[deprecated all_flatten (since := "2024-10-14")] abbrev all_join := @all_flatten
 
-@[simp] theorem any_bind {l : List α} {f : α → List β} :
-    (l.bind f).any p = l.any fun a => (f a).any p := by
+@[simp] theorem any_flatMap {l : List α} {f : α → List β} :
+    (l.flatMap f).any p = l.any fun a => (f a).any p := by
   induction l <;> simp_all
 
-@[simp] theorem all_bind {l : List α} {f : α → List β} :
-    (l.bind f).all p = l.all fun a => (f a).all p := by
+@[simp] theorem all_flatMap {l : List α} {f : α → List β} :
+    (l.flatMap f).all p = l.all fun a => (f a).all p := by
   induction l <;> simp_all
 
 @[simp] theorem any_reverse {l : List α} : l.reverse.any f = l.any f := by
@@ -3345,7 +3346,7 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
 @[deprecated exists_of_mem_flatten (since := "2024-10-14")] abbrev exists_of_mem_join := @exists_of_mem_flatten
 @[deprecated mem_flatten_of_mem (since := "2024-10-14")] abbrev mem_join_of_mem := @mem_flatten_of_mem
 @[deprecated forall_mem_flatten (since := "2024-10-14")] abbrev forall_mem_join := @forall_mem_flatten
-@[deprecated flatten_eq_bind (since := "2024-10-14")] abbrev join_eq_bind := @flatten_eq_bind
+@[deprecated flatten_eq_flatMap (since := "2024-10-14")] abbrev join_eq_bind := @flatten_eq_flatMap
 @[deprecated head?_flatten (since := "2024-10-14")] abbrev head?_join := @head?_flatten
 @[deprecated foldl_flatten (since := "2024-10-14")] abbrev foldl_join := @foldl_flatten
 @[deprecated foldr_flatten (since := "2024-10-14")] abbrev foldr_join := @foldr_flatten
@@ -3372,5 +3373,30 @@ theorem join_map_filter (p : α → Bool) (l : List (List α)) :
 @[deprecated reverse_flatten (since := "2024-10-14")] abbrev reverse_join := @reverse_flatten
 @[deprecated flatten_reverse (since := "2024-10-14")] abbrev join_reverse := @flatten_reverse
 @[deprecated getLast?_flatten (since := "2024-10-14")] abbrev getLast?_join := @getLast?_flatten
+@[deprecated flatten_eq_flatMap (since := "2024-10-16")] abbrev flatten_eq_bind := @flatten_eq_flatMap
+@[deprecated flatMap_def (since := "2024-10-16")] abbrev bind_def := @flatMap_def
+@[deprecated flatMap_id (since := "2024-10-16")] abbrev bind_id := @flatMap_id
+@[deprecated mem_flatMap (since := "2024-10-16")] abbrev mem_bind := @mem_flatMap
+@[deprecated exists_of_mem_flatMap (since := "2024-10-16")] abbrev exists_of_mem_bind := @exists_of_mem_flatMap
+@[deprecated mem_flatMap_of_mem (since := "2024-10-16")] abbrev mem_bind_of_mem := @mem_flatMap_of_mem
+@[deprecated flatMap_eq_nil_iff (since := "2024-10-16")] abbrev bind_eq_nil_iff := @flatMap_eq_nil_iff
+@[deprecated forall_mem_flatMap (since := "2024-10-16")] abbrev forall_mem_bind := @forall_mem_flatMap
+@[deprecated flatMap_singleton (since := "2024-10-16")] abbrev bind_singleton := @flatMap_singleton
+@[deprecated flatMap_singleton' (since := "2024-10-16")] abbrev bind_singleton' := @flatMap_singleton'
+@[deprecated head?_flatMap (since := "2024-10-16")] abbrev head_bind := @head?_flatMap
+@[deprecated flatMap_append (since := "2024-10-16")] abbrev bind_append := @flatMap_append
+@[deprecated flatMap_assoc (since := "2024-10-16")] abbrev bind_assoc := @flatMap_assoc
+@[deprecated map_flatMap (since := "2024-10-16")] abbrev map_bind := @map_flatMap
+@[deprecated flatMap_map (since := "2024-10-16")] abbrev bind_map := @flatMap_map
+@[deprecated map_eq_flatMap (since := "2024-10-16")] abbrev map_eq_bind := @map_eq_flatMap
+@[deprecated filterMap_flatMap (since := "2024-10-16")] abbrev filterMap_bind := @filterMap_flatMap
+@[deprecated filter_flatMap (since := "2024-10-16")] abbrev filter_bind := @filter_flatMap
+@[deprecated flatMap_eq_foldl (since := "2024-10-16")] abbrev bind_eq_foldl := @flatMap_eq_foldl
+@[deprecated flatMap_replicate (since := "2024-10-16")] abbrev bind_replicate := @flatMap_replicate
+@[deprecated reverse_flatMap (since := "2024-10-16")] abbrev reverse_bind := @reverse_flatMap
+@[deprecated flatMap_reverse (since := "2024-10-16")] abbrev bind_reverse := @flatMap_reverse
+@[deprecated getLast?_flatMap (since := "2024-10-16")] abbrev getLast?_bind := @getLast?_flatMap
+@[deprecated any_flatMap (since := "2024-10-16")] abbrev any_bind := @any_flatMap
+@[deprecated all_flatMap (since := "2024-10-16")] abbrev all_bind := @all_flatMap
 
 end List

src/Init/Data/List/Pairwise.lean

@@ -173,10 +173,12 @@ theorem pairwise_flatten {L : List (List α)} :
 
 @[deprecated pairwise_flatten (since := "2024-10-14")] abbrev pairwise_join := @pairwise_flatten
 
-theorem pairwise_bind {R : β → β → Prop} {l : List α} {f : α → List β} :
-    List.Pairwise R (l.bind f) ↔
+theorem pairwise_flatMap {R : β → β → Prop} {l : List α} {f : α → List β} :
+    List.Pairwise R (l.flatMap f) ↔
       (∀ a ∈ l, Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ x ∈ f a₁, ∀ y ∈ f a₂, R x y) l := by
-  simp [List.bind, pairwise_flatten, pairwise_map]
+  simp [List.flatMap, pairwise_flatten, pairwise_map]
+
+@[deprecated pairwise_flatMap (since := "2024-10-14")] abbrev pairwise_bind := @pairwise_flatMap
 
 theorem pairwise_reverse {l : List α} :
     l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a) := by

src/Init/Data/List/Perm.lean

@@ -470,9 +470,11 @@ theorem Perm.flatten {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatt
 
 @[deprecated Perm.flatten (since := "2024-10-14")] abbrev Perm.join := @Perm.flatten
 
-theorem Perm.bind_right {l₁ l₂ : List α} (f : α → List β) (p : l₁ ~ l₂) : l₁.bind f ~ l₂.bind f :=
+theorem Perm.flatMap_right {l₁ l₂ : List α} (f : α → List β) (p : l₁ ~ l₂) : l₁.flatMap f ~ l₂.flatMap f :=
   (p.map _).flatten
 
+@[deprecated Perm.flatMap_right (since := "2024-10-16")] abbrev Perm.bind_right := @Perm.flatMap_right
+
 theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
     (H : Pairwise (fun a b => f a → f b → False) l₁) (p : l₁ ~ l₂) : eraseP f l₁ ~ eraseP f l₂ := by
   induction p with

src/Init/Data/List/Range.lean

@@ -20,6 +20,7 @@ open Nat
 
 /-! ## Ranges and enumeration -/
 
+
 /-! ### range' -/
 
 theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step) n step := by

src/Init/Data/List/Sublist.lean

@@ -976,7 +976,7 @@ theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l :=
   drop_subset _ _ h
 
 theorem drop_suffix_drop_left (l : List α) {m n : Nat} (h : m ≤ n) : drop n l <:+ drop m l := by
-  rw [← Nat.sub_add_cancel h, Nat.add_comm, ← drop_drop]
+  rw [← Nat.sub_add_cancel h, ← drop_drop]
   apply drop_suffix
 
 -- See `Init.Data.List.Nat.TakeDrop` for `take_prefix_take_left`.

src/Init/Data/List/TakeDrop.lean

@@ -97,14 +97,14 @@ theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.
 
 theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := by simp
 
-@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (m + n) l
+@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l
   | m, [] => by simp
   | 0, l => by simp
   | m + 1, a :: l =>
     calc
       drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl
-      _ = drop (m + n) l := drop_drop n m l
-      _ = drop ((m + 1) + n) (a :: l) := by rw [Nat.add_right_comm]; rfl
+      _ = drop (n + m) l := drop_drop n m l
+      _ = drop (n + (m + 1)) (a :: l) := rfl
 
 theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
   | 0, _, _ => by simp
@@ -112,7 +112,7 @@ theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (t
   | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
 
 @[deprecated drop_drop (since := "2024-06-15")]
-theorem drop_add (m n) (l : List α) : drop (m + n) l = drop n (drop m l) := by
+theorem drop_add (m n) (l : List α) : drop (m + n) l = drop m (drop n l) := by
   simp [drop_drop]
 
 @[simp]
@@ -126,7 +126,7 @@ theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) :=
 
 @[simp]
 theorem drop_tail (l : List α) (n : Nat) : l.tail.drop n = l.drop (n + 1) := by
-  rw [Nat.add_comm, ← drop_drop, drop_one]
+  rw [← drop_drop, drop_one]
 
 @[simp]
 theorem drop_eq_nil_iff {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by

src/Init/Data/String/Basic.lean

@@ -317,9 +317,6 @@ theorem _root_.Char.utf8Size_le_four (c : Char) : c.utf8Size ≤ 4 := by
 
 @[simp] theorem pos_add_char (p : Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size := rfl
 
-protected theorem Pos.ne_zero_of_lt : {a b : Pos} → a < b → b ≠ 0
-  | _, _, hlt, rfl => Nat.not_lt_zero _ hlt
-
 theorem lt_next (s : String) (i : Pos) : i.1 < (s.next i).1 :=
   Nat.add_lt_add_left (Char.utf8Size_pos _) _
 
@@ -1024,66 +1021,6 @@ instance hasBeq : BEq Substring := ⟨beq⟩
 def sameAs (ss1 ss2 : Substring) : Bool :=
   ss1.startPos == ss2.startPos && ss1 == ss2
 
-/--
-Returns the longest common prefix of two substrings.
-The returned substring will use the same underlying string as `s`.
--/
-def commonPrefix (s t : Substring) : Substring :=
-  { s with stopPos := loop s.startPos t.startPos }
-where
-  /-- Returns the ending position of the common prefix, working up from `spos, tpos`. -/
-  loop spos tpos :=
-    if h : spos < s.stopPos ∧ tpos < t.stopPos then
-      if s.str.get spos == t.str.get tpos then
-        have := Nat.sub_lt_sub_left h.1 (s.str.lt_next spos)
-        loop (s.str.next spos) (t.str.next tpos)
-      else
-        spos
-    else
-      spos
-  termination_by s.stopPos.byteIdx - spos.byteIdx
-
-/--
-Returns the longest common suffix of two substrings.
-The returned substring will use the same underlying string as `s`.
--/
-def commonSuffix (s t : Substring) : Substring :=
-  { s with startPos := loop s.stopPos t.stopPos }
-where
-  /-- Returns the starting position of the common prefix, working down from `spos, tpos`. -/
-  loop spos tpos :=
-    if h : s.startPos < spos ∧ t.startPos < tpos then
-      let spos' := s.str.prev spos
-      let tpos' := t.str.prev tpos
-      if s.str.get spos' == t.str.get tpos' then
-        have : spos' < spos := s.str.prev_lt_of_pos spos (String.Pos.ne_zero_of_lt h.1)
-        loop spos' tpos'
-      else
-        spos
-    else
-      spos
-  termination_by spos.byteIdx
-
-/--
-If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
--/
-def dropPrefix? (s : Substring) (pre : Substring) : Option Substring :=
-  let t := s.commonPrefix pre
-  if t.bsize = pre.bsize then
-    some { s with startPos := t.stopPos }
-  else
-    none
-
-/--
-If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
--/
-def dropSuffix? (s : Substring) (suff : Substring) : Option Substring :=
-  let t := s.commonSuffix suff
-  if t.bsize = suff.bsize then
-    some { s with stopPos := t.startPos }
-  else
-    none
-
 end Substring
 
 namespace String
@@ -1145,28 +1082,6 @@ namespace String
 @[inline] def decapitalize (s : String) :=
   s.set 0 <| s.get 0 |>.toLower
 
-/--
-If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
--/
-def dropPrefix? (s : String) (pre : Substring) : Option Substring :=
-  s.toSubstring.dropPrefix? pre
-
-/--
-If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
--/
-def dropSuffix? (s : String) (suff : Substring) : Option Substring :=
-  s.toSubstring.dropSuffix? suff
-
-/-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
-or otherwise return `s`. -/
-def stripPrefix (s : String) (pre : Substring) : String :=
-  s.dropPrefix? pre |>.map Substring.toString |>.getD s
-
-/-- `s.stripSuffix suff` will remove `suff` from the end of `s` if it occurs there,
-or otherwise return `s`. -/
-def stripSuffix (s : String) (suff : Substring) : String :=
-  s.dropSuffix? suff |>.map Substring.toString |>.getD s
-
 end String
 
 namespace Char

src/Init/Data/String/Extra.lean

@@ -117,10 +117,10 @@ def utf8EncodeChar (c : Char) : List UInt8 :=
 /-- Converts the given `String` to a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded byte array. -/
 @[extern "lean_string_to_utf8"]
 def toUTF8 (a : @& String) : ByteArray :=
-  ⟨⟨a.data.bind utf8EncodeChar⟩⟩
+  ⟨⟨a.data.flatMap utf8EncodeChar⟩⟩
 
 @[simp] theorem size_toUTF8 (s : String) : s.toUTF8.size = s.utf8ByteSize := by
-  simp [toUTF8, ByteArray.size, Array.size, utf8ByteSize, List.bind]
+  simp [toUTF8, ByteArray.size, Array.size, utf8ByteSize, List.flatMap]
   induction s.data <;> simp [List.map, List.flatten, utf8ByteSize.go, Nat.add_comm, *]
 
 /-- Accesses a byte in the UTF-8 encoding of the `String`. O(1) -/

src/Init/Tactics.lean

@@ -910,15 +910,6 @@ macro_rules | `(tactic| trivial) => `(tactic| simp)
 -/
 syntax "trivial" : tactic
 
-/--
-`classical tacs` runs `tacs` in a scope where `Classical.propDecidable` is a low priority
-local instance.
-
-Note that `classical` is a scoping tactic: it adds the instance only within the
-scope of the tactic.
--/
-syntax (name := classical) "classical" ppDedent(tacticSeq) : tactic
-
 /--
 The `split` tactic is useful for breaking nested if-then-else and `match` expressions into separate cases.
 For a `match` expression with `n` cases, the `split` tactic generates at most `n` subgoals.

src/Lean/Data/Xml/Parser.lean

@@ -459,7 +459,7 @@ mutual
 
       let z ← optional (Content.Character <$> CharData)
       pure #[y, z]
-    let xs := #[x] ++ xs.concatMap id |>.filterMap id
+    let xs := #[x] ++ xs.flatMap id |>.filterMap id
     let mut res := #[]
     for x in xs do
       if res.size > 0 then

src/Lean/Elab/BuiltinCommand.lean

@@ -229,7 +229,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
 
 @[builtin_command_elab «variable»] def elabVariable : CommandElab
   | `(variable $binders*) => do
-    let binders ← binders.concatMapM replaceBinderAnnotation
+    let binders ← binders.flatMapM replaceBinderAnnotation
     -- Try to elaborate `binders` for sanity checking
     runTermElabM fun _ => Term.withSynthesize <| Term.withAutoBoundImplicit <|
       Term.elabBinders binders fun _ => pure ()
@@ -348,7 +348,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
 @[builtin_command_elab Lean.Parser.Command.include] def elabInclude : CommandElab
   | `(Lean.Parser.Command.include| include $ids*) => do
     let sc ← getScope
-    let vars ← sc.varDecls.concatMapM getBracketedBinderIds
+    let vars ← sc.varDecls.flatMapM getBracketedBinderIds
     let mut uids := #[]
     for id in ids do
       if let some idx := vars.findIdx? (· == id.getId) then

src/Lean/Elab/Command.lean

@@ -571,7 +571,7 @@ def getBracketedBinderIds : Syntax → CommandElabM (Array Name)
 private def mkTermContext (ctx : Context) (s : State) : CommandElabM Term.Context := do
   let scope      := s.scopes.head!
   let mut sectionVars := {}
-  for id in (← scope.varDecls.concatMapM getBracketedBinderIds), uid in scope.varUIds do
+  for id in (← scope.varDecls.flatMapM getBracketedBinderIds), uid in scope.varUIds do
     sectionVars := sectionVars.insert id uid
   return {
     macroStack             := ctx.macroStack
@@ -714,7 +714,7 @@ def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM Expand
   let currNamespace ← getCurrNamespace
   let currLevelNames ← getLevelNames
   let r ← Elab.expandDeclId currNamespace currLevelNames declId modifiers
-  for id in (← (← getScope).varDecls.concatMapM getBracketedBinderIds) do
+  for id in (← (← getScope).varDecls.flatMapM getBracketedBinderIds) do
     if id == r.shortName then
       throwError "invalid declaration name '{r.shortName}', there is a section variable with the same name"
   return r

src/Lean/Elab/Frontend.lean

@@ -151,7 +151,7 @@ def runFrontend
   snaps.runAndReport opts jsonOutput
 
   if let some ileanFileName := ileanFileName? then
-    let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
+    let trees := snaps.getAll.flatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
     let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
     let ilean := { module := mainModuleName, references := ← references.toLspModuleRefs : Lean.Server.Ilean }
     IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean

src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -226,7 +226,7 @@ def allCombinations (xss : Array (Array α)) : Option (Array (Array α)) :=
   else
     let rec go i acc : Array (Array α):=
       if h : i < xss.size then
-        xss[i].concatMap fun x => go (i + 1) (acc.push x)
+        xss[i].flatMap fun x => go (i + 1) (acc.push x)
       else
         #[acc]
     some (go 0 #[])

src/Lean/Elab/Tactic.lean

@@ -43,4 +43,3 @@ import Lean.Elab.Tactic.Rewrites
 import Lean.Elab.Tactic.DiscrTreeKey
 import Lean.Elab.Tactic.BVDecide
 import Lean.Elab.Tactic.BoolToPropSimps
-import Lean.Elab.Tactic.Classical

src/Lean/Elab/Tactic/Classical.lean

@@ -1,34 +0,0 @@
-/-
-Copyright (c) 2021 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Kim Morrison
--/
-prelude
-import Lean.Elab.Tactic.Basic
-
-/-! # `classical` tactic -/
-
-namespace Lean.Elab.Tactic
-open Lean Meta Elab.Tactic
-
-/--
-`classical t` runs `t` in a scope where `Classical.propDecidable` is a low priority
-local instance.
--/
-def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t : m α) :
-    m α := do
-  modifyEnv Meta.instanceExtension.pushScope
-  Meta.addInstance ``Classical.propDecidable .local 10
-  try
-    t
-  finally
-    modifyEnv Meta.instanceExtension.popScope
-
-@[builtin_tactic Lean.Parser.Tactic.classical]
-def evalClassical : Tactic := fun stx => do
-  match stx with
-  | `(tactic| classical $tacs:tacticSeq) =>
-     classical <| Elab.Tactic.evalTactic tacs
-  | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic

src/Lean/Meta/RecursorInfo.lean

@@ -67,6 +67,29 @@ instance : ToString RecursorInfo := ⟨fun info =>
 
 end RecursorInfo
 
+private def mkRecursorInfoForKernelRec (declName : Name) (val : RecursorVal) : MetaM RecursorInfo := do
+  let ival ← getConstInfoInduct val.getInduct
+  let numLParams    := ival.levelParams.length
+  let univLevelPos  := (List.range numLParams).map RecursorUnivLevelPos.majorType
+  let univLevelPos  := if val.levelParams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos
+  let produceMotive := List.replicate val.numMinors true
+  let paramsPos     := (List.range val.numParams).map some
+  let indicesPos    := (List.range val.numIndices).map fun pos => val.numParams + pos
+  let numArgs       := val.numIndices + val.numParams + val.numMinors + val.numMotives + 1
+  pure {
+    recursorName  := declName,
+    typeName      := val.getInduct,
+    univLevelPos  := univLevelPos,
+    majorPos      := val.getMajorIdx,
+    depElim       := true,
+    recursive     := ival.isRec,
+    produceMotive := produceMotive,
+    paramsPos     := paramsPos,
+    indicesPos    := indicesPos,
+    numArgs       := numArgs
+  }
+
+
 private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat) : MetaM (Option Nat) :=
   if majorPos?.isSome then pure majorPos?
   else do
@@ -179,8 +202,8 @@ private def checkMotiveResultType (declName : Name) (motiveArgs : Array Expr) (m
   if !motiveResultType.isSort || motiveArgs.size != motiveTypeParams.size then
     throwError "invalid user defined recursor '{declName}', motive must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant"
 
-private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat) : MetaM RecursorInfo := do
-  let cinfo ← getConstInfo declName
+private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) : MetaM RecursorInfo := do
+  let declName := cinfo.name
   let majorPos? ← getMajorPosIfAuxRecursor? declName majorPos?
   forallTelescopeReducing cinfo.type fun xs type => type.withApp fun motive motiveArgs => do
     checkMotive declName motive motiveArgs
@@ -227,6 +250,12 @@ def Attribute.Recursor.getMajorPos (stx : Syntax) : AttrM Nat := do
   else
     throwErrorAt stx "unexpected attribute argument, numeral expected"
 
+private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
+  let cinfo ← getConstInfo declName
+  match cinfo with
+  | ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
+  | _                        => mkRecursorInfoAux cinfo majorPos?
+
 builtin_initialize recursorAttribute : ParametricAttribute Nat ←
   registerParametricAttribute {
     name := `recursor,
@@ -240,7 +269,11 @@ def getMajorPos? (env : Environment) (declName : Name) : Option Nat :=
   recursorAttribute.getParam? env declName
 
 def mkRecursorInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
-  let majorPos? := majorPos? <|> getMajorPos? (← getEnv) declName
-  mkRecursorInfoCore declName majorPos?
+  let cinfo ← getConstInfo declName
+  match cinfo with
+  | ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
+  | _                        => match majorPos? with
+    | none => do mkRecursorInfoAux cinfo (getMajorPos? (← getEnv) declName)
+    | _    => mkRecursorInfoAux cinfo majorPos?
 
 end Lean.Meta

src/Lean/Meta/Tactic/Intro.lean

@@ -164,11 +164,7 @@ does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId true
 
-/--
-Calculate the number of new hypotheses that would be created by `intros`,
-i.e. the number of binders which can be introduced without unfolding definitions.
--/
-partial def getIntrosSize : Expr → Nat
+private partial def getIntrosSize : Expr → Nat
   | .forallE _ _ b _ => getIntrosSize b + 1
   | .letE _ _ _ b _  => getIntrosSize b + 1
   | .mdata _ b       => getIntrosSize b

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean

@@ -62,12 +62,12 @@ builtin_simproc [simp, seval] reduceNe  (( _ : Fin _) ≠ _)  := reduceBinPred `
 builtin_dsimproc [simp, seval] reduceBEq  (( _ : Fin _) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
 builtin_dsimproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred ``bne 4 (. != .)
 
-/-- Simplification procedure for ensuring `Fin n` literals are normalized. -/
+/-- Simplification procedure for ensuring `Fin` literals are normalized. -/
 builtin_dsimproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
   let_expr OfNat.ofNat _ m _ ← e | return .continue
   let some ⟨n, v⟩ ← getFinValue? e | return .continue
   let some m ← getNatValue? m | return .continue
-  if m < n then
+  if n == m then
     -- Design decision: should we return `.continue` instead of `.done` when simplifying.
     -- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`
     return .done e

src/Lean/Server/CodeActions/Basic.lean

@@ -124,7 +124,7 @@ def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array
         let names := codeActionProviderExt.getState env |>.toArray
         let caps ← names.mapM evalCodeActionProvider
         return (← builtinCodeActionProviders.get).toList.toArray ++ Array.zip names caps
-      caps.concatMapM fun (providerName, cap) => do
+      caps.flatMapM fun (providerName, cap) => do
         let cas ← cap params snap
         cas.mapIdxM fun i lca => do
           if lca.lazy?.isNone then return lca.eager

src/Lean/Server/CodeActions/Provider.lean

@@ -38,7 +38,7 @@ A code action which calls all `@[hole_code_action]` code actions on each hole
     unless head ≤ endPos && startPos ≤ tail do return result
     result.push (ctx, info)
   let #[(ctx, info)] := holes | return #[]
-  (holeCodeActionExt.getState snap.env).2.concatMapM (· params snap ctx info)
+  (holeCodeActionExt.getState snap.env).2.flatMapM (· params snap ctx info)
 
 /--
 The return value of `findTactic?`.

src/Lean/Server/InfoUtils.lean

@@ -197,7 +197,7 @@ def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextI
 /-- Find an info node, if any, which should be shown on hover/cursor at position `hoverPos`. -/
 partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (includeStop := false) (omitAppFns := false) (omitIdentApps := false) : Option InfoWithCtx := Id.run do
   let results := t.visitM (m := Id) (postNode := fun ctx info children results => do
-    let mut results := results.bind (·.getD [])
+    let mut results := results.flatMap (·.getD [])
     if omitAppFns && info.stx.isOfKind ``Parser.Term.app && info.stx[0].isIdent then
         results := results.filter (·.2.info.stx != info.stx[0])
     if omitIdentApps && info.stx.isIdent then

src/Lean/Server/Watchdog.lean

@@ -669,7 +669,7 @@ where
     let grouped := incomingCalls.groupByKey (·.«from»)
     let collapsed := grouped.toArray.map fun ⟨_, group⟩ => {
       «from» := group[0]!.«from»
-      fromRanges := group.concatMap (·.fromRanges)
+      fromRanges := group.flatMap (·.fromRanges)
     }
     collapsed
 
@@ -716,7 +716,7 @@ where
     let grouped := outgoingCalls.groupByKey (·.to)
     let collapsed := grouped.toArray.map fun ⟨_, group⟩ => {
       to := group[0]!.to
-      fromRanges := group.concatMap (·.fromRanges)
+      fromRanges := group.flatMap (·.fromRanges)
     }
     collapsed
 

src/Std/Data/DHashMap/Internal/Defs.lean

@@ -156,7 +156,7 @@ namespace DHashMap.Internal
 
 /-- Internal implementation detail of the hash map -/
 def toListModel (buckets : Array (AssocList α β)) : List ((a : α) × β a) :=
-  buckets.toList.bind AssocList.toList
+  buckets.toList.flatMap AssocList.toList
 
 /-- Internal implementation detail of the hash map -/
 @[inline] def computeSize (buckets : Array (AssocList α β)) : Nat :=

src/Std/Data/DHashMap/Internal/List/Associative.lean

@@ -1720,13 +1720,13 @@ theorem containsKey_append [BEq α] {l l' : List ((a : α) × β a)} {a : α} :
     containsKey a (l ++ l') = (containsKey a l || containsKey a l') := by
   simp [containsKey_eq_isSome_getEntry?]
 
-theorem containsKey_bind_eq_false [BEq α] {γ : Type w} {l : List γ} {f : γ → List ((a : α) × β a)}
+theorem containsKey_flatMap_eq_false [BEq α] {γ : Type w} {l : List γ} {f : γ → List ((a : α) × β a)}
     {a : α} (h : ∀ (i : Nat) (h : i < l.length), containsKey a (f l[i]) = false) :
-    containsKey a (l.bind f) = false := by
+    containsKey a (l.flatMap f) = false := by
   induction l
   · simp
   · next g t ih =>
-    simp only [List.bind_cons, containsKey_append, Bool.or_eq_false_iff]
+    simp only [List.flatMap_cons, containsKey_append, Bool.or_eq_false_iff]
     refine ⟨?_, ?_⟩
     · simpa using h 0 (by simp)
     · refine ih ?_

src/Std/Data/DHashMap/Internal/Model.lean

@@ -88,7 +88,7 @@ theorem exists_bucket_of_uset [BEq α] [Hashable α]
           containsKey k l = false) := by
   have h₀ : 0 < self.size := by omega
   obtain ⟨l₁, l₂, h₁, h₂, h₃⟩ := Array.exists_of_uset self i d hi
-  refine ⟨l₁.bind AssocList.toList ++ l₂.bind AssocList.toList, ?_, ?_, ?_⟩
+  refine ⟨l₁.flatMap AssocList.toList ++ l₂.flatMap AssocList.toList, ?_, ?_, ?_⟩
   · rw [toListModel, h₁]
     simpa using perm_append_comm_assoc _ _ _
   · rw [toListModel, h₃]
@@ -96,12 +96,12 @@ theorem exists_bucket_of_uset [BEq α] [Hashable α]
   · intro _ h k hki
     simp only [containsKey_append, Bool.or_eq_false_iff]
     refine ⟨?_, ?_⟩
-    · apply List.containsKey_bind_eq_false
+    · apply List.containsKey_flatMap_eq_false
       intro j hj
       rw [List.getElem_append_left' (l₂ := self[i] :: l₂), getElem_congr_coll h₁.symm]
       apply (h.hashes_to j _).containsKey_eq_false h₀ k
       omega
-    · apply List.containsKey_bind_eq_false
+    · apply List.containsKey_flatMap_eq_false
       intro j hj
       rw [← List.getElem_cons_succ self[i] _ _
         (by simp only [Array.ugetElem_eq_getElem, List.length_cons]; omega)]
@@ -121,7 +121,7 @@ theorem exists_bucket_of_update [BEq α] [Hashable α] (m : Array (AssocList α
 
 theorem exists_bucket' [BEq α] [Hashable α]
     (self : Array (AssocList α β)) (i : USize) (hi : i.toNat < self.size) :
-      ∃ l, Perm (self.toList.bind AssocList.toList) (self[i.toNat].toList ++ l) ∧
+      ∃ l, Perm (self.toList.flatMap AssocList.toList) (self[i.toNat].toList ++ l) ∧
         (∀ [LawfulHashable α], IsHashSelf self → ∀ k,
           (mkIdx self.size (by omega) (hash k)).1.toNat = i.toNat → containsKey k l = false) := by
   obtain ⟨l, h₁, -, h₂⟩ := exists_bucket_of_uset self i hi .nil
@@ -186,8 +186,8 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
     have := (hg (l := []) (l' := [])).length_eq
     rw [List.length_append, List.append_nil] at this
     omega
-  rw [updateAllBuckets, toListModel, Array.toList_map, List.bind_eq_foldl, List.foldl_map,
-    toListModel, List.bind_eq_foldl]
+  rw [updateAllBuckets, toListModel, Array.toList_map, List.flatMap_eq_foldl, List.foldl_map,
+    toListModel, List.flatMap_eq_foldl]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a: α) × δ a)) (l'' : List ((a : α) × β a)),
       Perm (g l'') l' →
       Perm (l.foldl (fun acc a => acc ++ (f a).toList) l')

src/Std/Data/DHashMap/Internal/WF.lean

@@ -31,14 +31,14 @@ namespace Std.DHashMap.Internal
 @[simp]
 theorem toListModel_mkArray_nil {c} :
     toListModel (mkArray c (AssocList.nil : AssocList α β)) = [] := by
-  suffices ∀ d, (List.replicate d AssocList.nil).bind AssocList.toList = [] from this _
+  suffices ∀ d, (List.replicate d AssocList.nil).flatMap AssocList.toList = [] from this _
   intro d
   induction d <;> simp_all [List.replicate]
 
 @[simp]
 theorem computeSize_eq {buckets : Array (AssocList α β)} :
     computeSize buckets = (toListModel buckets).length := by
-  rw [computeSize, toListModel, List.bind_eq_foldl, Array.foldl_eq_foldl_toList]
+  rw [computeSize, toListModel, List.flatMap_eq_foldl, Array.foldl_eq_foldl_toList]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
       l.foldl (fun d b => d + b.toList.length) l'.length =
         (l.foldl (fun acc a => acc ++ a.toList) l').length
@@ -129,7 +129,7 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
     (target : {d : Array (AssocList α β) // 0 < d.size}) : expand.go 0 source target =
       (toListModel source).foldl (fun acc p => reinsertAux hash acc p.1 p.2) target := by
   suffices ∀ i, expand.go i source target =
-    ((source.toList.drop i).bind AssocList.toList).foldl
+    ((source.toList.drop i).flatMap AssocList.toList).foldl
       (fun acc p => reinsertAux hash acc p.1 p.2) target by
     simpa using this 0
   intro i
@@ -139,10 +139,10 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
     rw [expand.go_pos hi]
     refine ih.trans ?_
     simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set]
-    rw [List.drop_eq_getElem_cons hi, List.bind_cons, List.foldl_append,
+    rw [List.drop_eq_getElem_cons hi, List.flatMap_cons, List.foldl_append,
       List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_getElem_toList]
   · next i source target hi =>
-    rw [expand.go_neg hi, List.drop_eq_nil_of_le, bind_nil, foldl_nil]
+    rw [expand.go_neg hi, List.drop_eq_nil_of_le, flatMap_nil, foldl_nil]
     rwa [Array.size_eq_length_toList, Nat.not_lt] at hi
 
 theorem isHashSelf_expand [BEq α] [Hashable α] [LawfulHashable α] [EquivBEq α]

src/lake/Lake/Build/Imports.lean

@@ -29,7 +29,7 @@ def buildImportsAndDeps (leanFile : FilePath) (imports : Array Module) : FetchM
     let precompileImports ← computePrecompileImportsAux leanFile imports
     let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
     let externLibJob ← BuildJob.collectArray <| ←
-      pkgs.concatMapM (·.externLibs.mapM (·.dynlib.fetch))
+      pkgs.flatMapM (·.externLibs.mapM (·.dynlib.fetch))
     let precompileJob ← BuildJob.collectArray <| ←
       precompileImports.mapM (·.dynlib.fetch)
     let job ←

src/lake/Lake/Build/Library.lean

@@ -60,7 +60,7 @@ def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
       ""
   withRegisterJob s!"{self.name}:static{suffix}" do
   let mods ← self.modules.fetch
-  let oJobs ← mods.concatMapM fun mod =>
+  let oJobs ← mods.flatMapM fun mod =>
     mod.nativeFacets shouldExport |>.mapM fun facet => fetch <| mod.facet facet.name
   let libFile := if shouldExport then self.staticExportLibFile else self.staticLibFile
   buildStaticLib libFile oJobs
@@ -80,10 +80,10 @@ protected def LeanLib.recBuildShared
 (self : LeanLib) : FetchM (BuildJob FilePath) := do
   withRegisterJob s!"{self.name}:shared" do
   let mods ← self.modules.fetch
-  let oJobs ← mods.concatMapM fun mod =>
+  let oJobs ← mods.flatMapM fun mod =>
     mod.nativeFacets true |>.mapM fun facet => fetch <| mod.facet facet.name
   let pkgs := mods.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
-  let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.shared.fetch))
+  let externJobs ← pkgs.flatMapM (·.externLibs.mapM (·.shared.fetch))
   buildLeanSharedLib self.sharedLibFile (oJobs ++ externJobs) self.weakLinkArgs self.linkArgs
 
 /-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/

src/lake/Lake/CLI/Build.lean

@@ -113,7 +113,7 @@ def resolveTargetInPackage (ws : Workspace)
     throw <| CliError.missingTarget pkg.name (target.toString false)
 
 def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliError (Array BuildSpec) :=
-  pkg.defaultTargets.concatMapM (resolveTargetInPackage ws pkg · .anonymous)
+  pkg.defaultTargets.flatMapM (resolveTargetInPackage ws pkg · .anonymous)
 
 def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Except CliError (Array BuildSpec) :=
   if facet.isAnonymous then

src/lake/Lake/Util/OrderedTagAttribute.lean

@@ -47,4 +47,4 @@ def OrderedTagAttribute.hasTag (attr : OrderedTagAttribute) (env : Environment)
 /-- Get all tagged declaration names, both those imported and those in the current module. -/
 def OrderedTagAttribute.getAllEntries (attr : OrderedTagAttribute) (env : Environment) : Array Name :=
   let s := attr.ext.toEnvExtension.getState env
-  s.importedEntries.concatMap id ++ s.state
+  s.importedEntries.flatMap id ++ s.state

tests/bench/bv_decide_inequality.lean

@@ -1,53 +0,0 @@
-import Std.Tactic.BVDecide
-
-/-! Smaller real-world problems taken from https://github.com/leanprover/LNSym,
-which previously had a bad interaction with the normalization pass -/
-
-variable (a1 a2 b1 b2 a b c d k n : BitVec 64)
-
-example :
-  (!decide (b1 - a1 ≤ a2 - a1) && !decide (b2 - a1 ≤ a2 - a1) && !decide (a1 - b1 ≤ b2 - b1) &&
-    !decide (a2 - b1 ≤ b2 - b1)) =
-  (!decide (a1 - b1 ≤ b2 - b1) && !decide (a2 - b1 ≤ b2 - b1) && !decide (b1 - a1 ≤ a2 - a1) &&
-    !decide (b2 - a1 ≤ a2 - a1)) := by
-  bv_decide
-
-example :
-    a2 - a1 < b1 - a1
-    → a2 - a1 < b2 - a1
-    → b2 - b1 < a1 - b1
-    → b2 - b1 < a2 - b1
-    → ¬a1 = b1 := by
-  bv_decide
-
-example : ¬a = b ↔ 0#64 < b - a ∧ 0#64 < a - b := by
-  bv_decide
-
-example :
-    b - a < c - a → b - a < d - a → d - c < a - c → d - c < b - c
-    → (0#64 < c - a ∧ 0#64 < d - a) ∧ d - c < a - c := by
-  bv_decide
-
-set_option sat.timeout 120 in
-example :
-    n < 18446744073709551615#64 - k →
-    ((a + k - a < a + k + 1#64 - a ∧ a + k - a < a + k + 1#64 + n - a) ∧
-        a + k + 1#64 + n - (a + k + 1#64) < a - (a + k + 1#64)) ∧
-      a + k + 1#64 + n - (a + k + 1#64) < a + k - (a + k + 1#64) := by
-  bv_decide
-
-example :
-    n < 18446744073709551615 →
-    (0#64 < addr + 1#64 - addr ∧ 0#64 < addr + 1#64 + n - addr)
-    ∧ addr + 1#64 + n - (addr + 1#64) < addr - (addr + 1#64) := by
-  bv_decide
-
-set_option sat.timeout 120 in
-example :
-    a2 - a1 < b1 - a1 → a2 - a1 < b2 - a1 →
-    b2 - b1 < a1 - b1 → b2 - b1 < a2 - b1 →
-    b2 - b1 = 18446744073709551615#64 ∨ c2 - b1 ≤ b2 - b1 ∧ c1 - b1 ≤ c2 - b1 →
-    ((a2 - a1 < c1 - a1 ∧ a2 - a1 < c2 - a1)
-    ∧ c2 - c1 < a1 - c1)
-    ∧ c2 - c1 < a2 - c1 := by
-  bv_decide

tests/bench/speedcenter.exec.velcom.yaml

@@ -356,9 +356,3 @@
   run_config:
     <<: *time
     cmd: lean bv_decide_mod.lean
-- attributes:
-    description: bv_decide_inequality.lean
-    tags: [fast]
-  run_config:
-    <<: *time
-    cmd: lean bv_decide_inequality.lean

tests/lean/run/classical.lean

@@ -1,21 +0,0 @@
-example : Bool := by
-  fail_if_success have := ∀ p, decide p -- no classical in scope
-  classical
-  have := ∀ p, decide p -- uses the classical instance
-  guard_expr decide (0 < 1) = @decide (0 < 1) (Nat.decLt 0 1)
-  exact decide (0 < 1) -- will use the decidable instance
-
--- double check no leakage
-example : Bool := by
-  fail_if_success have := ∀ p, decide p -- no classical in scope
-  exact decide (0 < 1) -- uses the decidable instance
-
--- check that classical respects tactic blocks
-example : Bool := by
-  fail_if_success have := ∀ p, decide p -- no classical in scope
-  ( -- start a scope
-    classical
-    have := ∀ p, decide p -- uses the classical instance
-  )
-  fail_if_success have := ∀ p, decide p -- no classical in scope again
-  exact decide (0 < 1) -- will use the decidable instance

tests/lean/run/issue5630.lean

@@ -1,15 +0,0 @@
-
-example (n : Fin 25) (P : Fin 25 → Prop) : P 26 := by
-  simp only [Fin.isValue]
-  guard_target = P 1
-  sorry
-
-example (n : Fin 25) (P : Fin 25 → Prop) : P 25 := by
-  simp only [Fin.isValue]
-  guard_target = P 0
-  sorry
-
-example (n : Fin 25) (P : Fin 25 → Prop) : P 24 := by
-  fail_if_success simp only [Fin.isValue]
-  guard_target = P 24
-  sorry