finish

src/Init/Data/Array/Find.lean

@@ -99,11 +99,6 @@ theorem getElem_zero_flatten {xss : Array (Array α)} (h) :
   simp [getElem?_eq_getElem, h] at t
   simp [← t]
 
-theorem back?_flatten {xss : Array (Array α)} :
-    (flatten xss).back? = (xss.findSomeRev? fun xs => xs.back?) := by
-  cases xss using array₂_induction
-  simp [List.getLast?_flatten, ← List.map_reverse, List.findSome?_map, Function.comp_def]
-
 theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by
   simp [← List.toArray_replicate, List.findSome?_replicate]
 

src/Init/Data/Array/Lemmas.lean

@@ -8,6 +8,7 @@ import Init.Data.Nat.Lemmas
 import Init.Data.List.Range
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
+import Init.Data.List.Nat.Basic
 import Init.Data.List.Monadic
 import Init.Data.List.OfFn
 import Init.Data.Array.Mem
@@ -60,21 +61,27 @@ theorem size_empty : (#[] : Array α).size = 0 := rfl
 
 /-! ### size -/
 
-theorem eq_empty_of_size_eq_zero (h : l.size = 0) : l = #[] := by
-  cases l
+theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
+  cases xs
   simp_all
 
-theorem ne_empty_of_size_eq_add_one (h : l.size = n + 1) : l ≠ #[] := by
-  cases l
+theorem ne_empty_of_size_eq_add_one (h : xs.size = n + 1) : xs ≠ #[] := by
+  cases xs
   simpa using List.ne_nil_of_length_eq_add_one h
 
-theorem ne_empty_of_size_pos (h : 0 < l.size) : l ≠ #[] := by
-  cases l
+theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
+  cases xs
   simpa using List.ne_nil_of_length_pos h
 
-theorem size_eq_zero : l.size = 0 ↔ l = #[] :=
+theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
   ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
 
+@[deprecated size_eq_zero_iff (since := "2025-02-24")]
+abbrev size_eq_zero := @size_eq_zero_iff
+
+theorem eq_empty_iff_size_eq_zero : xs = #[] ↔ xs.size = 0 :=
+  size_eq_zero_iff.symm
+
 theorem size_pos_of_mem {a : α} {xs : Array α} (h : a ∈ xs) : 0 < xs.size := by
   cases xs
   simp only [mem_toArray] at h
@@ -91,12 +98,18 @@ theorem exists_mem_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
   cases xs
   simpa using List.exists_mem_of_length_eq_add_one h
 
-theorem size_pos {xs : Array α} : 0 < xs.size ↔ xs ≠ #[] :=
-  Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero)
+theorem size_pos_iff {xs : Array α} : 0 < xs.size ↔ xs ≠ #[] :=
+  Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero_iff)
 
-theorem size_eq_one {xs : Array α} : xs.size = 1 ↔ ∃ a, xs = #[a] := by
+@[deprecated size_pos_iff (since := "2025-02-24")]
+abbrev size_pos := @size_pos_iff
+
+theorem size_eq_one_iff {xs : Array α} : xs.size = 1 ↔ ∃ a, xs = #[a] := by
   cases xs
-  simpa using List.length_eq_one
+  simpa using List.length_eq_one_iff
+
+@[deprecated size_eq_one_iff (since := "2025-02-24")]
+abbrev size_eq_one := @size_eq_one_iff
 
 /-! ### push -/
 
@@ -153,7 +166,7 @@ theorem ne_empty_iff_exists_push {xs : Array α} :
 
 theorem exists_push_of_size_pos {xs : Array α} (h : 0 < xs.size) :
     ∃ (ys : Array α) (a : α), xs = ys.push a := by
-  replace h : xs ≠ #[] := size_pos.mp h
+  replace h : xs ≠ #[] := size_pos_iff.mp h
   exact exists_push_of_ne_empty h
 
 theorem size_pos_iff_exists_push {xs : Array α} :
@@ -440,7 +453,7 @@ abbrev isEmpty_eq_true := @isEmpty_iff
 abbrev isEmpty_eq_false := @isEmpty_eq_false_iff
 
 theorem isEmpty_iff_size_eq_zero {xs : Array α} : xs.isEmpty ↔ xs.size = 0 := by
-  rw [isEmpty_iff, size_eq_zero]
+  rw [isEmpty_iff, size_eq_zero_iff]
 
 /-! ### Decidability of bounded quantifiers -/
 
@@ -1023,6 +1036,20 @@ private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a ==
   cases ys
   simp
 
