chore: update stage0

one more

one more

one more

fix test

src/Init/Data/Array/Lemmas.lean

@@ -1060,7 +1060,7 @@ theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) :
 
 /-! ### flatten -/
 
-@[simp] theorem toList_flatten {l : Array (Array α)} : l.flatten.toList = (l.toList.map toList).join := by
+@[simp] theorem toList_flatten {l : Array (Array α)} : l.flatten.toList = (l.toList.map toList).flatten := by
   dsimp [flatten]
   simp only [foldl_eq_foldl_toList]
   generalize l.toList = l
@@ -1071,7 +1071,7 @@ theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) :
   | cons h => induction h.toList <;> simp [*]
 
 theorem mem_flatten : ∀ {L : Array (Array α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l := by
-  simp only [mem_def, toList_flatten, List.mem_join, List.mem_map]
+  simp only [mem_def, toList_flatten, List.mem_flatten, List.mem_map]
   intro l
   constructor
   · rintro ⟨_, ⟨s, m, rfl⟩, h⟩
@@ -1567,7 +1567,7 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
     l.toArray.filterMap f = (l.filterMap f).toArray := by
   simp
 
-@[simp] theorem flatten_toArray (l : List (List α)) : (l.toArray.map List.toArray).flatten = l.join.toArray := by
+@[simp] theorem flatten_toArray (l : List (List α)) : (l.toArray.map List.toArray).flatten = l.flatten.toArray := by
   apply ext'
   simp [Function.comp_def]
 

src/Init/Data/List/Attach.lean

@@ -666,11 +666,13 @@ and simplifies these to the function directly taking the value.
     (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach := by
   simp [unattach, -map_subtype]
 
-@[simp] theorem unattach_join {p : α → Prop} {l : List (List { x // p x })} :
-    l.join.unattach = (l.map unattach).join := by
+@[simp] theorem unattach_flatten {p : α → Prop} {l : List (List { x // p x })} :
+    l.flatten.unattach = (l.map unattach).flatten := by
   unfold unattach
   induction l <;> simp_all
 
+@[deprecated unattach_flatten (since := "2024-10-14")] abbrev unattach_join := @unattach_flatten
+
 @[simp] theorem unattach_replicate {p : α → Prop} {n : Nat} {x : { x // p x }} :
     (List.replicate n x).unattach = List.replicate n x.1 := by
   simp [unattach, -map_subtype]

src/Init/Data/List/Basic.lean

@@ -29,7 +29,7 @@ The operations are organized as follow:
 * Lexicographic ordering: `lt`, `le`, and instances.
 * Head and tail operators: `head`, `head?`, `headD?`, `tail`, `tail?`, `tailD`.
 * Basic operations:
-  `map`, `filter`, `filterMap`, `foldr`, `append`, `join`, `pure`, `bind`, `replicate`, and
+  `map`, `filter`, `filterMap`, `foldr`, `append`, `flatten`, `pure`, `bind`, `replicate`, and
   `reverse`.
 * Additional functions defined in terms of these: `leftpad`, `rightPad`, and `reduceOption`.
 * Operations using indexes: `mapIdx`.
@@ -369,7 +369,7 @@ def tailD (list fallback : List α) : List α :=
 /-! ## Basic `List` operations.
 
 We define the basic functional programming operations on `List`:
-`map`, `filter`, `filterMap`, `foldr`, `append`, `join`, `pure`, `bind`, `replicate`, and `reverse`.
+`map`, `filter`, `filterMap`, `foldr`, `append`, `flatten`, `pure`, `bind`, `replicate`, and `reverse`.
 -/
 
 /-! ### map -/
@@ -543,18 +543,20 @@ theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux a
   simp [reverse, reverseAux]
   rw [← reverseAux_eq_append]
 
-/-! ### join -/
+/-! ### flatten -/
 
 /--
-`O(|join L|)`. `join L` concatenates all the lists in `L` into one list.
-* `join [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]`
+`O(|flatten L|)`. `join L` concatenates all the lists in `L` into one list.
+* `flatten [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]`
 -/
-def join : List (List α) → List α
+def flatten : List (List α) → List α
   | []      => []
-  | a :: as => a ++ join as
+  | a :: as => a ++ flatten as
 
-@[simp] theorem join_nil : List.join ([] : List (List α)) = [] := rfl
-@[simp] theorem join_cons : (l :: ls).join = l ++ ls.join := rfl
+@[simp] theorem flatten_nil : List.flatten ([] : List (List α)) = [] := rfl
+@[simp] theorem flatten_cons : (l :: ls).flatten = l ++ ls.flatten := rfl
+
+@[deprecated flatten (since := "2024-10-14"), inherit_doc flatten] abbrev join := @flatten
 
 /-! ### pure -/
 
@@ -568,11 +570,11 @@ def join : List (List α) → List α
 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 β := join (map b a)
+@[inline] protected def bind {α : Type u} {β : Type v} (a : List α) (b : α → List β) : List β := flatten (map b a)
 
-@[simp] theorem bind_nil (f : α → List β) : List.bind [] f = [] := by simp [join, List.bind]
+@[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 [join, List.bind]
+  List.bind (x :: xs) f = f x ++ List.bind xs f := by simp [flatten, List.bind]
 
 set_option linter.missingDocs false in
 @[deprecated bind_nil (since := "2024-06-15")] abbrev nil_bind := @bind_nil
@@ -1528,7 +1530,7 @@ def intersperse (sep : α) : List α → List α
 * `intercalate sep [a, b, c] = a ++ sep ++ b ++ sep ++ c`
 -/
 def intercalate (sep : List α) (xs : List (List α)) : List α :=
-  join (intersperse sep xs)
+  (intersperse sep xs).flatten
 
 /-! ### eraseDups -/
 

src/Init/Data/List/Count.lean

@@ -155,11 +155,13 @@ theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : List α)
   ext a
   simp (config := { contextual := true }) [Option.getD_eq_iff]
 
-@[simp] theorem countP_join (l : List (List α)) :
-    countP p l.join = Nat.sum (l.map (countP p)) := by
-  simp only [countP_eq_length_filter, filter_join]
+@[simp] theorem countP_flatten (l : List (List α)) :
+    countP p l.flatten = Nat.sum (l.map (countP p)) := by
+  simp only [countP_eq_length_filter, filter_flatten]
   simp [countP_eq_length_filter']
 
+@[deprecated countP_flatten (since := "2024-10-14")] abbrev countP_join := @countP_flatten
+
 @[simp] theorem countP_reverse (l : List α) : countP p l.reverse = countP p l := by
   simp [countP_eq_length_filter, filter_reverse]
 
@@ -230,8 +232,10 @@ 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_join (a : α) (l : List (List α)) : count a l.join = Nat.sum (l.map (count a)) := by
-  simp only [count_eq_countP, countP_join, count_eq_countP']
+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
 
 @[simp] theorem count_reverse (a : α) (l : List α) : count a l.reverse = count a l := by
   simp only [count_eq_countP, countP_eq_length_filter, filter_reverse, length_reverse]

src/Init/Data/List/Find.lean

@@ -132,14 +132,14 @@ theorem findSome?_append {l₁ l₂ : List α} : (l₁ ++ l₂).findSome? f = (l
     simp only [cons_append, findSome?]
     split <;> simp_all
 
-theorem head_join {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
-    (join L).head (by simpa using h) = (L.findSome? fun l => l.head?).get (by simpa using h) := by
-  simp [head_eq_iff_head?_eq_some, head?_join]
+theorem head_flatten {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
+    (flatten L).head (by simpa using h) = (L.findSome? fun l => l.head?).get (by simpa using h) := by
+  simp [head_eq_iff_head?_eq_some, head?_flatten]
 
-theorem getLast_join {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
-    (join L).getLast (by simpa using h) =
+theorem getLast_flatten {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
+    (flatten L).getLast (by simpa using h) =
       (L.reverse.findSome? fun l => l.getLast?).get (by simpa using h) := by
-  simp [getLast_eq_iff_getLast_eq_some, getLast?_join]
+  simp [getLast_eq_iff_getLast_eq_some, getLast?_flatten]
 
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   cases n with
@@ -326,35 +326,35 @@ theorem get_find?_mem (xs : List α) (p : α → Bool) (h) : (xs.find? p).get h
     simp only [cons_append, find?]
     by_cases h : p x <;> simp [h, ih]
 
-@[simp] theorem find?_join (xs : List (List α)) (p : α → Bool) :
-    xs.join.find? p = xs.findSome? (·.find? p) := by
+@[simp] theorem find?_flatten (xs : List (List α)) (p : α → Bool) :
+    xs.flatten.find? p = xs.findSome? (·.find? p) := by
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp only [join_cons, find?_append, findSome?_cons, ih]
+    simp only [flatten_cons, find?_append, findSome?_cons, ih]
     split <;> simp [*]
 
-theorem find?_join_eq_none {xs : List (List α)} {p : α → Bool} :
-    xs.join.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
+theorem find?_flatten_eq_none {xs : List (List α)} {p : α → Bool} :
+    xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
   simp
 
 /--
-If `find? p` returns `some a` from `xs.join`, then `p a` holds, and
+If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
 some list in `xs` contains `a`, and no earlier element of that list satisfies `p`.
 Moreover, no earlier list in `xs` has an element satisfying `p`.
 -/
-theorem find?_join_eq_some {xs : List (List α)} {p : α → Bool} {a : α} :
-    xs.join.find? p = some a ↔
+theorem find?_flatten_eq_some {xs : List (List α)} {p : α → Bool} {a : α} :
+    xs.flatten.find? p = some a ↔
       p a ∧ ∃ as ys zs bs, xs = as ++ (ys ++ a :: zs) :: bs ∧
         (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by
   rw [find?_eq_some]
   constructor
   · rintro ⟨h, ⟨ys, zs, h₁, h₂⟩⟩
     refine ⟨h, ?_⟩
-    rw [join_eq_append_iff] at h₁
+    rw [flatten_eq_append_iff] at h₁
     obtain (⟨as, bs, rfl, rfl, h₁⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, h₁⟩) := h₁
     · replace h₁ := h₁.symm
-      rw [join_eq_cons_iff] at h₁
+      rw [flatten_eq_cons_iff] at h₁
       obtain ⟨bs, cs, ds, rfl, h₁, rfl⟩ := h₁
       refine ⟨as ++ bs, [], cs, ds, by simp, ?_⟩
       simp
@@ -371,7 +371,7 @@ theorem find?_join_eq_some {xs : List (List α)} {p : α → Bool} {a : α} :
       · intro x m
         simpa using h₂ x (by simpa using .inr m)
   · rintro ⟨h, ⟨as, ys, zs, bs, rfl, h₁, h₂⟩⟩
-    refine ⟨h, as.join ++ ys, zs ++ bs.join, by simp, ?_⟩
+    refine ⟨h, as.flatten ++ ys, zs ++ bs.flatten, by simp, ?_⟩
     intro a m
     simp at m
     obtain ⟨l, ml, m⟩ | m := m
@@ -786,15 +786,15 @@ theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
   induction xs with simp
   | cons _ _ _ => split <;> simp_all [Option.map_or', Option.map_map]; rfl
 
-theorem findIdx?_join {l : List (List α)} {p : α → Bool} :
-    l.join.findIdx? p =
+theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
+    l.flatten.findIdx? p =
       (l.findIdx? (·.any p)).map
         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
   | cons xs l ih =>
-    simp only [join, findIdx?_append, map_take, map_cons, findIdx?, any_eq_true, Nat.zero_add,
+    simp only [flatten, findIdx?_append, map_take, map_cons, findIdx?, any_eq_true, Nat.zero_add,
       findIdx?_succ]
     split
     · simp only [Option.map_some', take_zero, sum_nil, length_cons, zero_lt_succ,
@@ -976,4 +976,13 @@ theorem IsInfix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <:+: l₂
 
 end lookup
 
+/-! ### Deprecations -/
+
+@[deprecated head_flatten (since := "2024-10-14")] abbrev head_join := @head_flatten
+@[deprecated getLast_flatten (since := "2024-10-14")] abbrev getLast_join := @getLast_flatten
+@[deprecated find?_flatten (since := "2024-10-14")] abbrev find?_join := @find?_flatten
+@[deprecated find?_flatten_eq_none (since := "2024-10-14")] abbrev find?_join_eq_none := @find?_flatten_eq_none
+@[deprecated find?_flatten_eq_some (since := "2024-10-14")] abbrev find?_join_eq_some := @find?_flatten_eq_some
+@[deprecated findIdx?_flatten (since := "2024-10-14")] abbrev findIdx?_join := @findIdx?_flatten
+
 end List

src/Init/Data/List/Impl.lean

@@ -109,12 +109,12 @@ The following operations are given `@[csimp]` replacements below:
     | x::xs, acc => by simp [bindTR.go, bind, go xs]
   exact (go as #[]).symm
 
-/-! ### join -/
+/-! ### flatten -/
 
-/-- Tail recursive version of `List.join`. -/
-@[inline] def joinTR (l : List (List α)) : List α := bindTR l id
+/-- Tail recursive version of `List.flatten`. -/
+@[inline] def flattenTR (l : List (List α)) : List α := bindTR l id
 
-@[csimp] theorem join_eq_joinTR : @join = @joinTR := by
+@[csimp] theorem flatten_eq_flattenTR : @flatten = @flattenTR := by
   funext α l; rw [← List.bind_id, List.bind_eq_bindTR]; rfl
 
 /-! ## Sublists -/
@@ -322,7 +322,7 @@ where
   | [_] => simp
   | x::y::xs =>
     let rec go {acc x} : ∀ xs,
-      intercalateTR.go sep.toArray x xs acc = acc.toList ++ join (intersperse sep (x::xs))
+      intercalateTR.go sep.toArray x xs acc = acc.toList ++ flatten (intersperse sep (x::xs))
     | [] => by simp [intercalateTR.go]
     | _::_ => by simp [intercalateTR.go, go]
     simp [intersperse, go]

src/Init/Data/List/Lemmas.lean

@@ -2068,106 +2068,98 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = concat L b
     | _, .inl rfl => .inr ⟨[], a, rfl⟩
     | _, .inr ⟨L, b, rfl⟩ => .inr ⟨a::L, b, rfl⟩
 
-/-! ### join -/
+/-! ### flatten -/
 
-@[simp] theorem length_join (L : List (List α)) : (join L).length = Nat.sum (L.map length) := by
+
+@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = Nat.sum (L.map length) := by
   induction L with
   | nil => rfl
   | cons =>
-    simp [join, length_append, *]
+    simp [flatten, length_append, *]
 
-theorem join_singleton (l : List α) : [l].join = l := by simp
+theorem flatten_singleton (l : List α) : [l].flatten = l := by simp
 
-@[simp] theorem mem_join : ∀ {L : List (List α)}, a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l
+@[simp] theorem mem_flatten : ∀ {L : List (List α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l
   | [] => by simp
-  | b :: l => by simp [mem_join, or_and_right, exists_or]
+  | b :: l => by simp [mem_flatten, or_and_right, exists_or]
 
-@[simp] theorem join_eq_nil_iff {L : List (List α)} : L.join = [] ↔ ∀ l ∈ L, l = [] := by
+@[simp] theorem flatten_eq_nil_iff {L : List (List α)} : L.flatten = [] ↔ ∀ l ∈ L, l = [] := by
   induction L <;> simp_all
 
-@[deprecated join_eq_nil_iff (since := "2024-09-05")] abbrev join_eq_nil := @join_eq_nil_iff
-
-theorem join_ne_nil_iff {xs : List (List α)} : xs.join ≠ [] ↔ ∃ x, x ∈ xs ∧ x ≠ [] := by
+theorem flatten_ne_nil_iff {xs : List (List α)} : xs.flatten ≠ [] ↔ ∃ x, x ∈ xs ∧ x ≠ [] := by
   simp
 
-@[deprecated join_ne_nil_iff (since := "2024-09-05")] abbrev join_ne_nil := @join_ne_nil_iff
+theorem exists_of_mem_flatten : a ∈ flatten L → ∃ l, l ∈ L ∧ a ∈ l := mem_flatten.1
 
-theorem exists_of_mem_join : a ∈ join L → ∃ l, l ∈ L ∧ a ∈ l := mem_join.1
+theorem mem_flatten_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ flatten L := mem_flatten.2 ⟨l, lL, al⟩
 
-theorem mem_join_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ join L := mem_join.2 ⟨l, lL, al⟩
-
-theorem forall_mem_join {p : α → Prop} {L : List (List α)} :
-    (∀ (x) (_ : x ∈ join L), p x) ↔ ∀ (l) (_ : l ∈ L) (x) (_ : x ∈ l), p x := by
-  simp only [mem_join, forall_exists_index, and_imp]
+theorem forall_mem_flatten {p : α → Prop} {L : List (List α)} :
+    (∀ (x) (_ : x ∈ flatten L), p x) ↔ ∀ (l) (_ : l ∈ L) (x) (_ : x ∈ l), p x := by
+  simp only [mem_flatten, forall_exists_index, and_imp]
   constructor <;> (intros; solve_by_elim)
 
-theorem join_eq_bind {L : List (List α)} : join L = L.bind id := by
+theorem flatten_eq_bind {L : List (List α)} : flatten L = L.bind id := by
   induction L <;> simp [List.bind]
 
-theorem head?_join {L : List (List α)} : (join L).head? = L.findSome? fun l => l.head? := by
+theorem head?_flatten {L : List (List α)} : (flatten L).head? = L.findSome? fun l => l.head? := by
   induction L with
   | nil => rfl
   | cons =>
     simp only [findSome?_cons]
     split <;> simp_all
 
--- `getLast?_join` is proved later, after the `reverse` section.
--- `head_join` and `getLast_join` are proved in `Init.Data.List.Find`.
+-- `getLast?_flatten` is proved later, after the `reverse` section.
+-- `head_flatten` and `getLast_flatten` are proved in `Init.Data.List.Find`.
 
-theorem foldl_join (f : β → α → β) (b : β) (L : List (List α)) :
-    (join L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
+theorem foldl_flatten (f : β → α → β) (b : β) (L : List (List α)) :
+    (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
   induction L generalizing b <;> simp_all
 
-theorem foldr_join (f : α → β → β) (b : β) (L : List (List α)) :
-    (join L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by
+theorem foldr_flatten (f : α → β → β) (b : β) (L : List (List α)) :
+    (flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by
   induction L <;> simp_all
 
-@[simp] theorem map_join (f : α → β) (L : List (List α)) : map f (join L) = join (map (map f) L) := by
+@[simp] theorem map_flatten (f : α → β) (L : List (List α)) : map f (flatten L) = flatten (map (map f) L) := by
   induction L <;> simp_all
 
-@[simp] theorem filterMap_join (f : α → Option β) (L : List (List α)) :
-    filterMap f (join L) = join (map (filterMap f) L) := by
+@[simp] theorem filterMap_flatten (f : α → Option β) (L : List (List α)) :
+    filterMap f (flatten L) = flatten (map (filterMap f) L) := by
   induction L <;> simp [*, filterMap_append]
 
-@[simp] theorem filter_join (p : α → Bool) (L : List (List α)) :
-    filter p (join L) = join (map (filter p) L) := by
+@[simp] theorem filter_flatten (p : α → Bool) (L : List (List α)) :
+    filter p (flatten L) = flatten (map (filter p) L) := by
   induction L <;> simp [*, filter_append]
 
-theorem join_filter_not_isEmpty  :
-    ∀ {L : List (List α)}, join (L.filter fun l => !l.isEmpty) = L.join
+theorem flatten_filter_not_isEmpty  :
+    ∀ {L : List (List α)}, flatten (L.filter fun l => !l.isEmpty) = L.flatten
   | [] => rfl
   | [] :: L
   | (a :: l) :: L => by
-      simp [join_filter_not_isEmpty (L := L)]
+      simp [flatten_filter_not_isEmpty (L := L)]
 
-theorem join_filter_ne_nil [DecidablePred fun l : List α => l ≠ []] {L : List (List α)} :
-    join (L.filter fun l => l ≠ []) = L.join := by
+theorem flatten_filter_ne_nil [DecidablePred fun l : List α => l ≠ []] {L : List (List α)} :
+    flatten (L.filter fun l => l ≠ []) = L.flatten := by
   simp only [ne_eq, ← isEmpty_iff, Bool.not_eq_true, Bool.decide_eq_false,
-    join_filter_not_isEmpty]
+    flatten_filter_not_isEmpty]
 
-@[deprecated filter_join (since := "2024-08-26")]
-theorem join_map_filter (p : α → Bool) (l : List (List α)) :
-    (l.map (filter p)).join = (l.join).filter p := by
-  rw [filter_join]
-
-@[simp] theorem join_append (L₁ L₂ : List (List α)) : join (L₁ ++ L₂) = join L₁ ++ join L₂ := by
+@[simp] theorem flatten_append (L₁ L₂ : List (List α)) : flatten (L₁ ++ L₂) = flatten L₁ ++ flatten L₂ := by
   induction L₁ <;> simp_all
 
-theorem join_concat (L : List (List α)) (l : List α) : join (L ++ [l]) = join L ++ l := by
+theorem flatten_concat (L : List (List α)) (l : List α) : flatten (L ++ [l]) = flatten L ++ l := by
   simp
 
-theorem join_join {L : List (List (List α))} : join (join L) = join (map join L) := by
+theorem flatten_flatten {L : List (List (List α))} : flatten (flatten L) = flatten (map flatten L) := by
   induction L <;> simp_all
 
-theorem join_eq_cons_iff {xs : List (List α)} {y : α} {ys : List α} :
-    xs.join = y :: ys ↔
-      ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ l, l ∈ as → l = []) ∧ ys = bs ++ cs.join := by
+theorem flatten_eq_cons_iff {xs : List (List α)} {y : α} {ys : List α} :
+    xs.flatten = y :: ys ↔
+      ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ l, l ∈ as → l = []) ∧ ys = bs ++ cs.flatten := by
   constructor
   · induction xs with
     | nil => simp
     | cons x xs ih =>
       intro h
-      simp only [join_cons] at h
+      simp only [flatten_cons] at h
       replace h := h.symm
       rw [cons_eq_append_iff] at h
       obtain (⟨rfl, h⟩ | ⟨z⟩) := h
@@ -2178,23 +2170,23 @@ theorem join_eq_cons_iff {xs : List (List α)} {y : α} {ys : List α} :
         refine ⟨[], a', xs, ?_⟩
         simp
   · rintro ⟨as, bs, cs, rfl, h₁, rfl⟩
-    simp [join_eq_nil_iff.mpr h₁]
+    simp [flatten_eq_nil_iff.mpr h₁]
 
-theorem join_eq_append_iff {xs : List (List α)} {ys zs : List α} :
-    xs.join = ys ++ zs ↔
-      (∃ as bs, xs = as ++ bs ∧ ys = as.join ∧ zs = bs.join) ∨
-        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.join ++ bs ∧
-          zs = c :: cs ++ ds.join := by
+theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} :
+    xs.flatten = ys ++ zs ↔
+      (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
+        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧
+          zs = c :: cs ++ ds.flatten := by
   constructor
   · induction xs generalizing ys with
     | nil =>
-      simp only [join_nil, nil_eq, append_eq_nil, and_false, cons_append, false_and, exists_const,
+      simp only [flatten_nil, nil_eq, append_eq_nil, and_false, cons_append, false_and, exists_const,
         exists_false, or_false, and_imp, List.cons_ne_nil]
       rintro rfl rfl
       exact ⟨[], [], by simp⟩
     | cons x xs ih =>
       intro h
-      simp only [join_cons] at h
+      simp only [flatten_cons] at h
       rw [append_eq_append_iff] at h
       obtain (⟨ys, rfl, h⟩ | ⟨c', rfl, h⟩) := h
       · obtain (⟨as, bs, rfl, rfl, rfl⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, rfl⟩) := ih h
@@ -2208,18 +2200,15 @@ theorem join_eq_append_iff {xs : List (List α)} {ys zs : List α} :
     · simp
     · simp
 
-@[deprecated join_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons := @join_eq_cons_iff
-@[deprecated join_eq_append_iff (since := "2024-09-05")] abbrev join_eq_append := @join_eq_append_iff
-
-/-- Two lists of sublists are equal iff their joins coincide, as well as the lengths of the
+/-- Two lists of sublists are equal iff their flattens coincide, as well as the lengths of the
 sublists. -/
-theorem eq_iff_join_eq : ∀ {L L' : List (List α)},
-    L = L' ↔ L.join = L'.join ∧ map length L = map length L'
+theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
+    L = L' ↔ L.flatten = L'.flatten ∧ map length L = map length L'
   | _, [] => by simp_all
   | [], x' :: L' => by simp_all
   | x :: L, x' :: L' => by
     simp
-    rw [eq_iff_join_eq]
+    rw [eq_iff_flatten_eq]
     constructor
     · rintro ⟨rfl, h₁, h₂⟩
       simp_all
@@ -2229,12 +2218,12 @@ theorem eq_iff_join_eq : ∀ {L L' : List (List α)},
 
 /-! ### bind -/
 
-theorem bind_def (l : List α) (f : α → List β) : l.bind f = join (map f l) := by rfl
+theorem bind_def (l : List α) (f : α → List β) : l.bind f = flatten (map f l) := by rfl
 
-@[simp] theorem bind_id (l : List (List α)) : List.bind l id = l.join := by simp [bind_def]
+@[simp] theorem bind_id (l : List (List α)) : List.bind l id = l.flatten := by simp [bind_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_join]
+  simp [bind_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 β} :
@@ -2245,7 +2234,7 @@ theorem mem_bind_of_mem {b : β} {l : List α} {f : α → List β} {a} (al : a
 
 @[simp]
 theorem bind_eq_nil_iff {l : List α} {f : α → List β} : List.bind l f = [] ↔ ∀ x ∈ l, f x = [] :=
-  join_eq_nil_iff.trans <| by
+  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
@@ -2483,23 +2472,23 @@ theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
     (replicate n a).filterMap f = [] := by
   simp [filterMap_replicate, h]
 
-@[simp] theorem join_replicate_nil : (replicate n ([] : List α)).join = [] := by
+@[simp] theorem flatten_replicate_nil : (replicate n ([] : List α)).flatten = [] := by
   induction n <;> simp_all [replicate_succ]
 
-@[simp] theorem join_replicate_singleton : (replicate n [a]).join = replicate n a := by
+@[simp] theorem flatten_replicate_singleton : (replicate n [a]).flatten = replicate n a := by
   induction n <;> simp_all [replicate_succ]
 
-@[simp] theorem join_replicate_replicate : (replicate n (replicate m a)).join = replicate (n * m) a := by
+@[simp] theorem flatten_replicate_replicate : (replicate n (replicate m a)).flatten = replicate (n * m) a := by
   induction n with
   | zero => simp
   | succ n ih =>
-    simp only [replicate_succ, join_cons, ih, append_replicate_replicate, replicate_inj, or_true,
+    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)).join := by
+theorem bind_replicate {β} (f : α → List β) : (replicate n a).bind f = (replicate n (f a)).flatten := by
   induction n with
   | zero => simp
-  | succ n ih => simp only [replicate_succ, bind_cons, ih, join_cons]
+  | succ n ih => simp only [replicate_succ, bind_cons, ih, flatten_cons]
 
 @[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
   cases n <;> simp [replicate_succ]
@@ -2674,14 +2663,14 @@ theorem reverse_eq_concat {xs ys : List α} {a : α} :
     xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse := by
   rw [reverse_eq_iff, reverse_concat]
 
-/-- Reversing a join is the same as reversing the order of parts and reversing all parts. -/
-theorem reverse_join (L : List (List α)) :
-    L.join.reverse = (L.map reverse).reverse.join := by
+/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts. -/
+theorem reverse_flatten (L : List (List α)) :
+    L.flatten.reverse = (L.map reverse).reverse.flatten := by
   induction L <;> simp_all
 
-/-- Joining a reverse is the same as reversing all parts and reversing the joined result. -/
-theorem join_reverse (L : List (List α)) :
-    L.reverse.join = (L.map reverse).join.reverse := by
+/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result. -/
+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
@@ -2801,8 +2790,8 @@ theorem getLast?_bind {L : List α} {f : α → List β} :
   rw [head?_bind]
   rfl
 
-theorem getLast?_join {L : List (List α)} :
-    (join L).getLast? = L.reverse.findSome? fun l => l.getLast? := by
+theorem getLast?_flatten {L : List (List α)} :
+    (flatten L).getLast? = L.reverse.findSome? fun l => l.getLast? := by
   simp [← bind_id, getLast?_bind]
 
 theorem getLast?_replicate (a : α) (n : Nat) : (replicate n a).getLast? = if n = 0 then none else some a := by
@@ -3302,12 +3291,16 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
   | nil => rfl
   | cons h t ih => simp_all [Bool.and_assoc]
 
-@[simp] theorem any_join {l : List (List α)} : l.join.any f = l.any (any · f) := by
+@[simp] theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f) := by
   induction l <;> simp_all
 
-@[simp] theorem all_join {l : List (List α)} : l.join.all f = l.all (all · f) := by
+@[deprecated any_flatten (since := "2024-10-14")] abbrev any_join := @any_flatten
+
+@[simp] theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f) := by
   induction l <;> simp_all
 
+@[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
   induction l <;> simp_all
@@ -3338,4 +3331,47 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
     (l.insert a).all f = (f a && l.all f) := by
   simp [all_eq]
 
+/-! ### Deprecations -/
+
+
+@[deprecated flatten_nil (since := "2024-10-14")] abbrev join_nil := @flatten_nil
+@[deprecated flatten_cons (since := "2024-10-14")] abbrev join_cons := @flatten_cons
+@[deprecated length_flatten (since := "2024-10-14")] abbrev length_join := @length_flatten
+@[deprecated flatten_singleton (since := "2024-10-14")] abbrev join_singleton := @flatten_singleton
+@[deprecated mem_flatten (since := "2024-10-14")] abbrev mem_join := @mem_flatten
+@[deprecated flatten_eq_nil_iff (since := "2024-09-05")] abbrev join_eq_nil := @flatten_eq_nil_iff
+@[deprecated flatten_eq_nil_iff (since := "2024-10-14")] abbrev join_eq_nil_iff := @flatten_eq_nil_iff
+@[deprecated flatten_ne_nil_iff (since := "2024-09-05")] abbrev join_ne_nil := @flatten_ne_nil_iff
+@[deprecated flatten_ne_nil_iff (since := "2024-10-14")] abbrev join_ne_nil_iff := @flatten_ne_nil_iff
+@[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 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
+@[deprecated map_flatten (since := "2024-10-14")] abbrev map_join := @map_flatten
+@[deprecated filterMap_flatten (since := "2024-10-14")] abbrev filterMap_join := @filterMap_flatten
+@[deprecated filter_flatten (since := "2024-10-14")] abbrev filter_join := @filter_flatten
+@[deprecated flatten_filter_not_isEmpty (since := "2024-10-14")] abbrev join_filter_not_isEmpty := @flatten_filter_not_isEmpty
+@[deprecated flatten_filter_ne_nil (since := "2024-10-14")] abbrev join_filter_ne_nil := @flatten_filter_ne_nil
+@[deprecated filter_flatten (since := "2024-08-26")]
+theorem join_map_filter (p : α → Bool) (l : List (List α)) :
+    (l.map (filter p)).flatten = (l.flatten).filter p := by
+  rw [filter_flatten]
+@[deprecated flatten_append (since := "2024-10-14")] abbrev join_append := @flatten_append
+@[deprecated flatten_concat (since := "2024-10-14")] abbrev join_concat := @flatten_concat
+@[deprecated flatten_flatten (since := "2024-10-14")] abbrev join_join := @flatten_flatten
+@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons_iff := @flatten_eq_cons_iff
+@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons := @flatten_eq_cons_iff
+@[deprecated flatten_eq_append_iff (since := "2024-09-05")] abbrev join_eq_append := @flatten_eq_append_iff
+@[deprecated flatten_eq_append_iff (since := "2024-10-14")] abbrev join_eq_append_iff := @flatten_eq_append_iff
+@[deprecated eq_iff_flatten_eq (since := "2024-10-14")] abbrev eq_iff_join_eq := @eq_iff_flatten_eq
+@[deprecated flatten_replicate_nil (since := "2024-10-14")] abbrev join_replicate_nil := @flatten_replicate_nil
+@[deprecated flatten_replicate_singleton (since := "2024-10-14")] abbrev join_replicate_singleton := @flatten_replicate_singleton
+@[deprecated flatten_replicate_replicate (since := "2024-10-14")] abbrev join_replicate_replicate := @flatten_replicate_replicate
+@[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
+
 end List

src/Init/Data/List/Pairwise.lean

@@ -160,21 +160,23 @@ theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x
   rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
   simp only [mem_append, or_comm]
 
-theorem pairwise_join {L : List (List α)} :
-    Pairwise R (join L) ↔
+theorem pairwise_flatten {L : List (List α)} :
+    Pairwise R (flatten L) ↔
       (∀ l ∈ L, Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, R x y) L := by
   induction L with
   | nil => simp
   | cons l L IH =>
-    simp only [join, pairwise_append, IH, mem_join, exists_imp, and_imp, forall_mem_cons,
+    simp only [flatten, pairwise_append, IH, mem_flatten, exists_imp, and_imp, forall_mem_cons,
       pairwise_cons, and_assoc, and_congr_right_iff]
     rw [and_comm, and_congr_left_iff]
     intros; exact ⟨fun h a b c d e => h c d e a b, fun h c d e a b => h a b c d e⟩
 
+@[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) ↔
       (∀ 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_join, pairwise_map]
+  simp [List.bind, pairwise_flatten, pairwise_map]
 
 theorem pairwise_reverse {l : List α} :
     l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a) := by

src/Init/Data/List/Perm.lean

@@ -461,15 +461,17 @@ theorem Perm.nodup {l l' : List α} (hl : l ~ l') (hR : l.Nodup) : l'.Nodup := h
 theorem Perm.nodup_iff {l₁ l₂ : List α} : l₁ ~ l₂ → (Nodup l₁ ↔ Nodup l₂) :=
   Perm.pairwise_iff <| @Ne.symm α
 
-theorem Perm.join {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.join ~ l₂.join := by
+theorem Perm.flatten {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatten ~ l₂.flatten := by
   induction h with
   | nil => rfl
-  | cons _ _ ih => simp only [join_cons, perm_append_left_iff, ih]
-  | swap => simp only [join_cons, ← append_assoc, perm_append_right_iff]; exact perm_append_comm ..
+  | cons _ _ ih => simp only [flatten_cons, perm_append_left_iff, ih]
+  | swap => simp only [flatten_cons, ← append_assoc, perm_append_right_iff]; exact perm_append_comm ..
   | trans _ _ ih₁ ih₂ => exact trans ih₁ ih₂
 
+@[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 :=
-  (p.map _).join
+  (p.map _).flatten
 
 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

src/Init/Data/List/Sublist.lean

@@ -483,30 +483,30 @@ theorem sublist_replicate_iff : l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = re
       rw [w]
       exact (replicate_sublist_replicate a).2 le
 
-theorem sublist_join_of_mem {L : List (List α)} {l} (h : l ∈ L) : l <+ L.join := by
+theorem sublist_flatten_of_mem {L : List (List α)} {l} (h : l ∈ L) : l <+ L.flatten := by
   induction L with
   | nil => cases h
   | cons l' L ih =>
     rcases mem_cons.1 h with (rfl | h)
     · simp [h]
-    · simp [ih h, join_cons, sublist_append_of_sublist_right]
+    · simp [ih h, flatten_cons, sublist_append_of_sublist_right]
 
-theorem sublist_join_iff {L : List (List α)} {l} :
-    l <+ L.join ↔
-      ∃ L' : List (List α), l = L'.join ∧ ∀ i (_ : i < L'.length), L'[i] <+ L[i]?.getD [] := by
+theorem sublist_flatten_iff {L : List (List α)} {l} :
+    l <+ L.flatten ↔
+      ∃ L' : List (List α), l = L'.flatten ∧ ∀ i (_ : i < L'.length), L'[i] <+ L[i]?.getD [] := by
   induction L generalizing l with
   | nil =>
     constructor
     · intro w
-      simp only [join_nil, sublist_nil] at w
+      simp only [flatten_nil, sublist_nil] at w
       subst w
       exact ⟨[], by simp, fun i x => by cases x⟩
     · rintro ⟨L', rfl, h⟩
-      simp only [join_nil, sublist_nil, join_eq_nil_iff]
+      simp only [flatten_nil, sublist_nil, flatten_eq_nil_iff]
       simp only [getElem?_nil, Option.getD_none, sublist_nil] at h
       exact (forall_getElem (p := (· = []))).1 h
   | cons l' L ih =>
-    simp only [join_cons, sublist_append_iff, ih]
+    simp only [flatten_cons, sublist_append_iff, ih]
     constructor
     · rintro ⟨l₁, l₂, rfl, s, L', rfl, h⟩
       refine ⟨l₁ :: L', by simp, ?_⟩
@@ -517,21 +517,21 @@ theorem sublist_join_iff {L : List (List α)} {l} :
       | nil =>
         exact ⟨[], [], by simp, by simp, [], by simp, fun i x => by cases x⟩
       | cons l₁ L' =>
-        exact ⟨l₁, L'.join, by simp, by simpa using h 0 (by simp), L', rfl,
+        exact ⟨l₁, L'.flatten, by simp, by simpa using h 0 (by simp), L', rfl,
           fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)⟩
 
-theorem join_sublist_iff {L : List (List α)} {l} :
-    L.join <+ l ↔
-      ∃ L' : List (List α), l = L'.join ∧ ∀ i (_ : i < L.length), L[i] <+ L'[i]?.getD [] := by
+theorem flatten_sublist_iff {L : List (List α)} {l} :
+    L.flatten <+ l ↔
+      ∃ L' : List (List α), l = L'.flatten ∧ ∀ i (_ : i < L.length), L[i] <+ L'[i]?.getD [] := by
   induction L generalizing l with
   | nil =>
     constructor
     · intro _
       exact ⟨[l], by simp, fun i x => by cases x⟩
     · rintro ⟨L', rfl, _⟩
-      simp only [join_nil, nil_sublist]
+      simp only [flatten_nil, nil_sublist]
   | cons l' L ih =>
-    simp only [join_cons, append_sublist_iff, ih]
+    simp only [flatten_cons, append_sublist_iff, ih]
     constructor
     · rintro ⟨l₁, l₂, rfl, s, L', rfl, h⟩
       refine ⟨l₁ :: L', by simp, ?_⟩
@@ -543,7 +543,7 @@ theorem join_sublist_iff {L : List (List α)} {l} :
         exact ⟨[], [], by simp, by simpa using h 0 (by simp), [], by simp,
           fun i x => by simpa using h (i+1) (Nat.add_lt_add_right x 1)⟩
       | cons l₁ L' =>
-        exact ⟨l₁, L'.join, by simp, by simpa using h 0 (by simp), L', rfl,
+        exact ⟨l₁, L'.flatten, by simp, by simpa using h 0 (by simp), L', rfl,
           fun i lt => by simpa using h (i+1) (Nat.add_lt_add_right lt 1)⟩
 
 @[simp] theorem isSublist_iff_sublist [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
@@ -938,12 +938,12 @@ theorem isInfix_replicate_iff {n} {a : α} {l : List α} :
     · simpa using Nat.sub_add_cancel h
     · simpa using w
 
-theorem infix_of_mem_join : ∀ {L : List (List α)}, l ∈ L → l <:+: join L
+theorem infix_of_mem_flatten : ∀ {L : List (List α)}, l ∈ L → l <:+: flatten L
   | l' :: _, h =>
     match h with
     | List.Mem.head .. => infix_append [] _ _
     | List.Mem.tail _ hlMemL =>
-      IsInfix.trans (infix_of_mem_join hlMemL) <| (suffix_append _ _).isInfix
+      IsInfix.trans (infix_of_mem_flatten hlMemL) <| (suffix_append _ _).isInfix
 
 theorem prefix_append_right_inj (l) : l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂ :=
   exists_congr fun r => by rw [append_assoc, append_right_inj]
@@ -1087,4 +1087,11 @@ theorem prefix_iff_eq_take : l₁ <+: l₂ ↔ l₁ = take (length l₁) l₂ :=
 
 -- See `Init.Data.List.Nat.Sublist` for `suffix_iff_eq_append`, `prefix_take_iff`, and `suffix_iff_eq_drop`.
 
+/-! ### Deprecations -/
+
+@[deprecated sublist_flatten_of_mem (since := "2024-10-14")] abbrev sublist_join_of_mem := @sublist_flatten_of_mem
+@[deprecated sublist_flatten_iff (since := "2024-10-14")] abbrev sublist_join_iff := @sublist_flatten_iff
+@[deprecated flatten_sublist_iff (since := "2024-10-14")] abbrev flatten_join_iff := @flatten_sublist_iff
+@[deprecated infix_of_mem_flatten (since := "2024-10-14")] abbrev infix_of_mem_join := @infix_of_mem_flatten
+
 end List

src/Init/Data/String/Extra.lean

@@ -121,7 +121,7 @@ def toUTF8 (a : @& String) : ByteArray :=
 
 @[simp] theorem size_toUTF8 (s : String) : s.toUTF8.size = s.utf8ByteSize := by
   simp [toUTF8, ByteArray.size, Array.size, utf8ByteSize, List.bind]
-  induction s.data <;> simp [List.map, List.join, utf8ByteSize.go, Nat.add_comm, *]
+  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) -/
 @[extern "lean_string_get_byte_fast"]

src/Lean/Data/Trie.lean

@@ -76,7 +76,7 @@ partial def upsert (t : Trie α) (s : String) (f : Option α → α) : Trie α :
         let c := s.getUtf8Byte i h
         if c == c'
         then node1 v c' (loop (i + 1) t')
-        else 
+        else
           let t := insertEmpty (i + 1)
           node v (.mk #[c, c']) #[t, t']
       else
@@ -190,7 +190,7 @@ private partial def toStringAux {α : Type} : Trie α → List Format
   | node1 _ c t =>
     [ format (repr c), Format.group $ Format.nest 4 $ flip Format.joinSep Format.line $ toStringAux t ]
   | node _ cs ts =>
-    List.join $ List.zipWith (fun c t =>
+    List.flatten $ List.zipWith (fun c t =>
       [ format (repr c), (Format.group $ Format.nest 4 $ flip Format.joinSep Format.line $ toStringAux t) ]
     ) cs.toList ts.toList
 

src/Lean/Elab/Deriving/FromToJson.lean

@@ -36,7 +36,7 @@ def mkToJsonBodyForStruct (header : Header) (indName : Name) : TermElabM Term :=
     let target := mkIdent header.targetNames[0]!
     if isOptField then ``(opt $nm $target.$(mkIdent field))
     else ``([($nm, toJson ($target).$(mkIdent field))])
-  `(mkObj <| List.join [$fields,*])
+  `(mkObj <| List.flatten [$fields,*])
 
 def mkToJsonBodyForInduct (ctx : Context) (header : Header) (indName : Name) : TermElabM Term := do
   let indVal ← getConstInfoInduct indName

src/Lean/Elab/Inductive.lean

@@ -770,7 +770,7 @@ private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array Ind
   forallBoundedTelescope indTypes[0]!.type numParams fun params type => do
     let otherTypes ← indTypes[1:].toArray.mapM fun indType => do whnfD (← instantiateForall indType.type params)
     let ctorTypes ← indTypes.toList.mapM fun indType => indType.ctors.mapM fun ctor => do whnfD (← instantiateForall ctor.type params)
-    let typesToCheck := otherTypes.toList ++ ctorTypes.join
+    let typesToCheck := otherTypes.toList ++ ctorTypes.flatten
     let rec go (i : Nat) (type : Expr) (typesToCheck : List Expr) : MetaM Nat := do
       if i < mask.size then
         if !masks.all fun mask => i < mask.size && mask[i]! then

src/Lean/Meta/Tactic/Backtrack.lean

@@ -167,7 +167,7 @@ private partial def processIndependentGoals (orig : List MVarId) (goals remainin
     -- and the new subgoals generated from goals on which it is successful.
     let (failed, newSubgoals') ← tryAllM igs fun g =>
       run cfg trace next orig cfg.maxDepth [g] []
-    let newSubgoals := newSubgoals'.join
+    let newSubgoals := newSubgoals'.flatten
     withTraceNode trace
       (fun _ => return m!"failed: {← ppMVarIds failed}, new: {← ppMVarIds newSubgoals}") do
     -- Update the list of goals with respect to which we need to check independence.

src/Lean/Server/InfoUtils.lean

@@ -65,7 +65,7 @@ def InfoTree.visitM' [Monad m]
 /--
   Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves). -/
 def InfoTree.collectNodesBottomUp (p : ContextInfo → Info → PersistentArray InfoTree → List α → List α) (i : InfoTree) : List α :=
-  i.visitM (m := Id) (postNode := fun ci i cs as => p ci i cs (as.filterMap id).join) |>.getD []
+  i.visitM (m := Id) (postNode := fun ci i cs as => p ci i cs (as.filterMap id).flatten) |>.getD []
 
 /--
   For every branch of the `InfoTree`, find the deepest node in that branch for which `p` returns