feat: List.erase_range (#5215)

src/Init/Data/List/Lemmas.lean

@@ -369,6 +369,21 @@ theorem mem_concat_self (xs : List α) (a : α) : a ∈ xs ++ [a] :=
 
 theorem mem_append_cons_self : a ∈ xs ++ a :: ys := mem_append_of_mem_right _ (mem_cons_self _ _)
 
+theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a ∈ xs) :
+    ∃ as bs, xs = as ++ a :: bs ∧ a ∉ as := by
+  induction xs with
+  | nil => cases h
+  | cons x xs ih =>
+    simp at h
+    cases h with
+    | inl h => exact ⟨[], xs, by simp_all⟩
+    | inr h =>
+      by_cases h' : a = x
+      · subst h'
+        exact ⟨[], xs, by simp⟩
+      · obtain ⟨as, bs, rfl, h⟩ := ih h
+        exact ⟨x :: as, bs, rfl, by simp_all⟩
+
 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 :=

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

@@ -8,6 +8,7 @@ import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Range
 import Init.Data.List.Pairwise
 import Init.Data.List.Find
+import Init.Data.List.Erase
 
 /-!
 # Lemmas about `List.range` and `List.enum`
@@ -228,6 +229,28 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
   rw [find?_eq_none]
   simp
 
+theorem erase_range' :
+    (range' s n).erase i =
+      range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1)) := by
+  by_cases h : i ∈ range' s n
+  · obtain ⟨as, bs, h₁, h₂⟩ := eq_append_cons_of_mem h
+    rw [h₁, erase_append_right _ h₂, erase_cons_head]
+    rw [range'_eq_append_iff] at h₁
+    obtain ⟨k, -, rfl, hbs⟩ := h₁
+    rw [eq_comm, range'_eq_cons_iff] at hbs
+    obtain ⟨rfl, -, rfl⟩ := hbs
+    simp at h
+    congr 2 <;> omega
+  · rw [erase_of_not_mem h]
+    simp only [mem_range'_1, not_and, Nat.not_lt] at h
+    by_cases h' : s ≤ i
+    · have p : min s (i + 1) + n - (i + 1) = 0 := by omega
+      simp [p]
+      omega
+    · have p : i - s = 0 := by omega
+      simp [p]
+      omega
+
 /-! ### range -/
 
 theorem range_loop_range' : ∀ s n : Nat, range.loop s (range' s n) = range' 0 (n + s)
@@ -335,6 +358,9 @@ theorem nodup_range (n : Nat) : Nodup (range n) := by
     (range n).find? p = none ↔ ∀ i, i < n → !p i := by
   simp [range_eq_range']
 
+theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1)) := by
+  simp [range_eq_range', erase_range']
+
 /-! ### iota -/
 
 theorem iota_eq_reverse_range' : ∀ n : Nat, iota n = reverse (range' 1 n)