+/-! ### back -/
+
+theorem back_eq_getElem (xs : Array α) (h : 0 < xs.size) : xs.back = xs[xs.size - 1] := by
+  cases xs
+  simp [List.getLast_eq_getElem]
+
+theorem back?_eq_getElem? (xs : Array α) : xs.back? = xs[xs.size - 1]? := by
+  cases xs
+  simp [List.getLast?_eq_getElem?]
+
+@[simp] theorem back_mem {xs : Array α} (h : 0 < xs.size) : xs.back h ∈ xs := by
+  cases xs
+  simp
+
 /-! ### map -/
 
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (xs : Array α) :
@@ -1397,6 +1424,18 @@ theorem filter_eq_push_iff {p : α → Bool} {xs ys : Array α} {a : α} :
 theorem mem_of_mem_filter {a : α} {xs : Array α} (h : a ∈ filter p xs) : a ∈ xs :=
   (mem_filter.mp h).1
 
+@[simp]
+theorem size_filter_pos_iff {xs : Array α} {p : α → Bool} :
+    0 < (filter p xs).size ↔ ∃ x ∈ xs, p x := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp]
+theorem size_filter_lt_size_iff_exists {xs : Array α} {p : α → Bool} :
+    (filter p xs).size < xs.size ↔ ∃ x ∈ xs, ¬p x := by
+  rcases xs with ⟨xs⟩
+  simp
+
 /-! ### filterMap -/
 
 @[congr]
@@ -1563,6 +1602,18 @@ theorem filterMap_eq_push_iff {f : α → Option β} {xs : Array α} {ys : Array
   · rintro ⟨⟨l₁⟩, a, ⟨l₂⟩, h₁, h₂, h₃, h₄⟩
     refine ⟨l₂.reverse, a, l₁.reverse, by simp_all⟩
 
+@[simp]
+theorem size_filterMap_pos_iff {xs : Array α} {f : α → Option β} :
+    0 < (filterMap f xs).size ↔ ∃ (x : α) (_ : x ∈ xs) (b : β), f x = some b := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp]
+theorem size_filterMap_lt_size_iff_exists {xs : Array α} {f : α → Option β} :
+    (filterMap f xs).size < xs.size ↔ ∃ (x : α) (_ : x ∈ xs), f x = none := by
+  rcases xs with ⟨xs⟩
+  simp
+
 /-! ### singleton -/
 
 @[simp] theorem singleton_def (v : α) : Array.singleton v = #[v] := rfl
