Merge branch 'nightly-testing-pre-2024-07-31' into nightly-testing

Batteries/Data/List/EraseIdx.lean

@@ -17,75 +17,15 @@ namespace List
 universe u v
 variable {α : Type u} {β : Type v}
 
-@[simp] theorem eraseIdx_zero (l : List α) : eraseIdx l 0 = tail l := by cases l <;> rfl
-
-theorem eraseIdx_eq_take_drop_succ :
-    ∀ (l : List α) (i : Nat), l.eraseIdx i = l.take i ++ l.drop (i + 1)
-  | nil, _ => by simp
-  | a::l, 0 => by simp
-  | a::l, i + 1 => by simp [eraseIdx_eq_take_drop_succ l i]
-
-theorem eraseIdx_sublist : ∀ (l : List α) (k : Nat), eraseIdx l k <+ l
-  | [], _ => by simp
-  | a::l, 0 => by simp
-  | a::l, k + 1 => by simp [eraseIdx_sublist l k]
-
-theorem eraseIdx_subset (l : List α) (k : Nat) : eraseIdx l k ⊆ l := (eraseIdx_sublist l k).subset
-
-@[simp]
-theorem eraseIdx_eq_self : ∀ {l : List α} {k : Nat}, eraseIdx l k = l ↔ length l ≤ k
-  | [], _ => by simp
-  | a::l, 0 => by simp [(cons_ne_self _ _).symm]
-  | a::l, k + 1 => by simp [eraseIdx_eq_self]
-
-alias ⟨_, eraseIdx_of_length_le⟩ := eraseIdx_eq_self
-
-theorem eraseIdx_append_of_lt_length {l : List α} {k : Nat} (hk : k < length l) (l' : List α) :
-    eraseIdx (l ++ l') k = eraseIdx l k ++ l' := by
-  rw [eraseIdx_eq_take_drop_succ, take_append_of_le_length, drop_append_of_le_length,
-    eraseIdx_eq_take_drop_succ, append_assoc]
-  all_goals omega
-
-theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤ k) (l' : List α) :
-    eraseIdx (l ++ l') k = l ++ eraseIdx l' (k - length l) := by
-  rw [eraseIdx_eq_take_drop_succ, eraseIdx_eq_take_drop_succ,
-    take_append_eq_append_take, drop_append_eq_append_drop,
-    take_of_length_le hk, drop_eq_nil_of_le (by omega), nil_append, append_assoc]
-  congr
-  omega
-
-protected theorem IsPrefix.eraseIdx {l l' : List α} (h : l <+: l') (k : Nat) :
-    eraseIdx l k <+: eraseIdx l' k := by
-  rcases h with ⟨t, rfl⟩
-  if hkl : k < length l then
-    simp [eraseIdx_append_of_lt_length hkl]
-  else
-    rw [Nat.not_lt] at hkl
-    simp [eraseIdx_append_of_length_le hkl, eraseIdx_of_length_le hkl]
-
-theorem mem_eraseIdx_iff_getElem {x : α} :
-    ∀ {l} {k}, x ∈ eraseIdx l k ↔ ∃ i : Fin l.length, ↑i ≠ k ∧ l[i.1] = x
-  | [], _ => by
-    simp only [eraseIdx, Fin.exists_iff, not_mem_nil, false_iff]
-    rintro ⟨i, h, -⟩
-    exact Nat.not_lt_zero _ h
-  | a::l, 0 => by simp [Fin.exists_fin_succ, mem_iff_get]
-  | a::l, k+1 => by
-    simp [Fin.exists_fin_succ, mem_eraseIdx_iff_getElem, @eq_comm _ a, k.succ_ne_zero.symm]
-
 @[deprecated mem_eraseIdx_iff_getElem (since := "2024-06-12")]
 theorem mem_eraseIdx_iff_get {x : α} {l} {k} :
     x ∈ eraseIdx l k ↔ ∃ i : Fin l.length, ↑i ≠ k ∧ l.get i = x := by
-  simp [mem_eraseIdx_iff_getElem]
-
-theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i ≠ k, l[i]? = some x := by
-  simp only [mem_eraseIdx_iff_getElem, getElem_eq_iff, Fin.exists_iff, exists_and_left]
-  refine exists_congr fun i => and_congr_right' ?_
+  simp only [mem_eraseIdx_iff_getElem, ne_eq, exists_and_left, get_eq_getElem]
   constructor
-  · rintro ⟨_, h⟩; exact h
-  · rintro h;
-    obtain ⟨h', -⟩ := getElem?_eq_some.1 h
-    exact ⟨h', h⟩
+  · rintro ⟨i, h, w, rfl⟩
+    exact ⟨⟨i, w⟩, h, rfl⟩
+  · rintro ⟨i, h, rfl⟩
+    exact ⟨i.1, h, i.2, rfl⟩
 
 @[deprecated mem_eraseIdx_iff_getElem? (since := "2024-06-12")]
 theorem mem_eraseIdx_iff_get? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i ≠ k, l.get? i = x := by

Batteries/Data/List/Pairwise.lean

@@ -42,53 +42,6 @@ theorem pairwise_of_reflexive_on_dupl_of_forall_ne [DecidableEq α] {l : List α
     apply h <;> try (apply hab.subset; simp)
     exact heq
 
-/-- given a list `is` of monotonically increasing indices into `l`, getting each index
-  produces a sublist of `l`.  -/
-theorem map_get_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pairwise (·.val < ·.val)) :
-    is.map (get l) <+ l := by
-  suffices ∀ n l', l' = l.drop n → (∀ i ∈ is, n ≤ i) → map (get l) is <+ l'
-    from this 0 l (by simp) (by simp)
-  intro n l' hl' his
-  induction is generalizing n l' with
-  | nil => simp
-  | cons hd tl IH =>
-    simp; cases hl'
-    have := IH h.of_cons (hd+1) _ rfl (pairwise_cons.mp h).1
-    specialize his hd (.head _)
-    have := (drop_eq_getElem_cons ..).symm ▸ this.cons₂ (get l hd)
-    have := Sublist.append (nil_sublist (take hd l |>.drop n)) this
-    rwa [nil_append, ← (drop_append_of_le_length ?_), take_append_drop] at this
-    simp [Nat.min_eq_left (Nat.le_of_lt hd.isLt), his]
-
-/-- given a sublist `l' <+ l`, there exists a list of indices `is` such that
-  `l' = map (get l) is`. -/
-theorem sublist_eq_map_get (h : l' <+ l) : ∃ is : List (Fin l.length),
-    l' = map (get l) is ∧ is.Pairwise (· < ·) := by
-  induction h with
-  | slnil => exact ⟨[], by simp⟩
-  | cons _ _ IH =>
-    let ⟨is, IH⟩ := IH
-    refine ⟨is.map (·.succ), ?_⟩
-    simp [comp, pairwise_map]
-    exact IH
-  | cons₂ _ _ IH =>
-    rcases IH with ⟨is,IH⟩
-    refine ⟨⟨0, by simp [Nat.zero_lt_succ]⟩ :: is.map (·.succ), ?_⟩
-    simp [comp_def, pairwise_map, IH, ← get_eq_getElem]
-
-theorem pairwise_iff_getElem : Pairwise R l ↔
-    ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j] := by
-  rw [pairwise_iff_forall_sublist]
-  constructor <;> intro h
-  · intros i j hi hj h'
-    apply h
-    simpa [h'] using map_get_sublist (is := [⟨i, hi⟩, ⟨j, hj⟩])
-  · intros a b h'
-    have ⟨is, h', hij⟩ := sublist_eq_map_get h'
-    rcases is with ⟨⟩ | ⟨a', ⟨⟩ | ⟨b', ⟨⟩⟩⟩ <;> simp at h'
-    rcases h' with ⟨rfl, rfl⟩
-    apply h; simpa using hij
-
 theorem pairwise_iff_get : Pairwise R l ↔ ∀ (i j) (_hij : i < j), R (get l i) (get l j) := by
   rw [pairwise_iff_getElem]
   constructor <;> intro h