deprecation

src/Init/Data/List/Lemmas.lean

@@ -1699,9 +1699,15 @@ theorem join_singleton (l : List α) : [l].join = l := by simp
   | [] => by simp
   | b :: l => by simp [mem_join, or_and_right, exists_or]
 
-@[simp] theorem join_eq_nil_iff {L : List (List α)} : L.join = [] ↔ ∀ l ∈ L, l = [] := by
+@[simp] theorem join_eq_nil {L : List (List α)} : L.join = [] ↔ ∀ l ∈ L, l = [] := by
   induction L <;> simp_all
 
+@[deprecated join_eq_nil (since := "2024-08-22")]
+theorem join_eq_nil_iff {L : List (List α)} : L.join = [] ↔ ∀ l ∈ L, l = [] := join_eq_nil
+
+theorem join_ne_nil (xs : List (List α)) : xs.join ≠ [] ↔ ∃ x, x ∈ xs ∧ x ≠ [] := by
+  simp
+
 theorem exists_of_mem_join : a ∈ join L → ∃ l, l ∈ L ∧ a ∈ l := mem_join.1
 
 theorem mem_join_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ join L := mem_join.2 ⟨l, lL, al⟩
@@ -1799,7 +1805,7 @@ theorem mem_bind_of_mem {b : β} {l : List α} {f : α → List β} {a} (al : a
 
 @[simp]
 theorem bind_eq_nil {l : List α} {f : α → List β} : List.bind l f = [] ↔ ∀ x ∈ l, f x = [] :=
-  join_eq_nil_iff.trans <| by
+  join_eq_nil.trans <| by
     simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
 
 theorem forall_mem_bind {p : β → Prop} {l : List α} {f : α → List β} :
@@ -2096,6 +2102,12 @@ theorem reverse_eq_iff {as bs : List α} : as.reverse = bs ↔ as = bs.reverse :
 @[simp] theorem head?_reverse (l : List α) : l.reverse.head? = l.getLast? := by
   rw [← getLast?_reverse, reverse_reverse]
 
+theorem getLast?_eq_head?_reverse {xs : List α} : xs.getLast? = xs.reverse.head? := by
+  simp
+
+theorem head?_eq_getLast?_reverse {xs : List α} : xs.head? = xs.reverse.getLast? := by
+  simp
+
 @[simp] theorem map_reverse (f : α → β) (l : List α) : l.reverse.map f = (l.map f).reverse := by
   induction l <;> simp [*]
 

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

@@ -23,8 +23,6 @@ open Nat
 theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step) n step := by
   simp [range', Nat.add_succ, Nat.mul_succ]
 
-@[simp] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl
-
 @[simp] theorem length_range' (s step) : ∀ n : Nat, length (range' s n step) = n
   | 0 => rfl
   | _ + 1 => congrArg succ (length_range' _ _ _)
@@ -32,6 +30,14 @@ theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step)
 @[simp] theorem range'_eq_nil : range' s n step = [] ↔ n = 0 := by
   rw [← length_eq_zero, length_range']
 
+theorem range'_ne_nil (s n : Nat) : range' s n ≠ [] ↔ n ≠ 0 := by
+  cases n <;> simp
+
+@[simp] theorem range'_zero : range' s 0 = [] := by
+  simp
+
+@[simp] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl
+
 theorem mem_range' : ∀{n}, m ∈ range' s n step ↔ ∃ i < n, m = s + step * i
   | 0 => by simp [range', Nat.not_lt_zero]
   | n + 1 => by
@@ -45,6 +51,21 @@ theorem mem_range' : ∀{n}, m ∈ range' s n step ↔ ∃ i < n, m = s + step *
     fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩,
     fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩
 
+theorem head?_range' (n : Nat) : (range' s n).head? = if n = 0 then none else some s := by
+  induction n <;> simp_all [range'_succ, head?_append]
+
+theorem getLast?_range' (n : Nat) : (range' s n).getLast? = if n = 0 then none else some (s + n - 1) := by
+  induction n generalizing s with
+  | zero => simp
+  | succ n ih =>
+    rw [range'_succ, getLast?_cons, ih]
+    by_cases h : n = 0
+    · rw [if_pos h]
+      simp [h]
+    · rw [if_neg h]
+      simp
+      omega
+
 theorem pairwise_lt_range' s n (step := 1) (pos : 0 < step := by simp) :
     Pairwise (· < ·) (range' s n step) :=
   match s, n, step, pos with
@@ -153,6 +174,9 @@ theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) :=
 @[simp] theorem range_eq_nil {n : Nat} : range n = [] ↔ n = 0 := by
   rw [← length_eq_zero, length_range]
 
+theorem range_ne_nil (n : Nat) : range n ≠ [] ↔ n ≠ 0 := by
+  cases n <;> simp
+
 @[simp]
 theorem range_sublist {m n : Nat} : range m <+ range n ↔ m ≤ n := by
   simp only [range_eq_range', range'_sublist_right]
@@ -188,6 +212,13 @@ theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·
   rw [← range'_eq_map_range]
   simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm
 
+theorem head?_range (n : Nat) : (range n).head? = if n = 0 then none else some 0 := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [range_succ, head?_append, ih]
+    split <;> simp_all
+
 theorem take_range (m n : Nat) : take m (range n) = range (min m n) := by
   apply List.ext_getElem
   · simp
@@ -204,6 +235,12 @@ theorem iota_eq_reverse_range' : ∀ n : Nat, iota n = reverse (range' 1 n)
 
 @[simp] theorem length_iota (n : Nat) : length (iota n) = n := by simp [iota_eq_reverse_range']
 
+@[simp] theorem iota_eq_nil (n : Nat) : iota n = [] ↔ n = 0 := by
+  cases n <;> simp
+
+theorem iota_ne_nil (n : Nat) : iota n ≠ [] ↔ n ≠ 0 := by
+  cases n <;> simp
+
 @[simp]
 theorem mem_iota {m n : Nat} : m ∈ iota n ↔ 1 ≤ m ∧ m ≤ n := by
   simp [iota_eq_reverse_range', Nat.add_comm, Nat.lt_succ]
@@ -214,6 +251,25 @@ theorem pairwise_gt_iota (n : Nat) : Pairwise (· > ·) (iota n) := by
 theorem nodup_iota (n : Nat) : Nodup (iota n) :=
   (pairwise_gt_iota n).imp Nat.ne_of_gt
 
+
+@[simp] theorem head?_iota (n : Nat) : (iota n).head? = if n = 0 then none else some n := by
+  cases n <;> simp
+
+@[simp] theorem head_iota (n : Nat) (h) : (iota n).head h = n := by
+  cases n with
+  | zero => simp at h
+  | succ n => simp
+
+@[simp] theorem reverse_iota : reverse (iota n) = range' 1 n := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [iota_succ, reverse_cons, ih, range'_1_concat, Nat.add_comm]
+
+@[simp] theorem getLast?_iota (n : Nat) : (iota n).getLast? = if n = 0 then none else some 1 := by
+  rw [getLast?_eq_head?_reverse]
+  simp [head?_range']
+
 /-! ### enumFrom -/
 
 @[simp]

src/Init/Data/List/Sublist.lean

@@ -490,7 +490,7 @@ theorem sublist_join_iff {L : List (List α)} {l} :
       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 [join_nil, sublist_nil, join_eq_nil]
       simp only [getElem?_nil, Option.getD_none, sublist_nil] at h
       exact (forall_getElem L' (· = [])).1 h
   | cons l' L ih =>