@@ -3185,6 +3236,106 @@ theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} (r : β
   rcases xs with ⟨xs⟩
   simp
 
+/-! #### Further results about `back` and `back?` -/
+
+@[simp] theorem back?_eq_none_iff {xs : Array α} : xs.back? = none ↔ xs = #[] := by
+  simp only [back?_eq_getElem?, ← size_eq_zero_iff]
+  simp only [_root_.getElem?_eq_none_iff]
+  omega
+
+theorem back?_eq_some_iff {xs : Array α} {a : α} :
+    xs.back? = some a ↔ ∃ ys : Array α, xs = ys.push a := by
+  rcases xs with ⟨xs⟩
+  simp only [List.back?_toArray, List.getLast?_eq_some_iff, toArray_eq, push_toList]
+  constructor
+  · rintro ⟨ys, rfl⟩
+    exact ⟨ys.toArray, by simp⟩
+  · rintro ⟨ys, rfl⟩
+    exact ⟨ys.toList, by simp⟩
+
+@[simp] theorem back?_isSome : xs.back?.isSome ↔ xs ≠ #[] := by
+  cases xs
+  simp
+
+theorem mem_of_back? {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs := by
+  obtain ⟨ys, rfl⟩ := back?_eq_some_iff.1 h
+  simp
+
+@[simp] theorem back_append_of_size_pos {xs ys : Array α} {h₁} (h₂ : 0 < ys.size) :
+    (xs ++ ys).back h₁ = ys.back h₂ := by
+  rcases xs with ⟨l⟩
+  rcases ys with ⟨l'⟩
+  simp only [List.append_toArray, List.back_toArray]
+  rw [List.getLast_append_of_ne_nil]
+
+theorem back_append {xs : Array α} (h : 0 < (xs ++ ys).size) :
+    (xs ++ ys).back h =
+      if h' : ys.isEmpty then
+        xs.back (by simp_all)
+      else
+        ys.back (by simp only [isEmpty_iff, eq_empty_iff_size_eq_zero] at h'; omega) := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [List.append_toArray, List.back_toArray, List.getLast_append, List.isEmpty_iff,
+    List.isEmpty_toArray]
+  split
+  · rw [dif_pos]
+    simpa only [List.isEmpty_toArray]
+  · rw [dif_neg]
+    simpa only [List.isEmpty_toArray]
+
+theorem back_append_right {xs ys : Array α} (h : 0 < ys.size) :
+    (xs ++ ys).back (by simp; omega) = ys.back h := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [List.append_toArray, List.back_toArray]
+  rw [List.getLast_append_right]
+
+theorem back_append_left {xs ys : Array α} (w : 0 < (xs ++ ys).size) (h : ys.size = 0) :
+    (xs ++ ys).back w = xs.back (by simp_all) := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [List.append_toArray, List.back_toArray]
+  rw [List.getLast_append_left]
+  simpa using h
+
+@[simp] theorem back?_append {xs ys : Array α} : (xs ++ ys).back? = ys.back?.or xs.back? := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [List.append_toArray, List.back?_toArray]
+  rw [List.getLast?_append]
+
+theorem back_filter_of_pos {p : α → Bool} {xs : Array α} (w : 0 < xs.size) (h : p (back xs w) = true) :
+    (filter p xs).back (by simpa using ⟨_, by simp, h⟩) = xs.back w := by
+  rcases xs with ⟨xs⟩
+  simp only [List.back_toArray] at h
+  simp only [List.size_toArray, List.filter_toArray', List.back_toArray]
+  rw [List.getLast_filter_of_pos _ h]
+
+theorem back_filterMap_of_eq_some {f : α → Option β} {xs : Array α} {w : 0 < xs.size} {b : β} (h : f (xs.back w) = some b) :
+    (filterMap f xs).back (by simpa using ⟨_, by simp, b, h⟩) = some b := by
+  rcases xs with ⟨xs⟩
+  simp only [List.back_toArray] at h
+  simp only [List.size_toArray, List.filterMap_toArray', List.back_toArray]
+  rw [List.getLast_filterMap_of_eq_some h]
+
+theorem back?_flatMap {xs : Array α} {f : α → Array β} :
+    (xs.flatMap f).back? = xs.reverse.findSome? fun a => (f a).back? := by
+  rcases xs with ⟨xs⟩
+  simp [List.getLast?_flatMap]
+
+theorem back?_flatten {xss : Array (Array α)} :
+    (flatten xss).back? = xss.reverse.findSome? fun xs => xs.back? := by
+  simp [← flatMap_id, back?_flatMap]
+
+theorem back?_mkArray (a : α) (n : Nat) :
+    (mkArray n a).back? = if n = 0 then none else some a := by
+  rw [mkArray_eq_toArray_replicate]
+  simp only [List.back?_toArray, List.getLast?_replicate]
+
+@[simp] theorem back_mkArray (w : 0 < n) : (mkArray n a).back (by simpa using w) = a := by
+  simp [back_eq_getElem]
+
 /-! ## Additional operations -/
 
 /-! ### leftpad -/
@@ -3376,10 +3527,6 @@ theorem back!_eq_back? [Inhabited α] (xs : Array α) : xs.back! = xs.back?.getD
 @[simp] theorem back!_push [Inhabited α] (xs : Array α) : (xs.push x).back! = x := by
   simp [back!_eq_back?]
 
-theorem mem_of_back? {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs := by
-  cases xs
-  simpa using List.mem_of_getLast? (by simpa using h)
-
 @[deprecated mem_of_back? (since := "2024-10-21")] abbrev mem_of_back?_eq_some := @mem_of_back?
 
 theorem getElem?_push_lt (xs : Array α) (x : α) (i : Nat) (h : i < xs.size) :

src/Init/Data/Array/Range.lean

@@ -31,7 +31,7 @@ theorem range'_succ (s n step) : range' s (n + 1) step = #[s] ++ range' (s + ste
   simp [List.range'_succ]
 
 @[simp] theorem range'_eq_empty_iff : range' s n step = #[] ↔ n = 0 := by
-  rw [← size_eq_zero, size_range']
+  rw [← size_eq_zero_iff, size_range']
 
 theorem range'_ne_empty_iff (s : Nat) {n step : Nat} : range' s n step ≠ #[] ↔ n ≠ 0 := by
   cases n <;> simp
@@ -136,7 +136,7 @@ theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) :=
   rw [range_eq_range', map_add_range']; rfl
 
 @[simp] theorem range_eq_empty_iff {n : Nat} : range n = #[] ↔ n = 0 := by
-  rw [← size_eq_zero, size_range]
+  rw [← size_eq_zero_iff, size_range]
 
 theorem range_ne_empty_iff {n : Nat} : range n ≠ #[] ↔ n ≠ 0 := by
   cases n <;> simp

src/Init/Data/List/Attach.lean

@@ -190,7 +190,7 @@ theorem length_attachWith {p : α → Prop} {l H} : length (l.attachWith p H) =
 
 @[simp]
 theorem pmap_eq_nil_iff {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = [] ↔ l = [] := by
-  rw [← length_eq_zero, length_pmap, length_eq_zero]
+  rw [← length_eq_zero_iff, length_pmap, length_eq_zero_iff]
 
 theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : List α}
     (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ [] := by

src/Init/Data/List/Count.lean

@@ -87,7 +87,7 @@ theorem countP_le_length : countP p l ≤ l.length := by
   countP_pos_iff
 
 @[simp] theorem countP_eq_zero {p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by
-  simp only [countP_eq_length_filter, length_eq_zero, filter_eq_nil_iff]
+  simp only [countP_eq_length_filter, length_eq_zero_iff, filter_eq_nil_iff]
 
 @[simp] theorem countP_eq_length {p} : countP p l = l.length ↔ ∀ a ∈ l, p a := by
   rw [countP_eq_length_filter, filter_length_eq_length]

src/Init/Data/List/Erase.lean

@@ -137,7 +137,7 @@ theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (erase
 @[simp] theorem eraseP_eq_self_iff {p} {l : List α} : l.eraseP p = l ↔ ∀ a ∈ l, ¬ p a := by
   rw [← Sublist.length_eq (eraseP_sublist l), length_eraseP]
   split <;> rename_i h
-  · simp only [any_eq_true, length_eq_zero] at h
+  · simp only [any_eq_true, length_eq_zero_iff] at h
     constructor
     · intro; simp_all [Nat.sub_one_eq_self]
     · intro; obtain ⟨x, m, h⟩ := h; simp_all

src/Init/Data/List/Lemmas.lean

@@ -96,9 +96,15 @@ theorem ne_nil_of_length_eq_add_one (_ : length l = n + 1) : l ≠ [] := fun _ =
 
 theorem ne_nil_of_length_pos (_ : 0 < length l) : l ≠ [] := fun _ => nomatch l
 
-@[simp] theorem length_eq_zero : length l = 0 ↔ l = [] :=
+@[simp] theorem length_eq_zero_iff : length l = 0 ↔ l = [] :=
   ⟨eq_nil_of_length_eq_zero, fun h => h ▸ rfl⟩
 
+@[deprecated length_eq_zero_iff (since := "2025-02-24")]
+abbrev length_eq_zero := @length_eq_zero_iff
+
+theorem eq_nil_iff_length_eq_zero : l = [] ↔ length l = 0 :=
+  length_eq_zero_iff.symm
+
 theorem length_pos_of_mem {a : α} : ∀ {l : List α}, a ∈ l → 0 < length l
   | _::_, _ => Nat.zero_lt_succ _
 
@@ -123,12 +129,21 @@ theorem exists_cons_of_length_eq_add_one :
     ∀ {l : List α}, l.length = n + 1 → ∃ h t, l = h :: t
   | _::_, _ => ⟨_, _, rfl⟩
 
-theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
-  Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero)
+theorem length_pos_iff {l : List α} : 0 < length l ↔ l ≠ [] :=
+  Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero_iff)
 
-theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
+@[deprecated length_pos_iff (since := "2025-02-24")]
+abbrev length_pos := @length_pos_iff
+
+theorem ne_nil_iff_length_pos {l : List α} : l ≠ [] ↔ 0 < length l :=
+  length_pos_iff.symm
+
+theorem length_eq_one_iff {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
   ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
 
+@[deprecated length_eq_one_iff (since := "2025-02-24")]
+abbrev length_eq_one := @length_eq_one_iff
+
 /-! ### cons -/
 
 theorem cons_ne_nil (a : α) (l : List α) : a :: l ≠ [] := nofun
@@ -284,7 +299,7 @@ such a rewrite, with `rw [getElem_of_eq h]`.
 theorem getElem_of_eq {l l' : List α} (h : l = l') {i : Nat} (w : i < l.length) :
     l[i] = l'[i]'(h ▸ w) := by cases h; rfl
 
-theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_pos.mp h) :=
+theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_pos_iff.mp h) :=
   match l, h with
   | _ :: _, _ => rfl
 
@@ -375,7 +390,7 @@ theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a ∈ xs) :
 theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _
 
 theorem exists_mem_of_ne_nil (l : List α) (h : l ≠ []) : ∃ x, x ∈ l :=
-  exists_mem_of_length_pos (length_pos.2 h)
+  exists_mem_of_length_pos (length_pos_iff.2 h)
 
 theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := by
   cases l <;> simp [-not_or]
@@ -533,7 +548,7 @@ theorem isEmpty_eq_false_iff_exists_mem {xs : List α} :
   cases xs <;> simp
 
 theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 := by
-  rw [isEmpty_iff, length_eq_zero]
+  rw [isEmpty_iff, length_eq_zero_iff]
 
 /-! ### any / all -/
 
@@ -910,13 +925,13 @@ theorem head?_eq_getElem? : ∀ l : List α, head? l = l[0]?
   | [] => rfl
   | a :: l => by simp
 
-theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_pos.mpr h) := by
+theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_pos_iff.mpr h) := by
   cases l with
   | nil => simp at h
   | cons _ _ => simp
 
 theorem getElem_zero_eq_head (l : List α) (h : 0 < l.length) :
-    l[0] = head l (by simpa [length_pos] using h) := by
+    l[0] = head l (by simpa [length_pos_iff] using h) := by
   cases l with
   | nil => simp at h
   | cons _ _ => simp
@@ -1003,7 +1018,7 @@ theorem one_lt_length_of_tail_ne_nil {l : List α} (h : l.tail ≠ []) : 1 < l.l
   | nil => simp at h
   | cons _ l =>
     simp only [tail_cons, ne_eq] at h
-    exact Nat.lt_add_of_pos_left (length_pos.mpr h)
+    exact Nat.lt_add_of_pos_left (length_pos_iff.mpr h)
 
 @[simp] theorem head_tail (l : List α) (h : l.tail ≠ []) :
     (tail l).head h = l[1]'(one_lt_length_of_tail_ne_nil h) := by
@@ -3417,7 +3432,7 @@ theorem get_cons_succ {as : List α} {h : i + 1 < (a :: as).length} :
 theorem get_cons_succ' {as : List α} {i : Fin as.length} :
   (a :: as).get i.succ = as.get i := rfl
 
-theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos.mp h)
+theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos_iff.mp h)
   | _::_, _ => rfl
 
 set_option linter.deprecated false in

src/Init/Data/List/Nat/Basic.lean

@@ -44,10 +44,42 @@ theorem tail_dropLast (l : List α) : tail (dropLast l) = dropLast (tail l) := b
 
 /-! ### filter -/
 
-theorem length_filter_lt_length_iff_exists {l} :
-    length (filter p l) < length l ↔ ∃ x ∈ l, ¬p x := by
+@[simp]
+theorem length_filter_pos_iff {l : List α} {p : α → Bool} :
+    0 < (filter p l).length ↔ ∃ x ∈ l, p x := by
   simpa [length_eq_countP_add_countP p l, countP_eq_length_filter] using
-    countP_pos_iff (p := fun x => ¬p x)
+    countP_pos_iff (p := p)
+
+@[simp]
+theorem length_filter_lt_length_iff_exists {l} :
+    (filter p l).length < l.length ↔ ∃ x ∈ l, ¬p x := by
+  simp [length_eq_countP_add_countP p l, countP_eq_length_filter]
+
+/-! ### filterMap -/
+
+@[simp]
+theorem length_filterMap_pos_iff {xs : List α} {f : α → Option β} :
+    0 < (filterMap f xs).length ↔ ∃ (x : α) (_ : x ∈ xs) (b : β), f x = some b := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [filterMap, mem_cons, exists_prop, exists_eq_or_imp]
+    split
+    · simp_all [ih]
+    · simp_all
+
+@[simp]
+theorem length_filterMap_lt_length_iff_exists {xs : List α} {f : α → Option β} :
+    (filterMap f xs).length < xs.length ↔ ∃ (x : α) (_ : x ∈ xs), f x = none := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [filterMap, mem_cons, exists_prop, exists_eq_or_imp]
+    split
+    · simp_all only [exists_prop, length_cons, true_or, iff_true]
+      have := length_filterMap_le f xs
+      omega
+    · simp_all
 
 /-! ### reverse -/
 

src/Init/Data/List/Nat/Sublist.lean

@@ -156,7 +156,7 @@ theorem append_sublist_of_sublist_left {xs ys zs : List α} (h : zs <+ xs) :
     have hl' := h'.length_le
     simp only [length_append] at hl'
     have : ys.length = 0 := by omega
-    simp_all only [Nat.add_zero, length_eq_zero, true_and, append_nil]
+    simp_all only [Nat.add_zero, length_eq_zero_iff, true_and, append_nil]
     exact Sublist.eq_of_length_le h' hl
   · rintro ⟨rfl, rfl⟩
     simp
@@ -169,7 +169,7 @@ theorem append_sublist_of_sublist_right {xs ys zs : List α} (h : zs <+ ys) :
     have hl' := h'.length_le
     simp only [length_append] at hl'
     have : xs.length = 0 := by omega
-    simp_all only [Nat.zero_add, length_eq_zero, true_and, append_nil]
+    simp_all only [Nat.zero_add, length_eq_zero_iff, true_and, append_nil]
     exact Sublist.eq_of_length_le h' hl
   · rintro ⟨rfl, rfl⟩
     simp

src/Init/Data/List/Range.lean

@@ -33,7 +33,7 @@ theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step)
   | _ + 1 => congrArg succ (length_range' _ _ _)
 
 @[simp] theorem range'_eq_nil_iff : range' s n step = [] ↔ n = 0 := by
-  rw [← length_eq_zero, length_range']
+  rw [← length_eq_zero_iff, length_range']
 
 @[deprecated range'_eq_nil_iff (since := "2025-01-29")] abbrev range'_eq_nil := @range'_eq_nil_iff
 
@@ -164,7 +164,7 @@ theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) :=
   simp only [range_eq_range', length_range']
 
 @[simp] theorem range_eq_nil {n : Nat} : range n = [] ↔ n = 0 := by
-  rw [← length_eq_zero, length_range]
+  rw [← length_eq_zero_iff, length_range]
 
 theorem range_ne_nil {n : Nat} : range n ≠ [] ↔ n ≠ 0 := by
   cases n <;> simp

src/Init/Data/List/TakeDrop.lean

@@ -45,7 +45,7 @@ theorem drop_one : ∀ l : List α, drop 1 l = tail l
     _ = succ (length l) - succ i := (Nat.succ_sub_succ_eq_sub (length l) i).symm
 
 theorem drop_of_length_le {l : List α} (h : l.length ≤ i) : drop i l = [] :=
-  length_eq_zero.1 (length_drop .. ▸ Nat.sub_eq_zero_of_le h)
+  length_eq_zero_iff.1 (length_drop .. ▸ Nat.sub_eq_zero_of_le h)
 
 theorem length_lt_of_drop_ne_nil {l : List α} {i} (h : drop i l ≠ []) : i < l.length :=
   gt_of_not_le (mt drop_of_length_le h)

src/Init/Data/List/ToArray.lean

@@ -44,6 +44,16 @@ theorem toArray_inj {as bs : List α} (h : as.toArray = bs.toArray) : as = bs :=
     | nil => simp at h
     | cons b bs => simpa using h
 
+theorem toArray_eq_iff {as : List α} {bs : Array α} : as.toArray = bs ↔ as = bs.toList := by
+  cases bs
+  simp
+
+-- We can't make this a `@[simp]` lemma because `#[] = [].toArray` at reducible transparency,
+-- so this would loop with `toList_eq_nil_iff`
+theorem eq_toArray_iff {as : Array α} {bs : List α} : as = bs.toArray ↔ as.toList = bs := by
+  cases as
+  simp
+
 @[simp] theorem size_toArrayAux {as : List α} {xs : Array α} :
     (as.toArrayAux xs).size = xs.size + as.length := by
   simp [size]
@@ -77,6 +87,21 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr
     l.toArray.back = l.getLast (by simp at h; exact ne_nil_of_length_pos h) := by
   simp [back, List.getLast_eq_getElem]
 
+@[simp] theorem _root_.Array.getLast!_toList [Inhabited α] (xs : Array α) :
+    xs.toList.getLast! = xs.back! := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp] theorem _root_.Array.getLast?_toList (xs : Array α) :
+    xs.toList.getLast? = xs.back? := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp] theorem _root_.Array.getLast_toList (xs : Array α) (h) :
+    xs.toList.getLast h = xs.back (by simpa [ne_nil_iff_length_pos] using h) := by
+  rcases xs with ⟨xs⟩
+  simp
+
 @[simp] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) :
     (l.toArray.set i a) = (l.set i a).toArray := rfl
 
@@ -514,8 +539,8 @@ private theorem popWhile_toArray_aux (p : α → Bool) (l : List α) :
 
 @[simp] theorem toArray_replicate (n : Nat) (v : α) : (List.replicate n v).toArray = mkArray n v := rfl
 
-@[deprecated toArray_replicate (since := "2024-12-13")]
-abbrev _root_.Array.mkArray_eq_toArray_replicate := @toArray_replicate
+theorem _root_.Array.mkArray_eq_toArray_replicate : mkArray n v = (List.replicate n v).toArray := by
+  simp
 
 @[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
 

src/Init/Data/NeZero.lean

@@ -40,3 +40,20 @@ theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 :=
 instance {p : Prop} [Decidable p] {n m : Nat} [NeZero n] [NeZero m] :
     NeZero (if p then n else m) := by
   split <;> infer_instance
+
+instance {n m : Nat} [h : NeZero n] : NeZero (n + m) where
+  out :=
+    match n, h, m with
+    | _ + 1, _, 0
+    | _ + 1, _, _ + 1 => fun h => nomatch h
+
+instance {n m : Nat} [h : NeZero m] : NeZero (n + m) where
+  out :=
+    match m, h, n with
+    | _ + 1, _, 0 => fun h => nomatch h
+    | _ + 1, _, _ + 1 => fun h => nomatch h
+
+instance {n m : Nat} [hn : NeZero n] [hm : NeZero m] : NeZero (n * m) where
+  out :=
+    match n, hn, m, hm with
+    | _ + 1, _, _ + 1, _ => fun h => nomatch h

src/Init/Data/Vector/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison
 prelude
 import Init.Data.Vector.Basic
 import Init.Data.Array.Attach
+import Init.Data.Array.Find
 
 /-!
 ## Vectors
@@ -662,12 +663,12 @@ protected theorem eq_empty (xs : Vector α 0) : xs = #v[] := by
 theorem eq_empty_of_size_eq_zero (xs : Vector α n) (h : n = 0) : xs = #v[].cast h.symm := by
   rcases xs with ⟨xs, rfl⟩
   apply toArray_inj.1
-  simp only [List.length_eq_zero, Array.toList_eq_nil_iff] at h
+  simp only [List.length_eq_zero_iff, Array.toList_eq_nil_iff] at h
   simp [h]
 
 theorem size_eq_one {xs : Vector α 1} : ∃ a, xs = #v[a] := by
   rcases xs with ⟨xs, h⟩
-  simpa using Array.size_eq_one.mp h
+  simpa using Array.size_eq_one_iff.mp h
 
 /-! ### push -/
 
@@ -1337,6 +1338,20 @@ theorem mem_setIfInBounds (xs : Vector α n) (i : Nat) (hi : i < n) (a : α) :
   cases ys
   simp
 
+/-! ### back -/
+
+theorem back_eq_getElem [NeZero n] (xs : Vector α n) : xs.back = xs[n - 1]'(by have := NeZero.ne n; omega) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.back_eq_getElem]
+
+theorem back?_eq_getElem? (xs : Vector α n) : xs.back? = xs[n - 1]? := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.back?_eq_getElem?]
+
+@[simp] theorem back_mem [NeZero n] {xs : Vector α n} : xs.back ∈ xs := by
+  cases xs
+  simp
+
 /-! ### map -/
 
 @[simp] theorem getElem_map (f : α → β) (xs : Vector α n) (i : Nat) (hi : i < n) :
@@ -2331,6 +2346,90 @@ theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} (r : β
   rcases xs with ⟨xs⟩
   simp
 
+/-! #### Further results about `back` and `back?` -/
+
+@[simp] theorem back?_eq_none_iff {xs : Vector α n} : xs.back? = none ↔ n = 0 := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+theorem back?_eq_some_iff {xs : Vector α n} {a : α} :
+    xs.back? = some a ↔ ∃ (w : 0 < n)(ys : Vector α (n - 1)), xs = (ys.push a).cast (by omega) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [back?_mk, Array.back?_eq_some_iff, mk_eq, toArray_cast, toArray_push]
+  constructor
+  · rintro ⟨ys, rfl⟩
+    simp
+    exact ⟨⟨ys, by simp⟩, by simp⟩
+  · rintro ⟨w, ⟨ys, h₁⟩, h₂⟩
+    exact ⟨ys, by simpa using h₂⟩
+
+@[simp] theorem back?_isSome {xs : Vector α n} : xs.back?.isSome ↔ n ≠ 0 := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp] theorem back_append_of_neZero {xs : Vector α n} {ys : Vector α m} [NeZero m] :
+    (xs ++ ys).back = ys.back := by
+  rcases xs with ⟨l⟩
+  rcases ys with ⟨l'⟩
+  simp only [mk_append_mk, back_mk]
+  rw [Array.back_append_of_size_pos]
+
+theorem back_append {xs : Vector α n} {ys : Vector α m} [NeZero (n + m)] :
+    (xs ++ ys).back =
+      if h' : m = 0 then
+        have : NeZero n := by subst h'; simp_all
+        xs.back
+      else
+        have : NeZero m := ⟨h'⟩
+        ys.back := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp [Array.back_append]
+  split <;> rename_i h
+  · rw [dif_pos]
+    simp_all
+  · rw [dif_neg]
+    rwa [Array.isEmpty_iff_size_eq_zero] at h
+
+theorem back_append_right {xs : Vector α n} {ys : Vector α m} [NeZero m] :
+    (xs ++ ys).back = ys.back := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [mk_append_mk, back_mk]
+  rw [Array.back_append_right]
+
+theorem back_append_left {xs : Vector α n} {ys : Vector α 0} [NeZero n] :
+    (xs ++ ys).back = xs.back := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, h⟩
+  simp only [mk_append_mk, back_mk]
+  rw [Array.back_append_left _ h]
+
+@[simp] theorem back?_append {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).back? = ys.back?.or xs.back? := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp
+
+theorem back?_flatMap {xs : Vector α n} {f : α → Vector β m} :
+    (xs.flatMap f).back? = xs.reverse.findSome? fun a => (f a).back? := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.back?_flatMap]
+  rfl
+
+theorem back?_flatten {xss : Vector (Vector α m) n} :
+    (flatten xss).back? = xss.reverse.findSome? fun xs => xs.back? := by
+  rcases xss with ⟨xss, rfl⟩
+  simp [Array.back?_flatten, ← Array.map_reverse, Array.findSome?_map, Function.comp_def]
+  rfl
+
+theorem back?_mkVector (a : α) (n : Nat) :
+    (mkVector n a).back? = if n = 0 then none else some a := by
+  rw [mkVector_eq_mk_mkArray]
+  simp only [back?_mk, Array.back?_mkArray]
+
+@[simp] theorem back_mkArray [NeZero n] : (mkVector n a).back = a := by
+  simp [back_eq_getElem]
+
 /-! ### leftpad and rightpad -/
 
 @[simp] theorem leftpad_mk (n : Nat) (a : α) (xs : Array α) (h : xs.size = m) :

src/Lean/Elab/Quotation.lean

@@ -190,7 +190,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
                 | $[some $ids:ident],* => $(quote inner)
                 | $[_%$ids],*          => Array.empty)
             | _ =>
-              let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back!
+              let arr ← ids[:ids.size - 1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back!
               `(Array.map (fun $(← mkTuple ids) => $(inner[0]!)) $arr)
           let arr ← if k == `sepBy then
             `(mkSepArray $arr $(getSepStxFromSplice arg))

src/Lean/Elab/Tactic/Basic.lean

@@ -177,7 +177,7 @@ where
     throwExs (failures : Array EvalTacticFailure) : TacticM Unit := do
      if h : 0 < failures.size  then
        -- For macros we want to report the error from the first registered / last tried rule (#3770)
-       let fail := failures[failures.size-1]
+       let fail := failures[failures.size - 1]
        fail.state.restore (restoreInfo := true)
        throw fail.exception -- (*)
      else

src/Lean/Meta/ArgsPacker.lean

@@ -560,7 +560,7 @@ where
   go : List Expr → Array Expr → MetaM α
   | [], acc => k acc
   | t::ts, acc => do
-    let name := if argsPacker.numFuncs = 1 then name else .mkSimple s!"{name}{acc.size+1}"
+    let name := if argsPacker.numFuncs = 1 then name else .mkSimple s!"{name}{acc.size + 1}"
     withLocalDeclD name t fun x => do
       go ts (acc.push x)
 

src/Lean/Meta/Constructions/BRecOn.lean

@@ -293,8 +293,8 @@ private def mkBRecOnFromRec (recName : Name) (ind reflexive : Bool) (nParams : N
         if let some n := all[i]? then
           if ind then mkIBelowName n else mkBelowName n
         else
-          if ind then .str all[0]! s!"ibelow_{i-all.size+1}"
-                 else .str all[0]! s!"below_{i-all.size+1}"
+          if ind then .str all[0]! s!"ibelow_{i-all.size + 1}"
+                 else .str all[0]! s!"below_{i-all.size + 1}"
       mkAppN (.const belowName blvls) (params ++ motives)
 
     -- create types of functionals (one for each motive)

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

@@ -197,7 +197,7 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
     (hg : ∀ {l l'}, Perm (g (l ++ l')) (g l ++ g l')) :
     Perm (toListModel (updateAllBuckets m.1.buckets f)) (g (toListModel m.1.2)) := by
   have hg₀ : g [] = [] := by
-    rw [← List.length_eq_zero]
+    rw [← List.length_eq_zero_iff]
     have := (hg (l := []) (l' := [])).length_eq
     rw [List.length_append, List.append_nil] at this
     omega

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -231,7 +231,7 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n)))
     apply Exists.intro <| Nat.le_refl arr.size
     intro c' heq
     simp only [Option.some.injEq] at heq
-    have hsize : List.length c'.clause = arr.size- arr.size := by
+    have hsize : List.length c'.clause = arr.size - arr.size := by
       simp [← heq, empty]
     apply Exists.intro hsize
     intro i

src/lake/Lake/Toml/Elab/Expression.lean

@@ -206,7 +206,7 @@ where
       if let some v := v? then
         match v with
         | .array ref vs =>
-          .array ref <| vs.modify (vs.size-1) fun
+          .array ref <| vs.modify (vs.size - 1) fun
           | .table ref t' => .table ref <| insert t' kRef k' ks newV
           | _ => .table kRef {}
         | .table ref t' => .table ref <| insert t' kRef k' ks newV